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

State before:
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
⊢ of_fraction d a' b' ≤ of_fraction d a b
Tactic:
obtain ⟨m, ha, hb⟩ := Nat.proportional_of_mul_eq_mul_of_coprime h hc
State after:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
⊢ of_fraction d a' b' ≤ of_fraction d a b

State before:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
⊢ of_fraction d a' b' ≤ of_fraction d a b
Tactic:
have hmz : m ≠ 0 :=
  hab.elim (fun haz ↦ left_ne_zero_of_mul <| ha ▸ haz)
           (fun hbz ↦ left_ne_zero_of_mul <| hb ▸ hbz)
State after:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
⊢ of_fraction d a' b' ≤ of_fraction d a b

State before:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
⊢ of_fraction d a' b' ≤ of_fraction d a b
Tactic:
have hm : (1 : ℤ) ≤ m := Int.toNat_le.mp <| Nat.one_le_iff_ne_zero.mpr hmz
State after:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
⊢ of_fraction d a' b' ≤ of_fraction d a b

State before:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
⊢ of_fraction d a' b' ≤ of_fraction d a b
Tactic:
apply dom_of_pair_le
State after:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
⊢ ∀ (a_1 : ↑(testvecs 2 d)),
    0 ≤ pair' (of_fraction d a' b') (v a_1) → pair' (of_fraction d a' b') (v a_1) ≤ pair' (of_fraction d a b) (v a_1)

State before:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
⊢ ∀ (a_1 : ↑(testvecs 2 d)),
    0 ≤ pair' (of_fraction d a' b') (v a_1) → pair' (of_fraction d a' b') (v a_1) ≤ pair' (of_fraction d a b) (v a_1)
Tactic:
intro i hi
State after:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d a' b') (v i)
⊢ pair' (of_fraction d a' b') (v i) ≤ pair' (of_fraction d a b) (v i)

State before:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d a' b') (v i)
⊢ pair' (of_fraction d a' b') (v i) ≤ pair' (of_fraction d a b) (v i)
Tactic:
simp_rw [pair'_of_fraction] at hi ⊢
State after:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2)
⊢ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2) ≤ ↑a * v i 2 + ↑b * (v i 1 + v i 2)

State before:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2)
⊢ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2) ≤ ↑a * v i 2 + ↑b * (v i 1 + v i 2)
Tactic:
rw [ha, hb, Nat.cast_mul, Nat.cast_mul, mul_assoc, mul_assoc, ← mul_add]
State after:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2)
⊢ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2) ≤ ↑m * (↑a' * v i 2 + ↑b' * (v i 1 + v i 2))

State before:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2)
⊢ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2) ≤ ↑m * (↑a' * v i 2 + ↑b' * (v i 1 + v i 2))
Tactic:
exact le_mul_of_one_le_left hi hm
State after:
no goals