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

State before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
⊢ (∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂) ↔
    ∀ (a b : ℕ), mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
Tactic:
refine ⟨fun H a b h₁ h₂ ↦ ?_, fun H a b _ ↦ H a b⟩
State after:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
⊢ a * I.b₂ = b * I.a₂

State before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
⊢ a * I.b₂ = b * I.a₂
Tactic:
cases' Nat.eq_zero_or_pos (Nat.gcd a b) with h₀ h₀
State after:
case inl
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b = 0
⊢ a * I.b₂ = b * I.a₂

case inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b > 0
⊢ a * I.b₂ = b * I.a₂

State before:
case inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b > 0
⊢ a * I.b₂ = b * I.a₂
Tactic:
obtain ⟨g, a', b', hg₁, hcop, rfl, rfl⟩ := Nat.exists_coprime' h₀
State after:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
h₀ : Nat.gcd (a' * g) (b' * g) > 0
⊢ a' * g * I.b₂ = b' * g * I.a₂

State before:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
h₀ : Nat.gcd (a' * g) (b' * g) > 0
⊢ a' * g * I.b₂ = b' * g * I.a₂
Tactic:
clear h₀
State after:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ a' * g * I.b₂ = b' * g * I.a₂

State before:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ a' * g * I.b₂ = b' * g * I.a₂
Tactic:
simp_rw [mul_comm _ g, mul_assoc]
State after:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ g * (a' * I.b₂) = g * (b' * I.a₂)

State before:
case inl
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b = 0
⊢ a * I.b₂ = b * I.a₂
Tactic:
obtain ⟨rfl, rfl⟩ := Nat.gcd_eq_zero_iff.mp h₀
State after:
case inl.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
h₁ : mem_S_le d ↑0 ↑0
h₂ : mem 0 0 I
h₀ : Nat.gcd 0 0 = 0
⊢ 0 * I.b₂ = 0 * I.a₂

State before:
case inl.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
h₁ : mem_S_le d ↑0 ↑0
h₂ : mem 0 0 I
h₀ : Nat.gcd 0 0 = 0
⊢ 0 * I.b₂ = 0 * I.a₂
Tactic:
simp only [zero_mul]
State after:
no goals