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

State before:
d a b : ℕ
inst✝ : NeZero d
⊢ normalized (of_fraction d a b)
Tactic:
refine ⟨?_, ?_⟩
State after:
case refine_1
d a b : ℕ
inst✝ : NeZero d
⊢ of_fraction d a b 0 = 0

case refine_2
d a b : ℕ
inst✝ : NeZero d
⊢ Monotone (of_fraction d a b)

State before:
case refine_1
d a b : ℕ
inst✝ : NeZero d
⊢ of_fraction d a b 0 = 0
Tactic:
simp [of_fraction]
State after:
no goals

State before:
case refine_2
d a b : ℕ
inst✝ : NeZero d
⊢ Monotone (of_fraction d a b)
Tactic:
have help : ∀ i j : Fin 3, i ≤ j → i = 0 ∨ (i = j) ∨ (i = 1 ∧ j = 2)
State after:
case help
d a b : ℕ
inst✝ : NeZero d
⊢ ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2

case refine_2
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
⊢ Monotone (of_fraction d a b)

State before:
case refine_2
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
⊢ Monotone (of_fraction d a b)
Tactic:
intro i j hij
State after:
case refine_2
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i j : Fin (Nat.succ 2)
hij : i ≤ j
⊢ of_fraction d a b i ≤ of_fraction d a b j

State before:
case refine_2
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i j : Fin (Nat.succ 2)
hij : i ≤ j
⊢ of_fraction d a b i ≤ of_fraction d a b j
Tactic:
rcases help i j hij with rfl | rfl | ⟨rfl, rfl⟩
State after:
case refine_2.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
j : Fin (Nat.succ 2)
hij : 0 ≤ j
⊢ of_fraction d a b 0 ≤ of_fraction d a b j

case refine_2.inr.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i : Fin (Nat.succ 2)
hij : i ≤ i
⊢ of_fraction d a b i ≤ of_fraction d a b i

case refine_2.inr.inr.intro
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
hij : 1 ≤ 2
⊢ of_fraction d a b 1 ≤ of_fraction d a b 2

State before:
case help
d a b : ℕ
inst✝ : NeZero d
⊢ ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
Tactic:
decide
State after:
no goals

State before:
case refine_2.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
j : Fin (Nat.succ 2)
hij : 0 ≤ j
⊢ of_fraction d a b 0 ≤ of_fraction d a b j
Tactic:
simp [of_fraction]
State after:
no goals

State before:
case refine_2.inr.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i : Fin (Nat.succ 2)
hij : i ≤ i
⊢ of_fraction d a b i ≤ of_fraction d a b i
Tactic:
exact le_rfl
State after:
no goals

State before:
case refine_2.inr.inr.intro
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
hij : 1 ≤ 2
⊢ of_fraction d a b 1 ≤ of_fraction d a b 2
Tactic:
simp [of_fraction]
State after:
no goals