Theorem: Imo1989P5.coprime_of_product (Compfiles/Imo1989P5.lean)

State before:
n : ℕ
lst : List ℕ
h : ∀ y ∈ lst, n.Coprime y
⊢ n.Coprime lst.prod
Tactic:
induction lst with
| nil => simp only [List.prod_nil, Nat.coprime_one_right_eq_true]
| cons x xs ih =>
  have hy : ∀ (y : ℕ), y ∈ xs → Nat.Coprime n y :=
    fun y hy ↦ h y (List.mem_cons.mpr (Or.inr hy))
  have h1 := h x (by simp)
  rw [List.prod_cons]
  exact Nat.Coprime.mul_right h1 (ih hy)
State after:
no goals

State before:
case nil
n : ℕ
h : ∀ y ∈ [], n.Coprime y
⊢ n.Coprime [].prod
Tactic:
simp only [List.prod_nil, Nat.coprime_one_right_eq_true]
State after:
no goals

State before:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
⊢ n.Coprime (x :: xs).prod
Tactic:
have hy : ∀ (y : ℕ), y ∈ xs → Nat.Coprime n y :=
  fun y hy ↦ h y (List.mem_cons.mpr (Or.inr hy))
State after:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
⊢ n.Coprime (x :: xs).prod

State before:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
⊢ n.Coprime (x :: xs).prod
Tactic:
have h1 := h x (by simp)
State after:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
h1 : n.Coprime x
⊢ n.Coprime (x :: xs).prod

State before:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
h1 : n.Coprime x
⊢ n.Coprime (x :: xs).prod
Tactic:
rw [List.prod_cons]
State after:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
h1 : n.Coprime x
⊢ n.Coprime (x * xs.prod)

State before:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
h1 : n.Coprime x
⊢ n.Coprime (x * xs.prod)
Tactic:
exact Nat.Coprime.mul_right h1 (ih hy)
State after:
no goals

State before:
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
⊢ x ∈ x :: xs
Tactic:
simp
State after:
no goals