-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dvd_gcd (xs : IntList) (c : Nat) (w : ∀ {a : Int}, a ∈ xs → (c : Int) ∣ a) :
    c ∣ xs.gcd

Proof state:
case cons.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ c ∣ gcd xs

Tactic:
apply ih

Result:
case cons.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ ∀ {a : Int}, a ∈ xs → c ∣ a.natAbs

Proof state:
case cons.a.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
b : Int
m : b ∈ xs
⊢ b ∈ x :: xs

Tactic:
exact List.mem_cons_of_mem x m

Result:
no goals

Proof state:
case nil
c : Nat
w : ∀ {a : Int}, a ∈ [] → c ∣ a.natAbs
this : c ∣ 0
⊢ c ∣ gcd []

Tactic:
exact this

Result:
no goals

Proof state:
case cons.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ c ∣ x.natAbs

Tactic:
apply w

Result:
case cons.a.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ x ∈ x :: xs

Proof state:
case nil
c : Nat
w : ∀ {a : Int}, a ∈ [] → c ∣ a.natAbs
⊢ c ∣ gcd []

Tactic:
have := Nat.dvd_zero c

Result:
case nil
c : Nat
w : ∀ {a : Int}, a ∈ [] → c ∣ a.natAbs
this : c ∣ 0
⊢ c ∣ gcd []

Proof state:
case cons.a.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ x ∈ x :: xs

Tactic:
simp

Result:
no goals

Proof state:
case cons
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ c ∣ gcd (x :: xs)

Tactic:
simp

Result:
case cons
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ c ∣ x.natAbs.gcd (gcd xs)

Proof state:
case cons
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ c ∣ x.natAbs.gcd (gcd xs)

Tactic:
apply Nat.dvd_gcd

Result:
case cons.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ c ∣ x.natAbs

case cons.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ c ∣ gcd xs

Proof state:
case cons.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
⊢ ∀ {a : Int}, a ∈ xs → c ∣ a.natAbs

Tactic:
intro b m

Result:
case cons.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
b : Int
m : b ∈ xs
⊢ c ∣ b.natAbs

Proof state:
xs : IntList
c : Nat
w : ∀ {a : Int}, a ∈ xs → ↑c ∣ a
⊢ c ∣ xs.gcd

Tactic:
simp only [Int.ofNat_dvd_left] at w

Result:
xs : IntList
c : Nat
w : ∀ {a : Int}, a ∈ xs → c ∣ a.natAbs
⊢ c ∣ xs.gcd

Proof state:
case cons.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
b : Int
m : b ∈ xs
⊢ c ∣ b.natAbs

Tactic:
apply w

Result:
case cons.a.a
c : Nat
x : Int
xs : List Int
ih : (∀ {a : Int}, a ∈ xs → c ∣ a.natAbs) → c ∣ gcd xs
w : ∀ {a : Int}, a ∈ x :: xs → c ∣ a.natAbs
b : Int
m : b ∈ xs
⊢ b ∈ x :: xs