Theorem: GcdLinearCombination (NazgandLean4/IntegerInduction.lean)

State before:
k₀ k₁ : ℤ
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
obtain ⟨m, n, h⟩ := IsBezout.gcd_eq_sum k₀ k₁
State after:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁

State before:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
have := associated_gcd_gcd k₀ k₁
State after:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
this : Associated (IsBezout.gcd k₀ k₁) (GCDMonoid.gcd k₀ k₁)
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁

State before:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
this : Associated (IsBezout.gcd k₀ k₁) (GCDMonoid.gcd k₀ k₁)
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
rw [Int.associated_iff] at this
State after:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
this : IsBezout.gcd k₀ k₁ = GCDMonoid.gcd k₀ k₁ ∨ IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁

State before:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
this : IsBezout.gcd k₀ k₁ = GCDMonoid.gcd k₀ k₁ ∨ IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
cases this with
| inl h' =>
  use m, n
  rw [h, Int.coe_gcd, h']
| inr h' =>
  use -m, -n
  rw [Int.coe_gcd]
  linarith
State after:
no goals

State before:
case intro.intro.inl
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = GCDMonoid.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
use m, n
State after:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = GCDMonoid.gcd k₀ k₁
⊢ ↑(k₀.gcd k₁) = m * k₀ + n * k₁

State before:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = GCDMonoid.gcd k₀ k₁
⊢ ↑(k₀.gcd k₁) = m * k₀ + n * k₁
Tactic:
rw [h, Int.coe_gcd, h']
State after:
no goals

State before:
case intro.intro.inr
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
use -m, -n
State after:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ ↑(k₀.gcd k₁) = -m * k₀ + -n * k₁

State before:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ ↑(k₀.gcd k₁) = -m * k₀ + -n * k₁
Tactic:
rw [Int.coe_gcd]
State after:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ GCDMonoid.gcd k₀ k₁ = -m * k₀ + -n * k₁

State before:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ GCDMonoid.gcd k₀ k₁ = -m * k₀ + -n * k₁
Tactic:
linarith
State after:
no goals