Theorem: Weight.ex_of_fraction (Weights/Dimension2.lean)

State before:
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ ∃ a b, w = of_fraction d a b
Tactic:
refine ⟨w 2 - w 1, w 1, funext <| fun i ↦ ?_⟩
State after:
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
i : Fin (Nat.succ 2)
⊢ w i = of_fraction d (w 2 - w 1) (w 1) i

State before:
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
i : Fin (Nat.succ 2)
⊢ w i = of_fraction d (w 2 - w 1) (w 1) i
Tactic:
fin_cases i
State after:
case head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 0, isLt := (_ : 0 < Nat.succ 2) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 0, isLt := (_ : 0 < Nat.succ 2) }

case tail.head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 1, isLt := (_ : (fun a => a < Nat.succ 2) 1) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 1, isLt := (_ : (fun a => a < Nat.succ 2) 1) }

case tail.tail.head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 2, isLt := (_ : (fun a => (fun a => a < Nat.succ 2) a) 2) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 2, isLt := (_ : (fun a => (fun a => a < Nat.succ 2) a) 2) }

State before:
case head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 0, isLt := (_ : 0 < Nat.succ 2) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 0, isLt := (_ : 0 < Nat.succ 2) }
Tactic:
simp [of_fraction, h.1]
State after:
no goals

State before:
case tail.head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 1, isLt := (_ : (fun a => a < Nat.succ 2) 1) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 1, isLt := (_ : (fun a => a < Nat.succ 2) 1) }
Tactic:
simp [of_fraction]
State after:
no goals

State before:
case tail.tail.head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 2, isLt := (_ : (fun a => (fun a => a < Nat.succ 2) a) 2) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 2, isLt := (_ : (fun a => (fun a => a < Nat.succ 2) a) 2) }
Tactic:
exact Nat.eq_add_of_sub_eq (h.2 (Fin.coe_sub_iff_le.mp rfl)) rfl
State after:
no goals