plskillme.lean

example {x:Rat} : 3 * x / 0.2 = (2 + 1/2) / (3 + 1/3) -> x = 1/20 := by
  let is1 : (0.2:Rat) = 1/5 := by rfl
  rw [is1]
  let is2 : 3 * x / (1/5) = 3 * x * 5 := by
    simp_all only [one_div, div_inv_eq_mul]
  rw [is2]
  let is3 : 3 * x * 5 = 15 * x := by
    calc
      3 * x * 5 = 3 * 5 * x := mul_right_comm 3 x 5
      3 * 5 * _ = 15 * x := by 
        simp_all only [mul_eq_mul_right_iff]
        apply Or.inl
        rfl
  rw [is3]
  let is4 : (2:Rat) + 1/2 = 5/2 := by rfl
  rw [is4]
  let is5 : (3:Rat) + 1/3 = 10/3 := by rfl
  rw [is5]
  let is6 : (5:Rat)/2/(10/3) = 5/2 * (3/10) := by rfl
  rw [is6]
  let is7: ((5:Rat)/2) * (3/10) = 15/20 := by rfl
  rw [is7]
  let is8: 15*x=15/20 <-> 15*x*(1/15)=15/20*(1/15):= by 
    simp_all only [one_div, mul_eq_mul_right_iff, inv_eq_zero,OfNat.ofNat_ne_zero, or_false]
  rw [is8]
  let is9: 15*x*(1/15) = x := by 
    refine (div_eq_iff_mul_eq ?hb).mp ?_
    refine one_div_ne_zero ?hb.h
    trivial
    let is1 : (x:Rat) / (1/15) = x * 15 := by aesop
    rw [is1]
    rw [Rat.mul_comm]
  rw [is9]
  let is10 : (15:Rat)/20 * (1/15) = 1/20 := by aesop
  rw [is10]
  apply id