Basic algebra in lean

tedium.lean

import Mathlib
import Lean.Meta

macro "rwi" pat:term "=>" new:term ":=" prf:term : tactic =>
  `(tactic| rewrite [let _eq : $pat = $new := $prf ; _eq ])

macro "rwi" pat:term "=>" new:term "at" loc:Lean.Parser.Tactic.locationHyp ":=" prf:term : tactic =>
  `(tactic| rewrite [let _eq : $pat = $new := $prf ; _eq ] at $loc)

def wmap : Type _ -> Type _ -> Type _ | A, B => @Subtype (Prod (A -> B) (B -> A)) fun ⟨ f , h ⟩ => ∀ i, h (f i) = i

def p1 : (w:wmap A B) -> let ⟨ ⟨ _ , h ⟩ , _ ⟩ := w; ∀ a:A , @Subtype B fun b => h b = a := by
  intro w
  let ⟨ ⟨ f , h ⟩ , p ⟩ := w
  simp at p
  simp
  intro a
  refine ⟨ f a , ?_ ⟩
  apply p

def mkwmap (f: A -> B)(h:B->A)(p: ∀ i, h (f i) = i) : wmap A B := ⟨ ⟨ f , h ⟩  , p ⟩

def symmetric (f:A->B) := { h:B->A // ∀ i, h (f i) = i }

def symm_fun_inj: (p1: symmetric f) -> Function.Injective f := by
  intro ⟨ h , p ⟩
  exact Function.LeftInverse.injective p


def wmap_inj (w:wmap A B) : Function.Injective w.val.fst := by
  let ⟨ _ , p ⟩ := w;
  exact Function.LeftInverse.injective p

def add_invar_real_alt {a b:Real}(c:Real) : (a + c = b + c) -> a = b := by
  apply symm_fun_inj (f:=fun i => i + c)
  refine Subtype.mk ?_ ?_
  exact fun i => i - c
  simp only [add_sub_cancel_right, implies_true]

def add_invar_real {a b:Real}(c:Real) : (a + c = b + c) -> a = b := by
  let m := by
    refine @mkwmap Real Real ?_ ?_ ?_
    exact fun i => i + c
    exact fun i => i - c
    intro i
    exact add_sub_cancel_right i c

  apply wmap_inj m




def pow_invar_1 {a b c : Real} (h1: a >= 0)(h2: b >= 0)(h3:Not (c = 0)) : a ^ c = b ^ c -> a = b := by
  let _eq1 : wmap { i:Real // i >= 0 } { i:Real // i >= 0 } := by
    refine mkwmap ?_ ?_ ?_
    exact fun ⟨ i , p ⟩  => by
      refine ⟨ i ^ c , ?_ ⟩
      exact Real.rpow_nonneg p c
    exact fun ⟨ i , p ⟩ => by
      refine ⟨ i ^ (1 / c) , ?_ ⟩
      exact Real.rpow_nonneg p (1 / c)
    intro ⟨ i , p ⟩
    dsimp
    rw [@Subtype.mk_eq_mk]
    let eq1 : (i ^ c) ^ (1 / c) = i ^ (c * (1 / c)) := by
      refine Eq.symm (Real.rpow_mul ?_ c (1 / c))
      exact p
    rw [eq1]
    let eq3 : c * (1 / c) = 1 := by
      exact mul_one_div_cancel h3
    rw [eq3]
    norm_num
  let _eq2 := wmap_inj _eq1
  unfold Function.Injective _eq1 mkwmap at _eq2
  simp only [Subtype.forall, ge_iff_le, Subtype.mk.injEq] at _eq2
  let _eq2 := _eq2 a h1 b h2
  exact _eq2

def pow_invar_2 {a b c : Real} (h1: a >= 0)(h2: b >= 0)(h3:Not (c = 0)) : a ^ c = b ^ c <-> a = b := by
  apply Iff.intro
  exact fun a_1 => pow_invar_1 h1 h2 h3 a_1
  intro i
  rw [i]

def pows_to_mult {a b c:Real} (h1:a >= 0): (a ^ b) ^ c = a ^ (b * c) := by
  exact Eq.symm (Real.rpow_mul h1 b c)

def pow2_r {a b:Real} : (a * b) ^ (2:Real) = (a ^ 2) * (b ^ 2) := by
  rw [Real.rpow_two]
  exact mul_pow a b 2

def hmm : wmap { i // i = (Not P -> P)  } { i // i = (Not P -> False) } := by
  refine mkwmap ?_ ?_ ?_
  intro ⟨ r , p ⟩
  refine ⟨ r , ?_ ⟩
  rw [p]
  refine Eq.symm (implies_congr_ctx rfl ?_)
  exact fun a => Eq.symm (eq_false a)
  intro ⟨ r , p ⟩
  refine ⟨ r , ?_ ⟩
  rw [p]
  refine Eq.symm (implies_congr_ctx rfl ?_)
  exact fun a => eq_false a
  simp only [Subtype.coe_eta, implies_true]

-- -- cuberoot(7x) = sqrt(x) -> x = 49
-- set_option pp.proofs false in
example {x:Real}{xnz:x>=0} : (7 * x) ^ ((1:Real) / 3) = x ^ ((1:Real) / 2) -> x = 49 ∨ x = 0 := by
  let _eq1 := by
    refine pow_invar_2 (a:=(7 * x) ^ ((1:Real) / 3)) (b:=x ^ ((1:Real) / 2)) (c:=6) ?_ ?_ ?_
    {
      refine Real.rpow_nonneg ?_ (1 / 3)
      simp only [Nat.ofNat_pos, mul_nonneg_iff_of_pos_left]
      exact xnz
    }
    { exact Real.rpow_nonneg xnz (1 / 2)}
    { exact OfNat.ofNat_ne_zero 6 }
  rw [<- _eq1]
  clear _eq1
  rwi ((7 * x) ^ ((1:Real) / 3)) ^ (6:Real) => ((7 * x) ^ (6 * ((1:Real) / 3))) := by
    rw [@mul_one_div, pows_to_mult]
    norm_num
    norm_num
    exact xnz
  rewrite [pows_to_mult]
  ring_nf
  rewrite [pow2_r]
  ring_nf
  let _eq3 : (x ^ (2:Real) * 49 = x ^ (3:Real)) <-> ((x ^ (2:Real) * 49) - x ^ (3:Real) = 0) := by
    exact Iff.symm sub_eq_zero
  rw [← Real.rpow_two, _eq3]
  clear _eq3
  -- intro i
  -- by_contra ta
  -- let _eq_2 : Not (x = 49 ∨ x = 0) -> (Not (x = 49)) ∧ (Not (x = 0)) := by
  --   exact fun a => (fun {p q} => not_or.mp) ta
  -- let ⟨ c , _ ⟩ := _eq_2 ta
  -- clear _eq_2 ta
  let _eq : (x ^ (2:Real) * 49 - x ^ (3:Real) = 0) <-> (x ^ (2:Real) * (49 - x) = 0) := by
    refine eq_zero_iff_eq_zero_of_add_eq_zero ?_
    let _eq : (49:Real) - x = -x + 49 := by
      exact sub_eq_neg_add 49 x
    rw [_eq]
    let _eq2 : -x + 49 = -1 * (x - 49) := by
      norm_num
      rw [<-_eq]
    rw [_eq2]
    clear _eq2 _eq
    rwi x ^ (2:Real) * (-1 * (x - 49)) => -1 * (x ^ (2:Real) * (x - 49)) := by
      exact mul_left_comm (x ^ 2) (-1) (x - 49)
    rwi x ^ (2:Real) * 49 - x ^ (3:Real) => x ^ (2:Real) * (49 - x) := by
      refine Eq.symm (CancelDenoms.sub_subst rfl ?_)
      calc
        x^(2 : ℝ) * x = x^(2 + 1 : ℝ) := by rw [Real.rpow_two]; norm_cast
        _ = x^(3 : ℝ) := by norm_num
    rwi -1 * (x ^ (2:Real) * (x - 49)) => x ^ (2:Real) * (-1 * (x - 49)) := by
      exact mul_left_comm (-1) (x ^ 2) (x - 49)
    rwi x ^ (2:Real) * (49 - x) + x ^ (2:Real) * (-1 * (x - 49)) => x ^ (2:Real) * ((49 - x) + (-1 * (x - 49))) := by
      exact Eq.symm (LeftDistribClass.left_distrib (x ^ 2) (49 - x) (-1 * (x - 49)))
    rwi -1 * (x - 49) => -x + 49 := by norm_num; exact sub_eq_neg_add 49 x
    rwi 49 - x => -x + 49 := by exact sub_eq_neg_add 49 x
    rwi -x + 49 + (-x + 49) => 2 * (-x + 49) := by exact Eq.symm (two_mul (-x + 49))
    rwi 2 * (-x + 49) => -2 * x + 98 := by ring_nf
    let _roots : x ^ 2 = 0 ∨ -2 * x + 98 = 0 -> x ^ (2:Real) * (-2 * x + 98) = 0 := by norm_num
    apply _roots
    clear _roots
    refine .inr ?_
    rwi -2 * x + 98 = 0 => -2 * x = -98 := by
      apply propext
      exact Iff.symm eq_neg_iff_add_eq_zero
    rwi -2 * x = -98 => x = -98 / -2 := by
      norm_num
      refine Function.Injective.eq_iff' ?_ ?_
      unfold Function.Injective
      intro a b
      let eq : wmap Real Real := by
        refine mkwmap ?_ ?_ ?_
        exact fun i => i * 2
        exact fun i => i / 2
        intro i
        ring_nf
      let _eq := wmap_inj eq
      unfold Function.Injective eq mkwmap at _eq
      simp only [OfNat.ofNat_ne_zero, or_false ] at _eq
      rw [NonUnitalNormedCommRing.mul_comm 2 a, NonUnitalNormedCommRing.mul_comm 2 b]
      apply _eq
      ring_nf
    ring_nf
    admit
  rw [_eq]
  clear _eq
  intro h
  rw [mul_eq_zero] at h
  cases h
  case _ h =>
    refine .inr ?_
    let eq := by
      refine pow_invar_2 (a:= x ^ (2:Real)) (b:=0) (c:=(1:Real)/2) ?_ ?_ ?_
      exact Real.rpow_nonneg xnz 2
      exact Preorder.le_refl 0
      simp only [one_div, inv_eq_zero, OfNat.ofNat_ne_zero, not_false_eq_true]
    rw [<-eq] at h
    clear eq
    rwi ((x ^ (2:Real)) ^ ((1:Real) / 2) = 0 ^ ((1:Real) / 2)) => (x = 0) at h := by
      rwi (x ^ (2:Real)) ^ ((1:Real) / 2) => x ^ (2 * ((1:Real)/2)) := by
        exact pows_to_mult xnz
      rwi (2 * ((1:Real) / 2)) => 1 := by
        norm_num
      rwi (x ^ (1:Real)) => x := by
        exact Real.rpow_one x
      rwi (0:Real) ^ ((1:Real) / 2) => 0 := by
        refine Real.zero_rpow ?_
        norm_num
      rfl
    exact h
  case _ h =>
    refine .inl ?_
    rwi 49 - x = 0 => - x = -49 at h := by
      rwi 49 - x => -x + 49 := by
        exact sub_eq_neg_add 49 x
      apply propext
      apply Iff.intro
      intro i
      exact Eq.symm (neg_eq_of_add_eq_zero_right h)
      intro i
      exact eq_neg_iff_add_eq_zero.mp i
    rwi -x = -49 => x = 49 at h := by
      apply propext
      exact neg_inj
    exact h
  exact xnz