some random stuff

no_rec_2_rec.lean

import Mathlib

example (p1: (V:Rat) = I * R)(vnz: Not (V = 0))(rnz: Not (R = 0)) : R = (I *  R ^ 2) / V := by
  let target := p1
  let s1 : V = I * R <-> V / V = I * R / V := by 
    exact (iff_true_right (congrFun (congrArg HDiv.hDiv p1) V)).mpr p1
  rw [s1] at target
  let v_on_v_one: V / V = 1 := by
    exact (div_eq_one_iff_eq vnz).mpr rfl
  rw [v_on_v_one] at target
  let tmp2 : 1 = I * R / V <-> 1 * R = (I * R / V) * R := by 
    exact Iff.symm (mul_left_inj' rnz)
  rw [tmp2] at target
  simp only [one_mul] at target
  let tmp3 : I * R / V * R = I * R * R / V := by
    exact div_mul_eq_mul_div (I * R) V R
  rw [tmp3] at target
  let tmp4 : I * R * R = R * R * I := by exact mul_rotate I R R
  rw [tmp4] at target
  let tmp5: R * R = R ^ 2 := by exact Eq.symm (pow_two R)
  rw [tmp5] at target
  let tmp6: R ^ 2 * I = I * R ^ 2 := by exact Rat.mul_comm (R ^ 2) I
  rw [tmp6] at target
  exact target