Theorem: HTPI.list_elt_dvd_prod_by_length (HTPILib/Chap7.lean)

State before:
a : ℕ
⊢ ∀ (n : ℕ) (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
Tactic:
by_induc
State after:
case Base_Case
a : ℕ
⊢ ∀ (l : List ℕ), List.length l = 0 → a ∈ l → a ∣ prod l

case Induction_Step
a : ℕ
⊢ ∀ (n : ℕ),
    (∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l) →
      ∀ (l : List ℕ), List.length l = n + 1 → a ∈ l → a ∣ prod l

State before:
case Base_Case
a : ℕ
⊢ ∀ (l : List ℕ), List.length l = 0 → a ∈ l → a ∣ prod l
Tactic:
fix l : List Nat
State after:
case Base_Case
a : ℕ
l : List ℕ
⊢ List.length l = 0 → a ∈ l → a ∣ prod l

State before:
case Base_Case
a : ℕ
l : List ℕ
⊢ List.length l = 0 → a ∈ l → a ∣ prod l
Tactic:
assume h1 : l.length = 0
State after:
case Base_Case
a : ℕ
l : List ℕ
h1 : List.length l = 0
⊢ a ∈ l → a ∣ prod l

State before:
case Base_Case
a : ℕ
l : List ℕ
h1 : List.length l = 0
⊢ a ∈ l → a ∣ prod l
Tactic:
rewrite [List.length_eq_zero] at h1
State after:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ a ∈ l → a ∣ prod l

State before:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ a ∈ l → a ∣ prod l
Tactic:
rewrite [h1]
State after:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ a ∈ [] → a ∣ prod []

State before:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ a ∈ [] → a ∣ prod []
Tactic:
contrapos
State after:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ ¬a ∣ prod [] → a ∉ []

State before:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ ¬a ∣ prod [] → a ∉ []
Tactic:
assume h2 : ¬a ∣ prod []
State after:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
h2 : ¬a ∣ prod []
⊢ a ∉ []

State before:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
h2 : ¬a ∣ prod []
⊢ a ∉ []
Tactic:
show a ∉ [] from List.not_mem_nil a
State after:
no goals

State before:
case Induction_Step
a : ℕ
⊢ ∀ (n : ℕ),
    (∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l) →
      ∀ (l : List ℕ), List.length l = n + 1 → a ∈ l → a ∣ prod l
Tactic:
fix n : Nat
State after:
case Induction_Step
a n : ℕ
⊢ (∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l) → ∀ (l : List ℕ), List.length l = n + 1 → a ∈ l → a ∣ prod l

State before:
case Induction_Step
a n : ℕ
⊢ (∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l) → ∀ (l : List ℕ), List.length l = n + 1 → a ∈ l → a ∣ prod l
Tactic:
assume ih : ∀ (l : List Nat), List.length l = n → a ∈ l → a ∣ prod l
State after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
⊢ ∀ (l : List ℕ), List.length l = n + 1 → a ∈ l → a ∣ prod l

State before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
⊢ ∀ (l : List ℕ), List.length l = n + 1 → a ∈ l → a ∣ prod l
Tactic:
fix l : List Nat
State after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
⊢ List.length l = n + 1 → a ∈ l → a ∣ prod l

State before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
⊢ List.length l = n + 1 → a ∈ l → a ∣ prod l
Tactic:
assume h1 : l.length = n + 1
State after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
⊢ a ∈ l → a ∣ prod l

State before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
⊢ a ∈ l → a ∣ prod l
Tactic:
obtain (b : Nat) (h2 : ∃ (L : List Nat),
  l = b :: L ∧ L.length = n) from exists_cons_of_length_eq_succ h1
State after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
⊢ a ∈ l → a ∣ prod l

State before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
⊢ a ∈ l → a ∣ prod l
Tactic:
obtain (L : List Nat) (h3 : l = b :: L ∧ L.length = n) from h2
State after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
⊢ a ∈ l → a ∣ prod l

State before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
⊢ a ∈ l → a ∣ prod l
Tactic:
have h4 : a ∈ L → a ∣ prod L := ih L h3.right
State after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
⊢ a ∈ l → a ∣ prod l

State before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
⊢ a ∈ l → a ∣ prod l
Tactic:
assume h5 : a ∈ l
State after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ l
⊢ a ∣ prod l

State before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ l
⊢ a ∣ prod l
Tactic:
rewrite [h3.left, prod_cons]
State after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ l
⊢ a ∣ b * prod L

State before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ l
⊢ a ∣ b * prod L
Tactic:
rewrite [h3.left, List.mem_cons] at h5
State after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b ∨ a ∈ L
⊢ a ∣ b * prod L

State before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b ∨ a ∈ L
⊢ a ∣ b * prod L
Tactic:
by_cases on h5
State after:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ a ∣ b * prod L

case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
⊢ a ∣ b * prod L

State before:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ a ∣ b * prod L
Tactic:
apply Exists.intro (prod L)
State after:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ b * prod L = a * prod L

State before:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ b * prod L = a * prod L
Tactic:
rewrite [h5]
State after:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ b * prod L = b * prod L

State before:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ b * prod L = b * prod L
Tactic:
rfl
State after:
no goals

State before:
case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
⊢ a ∣ b * prod L
Tactic:
have h6 : a ∣ prod L := h4 h5
State after:
case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
⊢ a ∣ b * prod L

State before:
case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
⊢ a ∣ b * prod L
Tactic:
have h7 : prod L ∣ b * prod L := by
  apply Exists.intro b
  ring
  done
State after:
case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
h7 : prod L ∣ b * prod L
⊢ a ∣ b * prod L

State before:
case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
h7 : prod L ∣ b * prod L
⊢ a ∣ b * prod L
Tactic:
show a ∣ b * prod L from dvd_trans h6 h7
State after:
no goals

State before:
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
⊢ prod L ∣ b * prod L
Tactic:
apply Exists.intro b
State after:
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
⊢ b * prod L = prod L * b

State before:
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
⊢ b * prod L = prod L * b
Tactic:
ring
State after:
no goals