Theorem: Weight.BasicInterval.coprime (Weights/BasicInterval.lean)

State before:
I : BasicInterval
⊢ Nat.Coprime (I.a₂ * I.b₁) (I.a₁ * I.b₂)
Tactic:
rw [Nat.Coprime, Nat.gcd_eq_iff]
State after:
I : BasicInterval
⊢ 1 ∣ I.a₂ * I.b₁ ∧ 1 ∣ I.a₁ * I.b₂ ∧ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c ∣ 1

State before:
I : BasicInterval
⊢ 1 ∣ I.a₂ * I.b₁ ∧ 1 ∣ I.a₁ * I.b₂ ∧ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c ∣ 1
Tactic:
simp? says simp only [isUnit_one, IsUnit.dvd, Nat.isUnit_iff, Nat.dvd_one, true_and]
State after:
I : BasicInterval
⊢ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c = 1

State before:
I : BasicInterval
⊢ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c = 1
Tactic:
intros c h₁ h₂
State after:
I : BasicInterval
c : ℕ
h₁ : c ∣ I.a₂ * I.b₁
h₂ : c ∣ I.a₁ * I.b₂
⊢ c = 1

State before:
I : BasicInterval
c : ℕ
h₁ : c ∣ I.a₂ * I.b₁
h₂ : c ∣ I.a₁ * I.b₂
⊢ c = 1
Tactic:
rw [I.rel] at h₁
State after:
I : BasicInterval
c : ℕ
h₁ : c ∣ I.a₁ * I.b₂ + 1
h₂ : c ∣ I.a₁ * I.b₂
⊢ c = 1

State before:
I : BasicInterval
c : ℕ
h₁ : c ∣ I.a₁ * I.b₂ + 1
h₂ : c ∣ I.a₁ * I.b₂
⊢ c = 1
Tactic:
exact Nat.dvd_one.mp <| (Nat.dvd_add_right h₂).mp h₁
State after:
no goals

State before:
I : BasicInterval
⊢ 1 ∣ I.a₂ * I.b₁ ∧ 1 ∣ I.a₁ * I.b₂ ∧ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c ∣ 1
Tactic:
simp only [isUnit_one, IsUnit.dvd, Nat.isUnit_iff, Nat.dvd_one, true_and]
State after:
I : BasicInterval
⊢ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c = 1