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

State before:
a : ℕ
l : List ℕ
h : a ∈ l
⊢ a ∣ prod l
Tactic:
set n : Nat := l.length
State after:
a : ℕ
l : List ℕ
h : a ∈ l
n : ℕ := List.length l
⊢ a ∣ prod l

State before:
a : ℕ
l : List ℕ
h : a ∈ l
n : ℕ := List.length l
⊢ a ∣ prod l
Tactic:
have h1 : l.length = n := by rfl
State after:
a : ℕ
l : List ℕ
h : a ∈ l
n : ℕ := List.length l
h1 : List.length l = n
⊢ a ∣ prod l

State before:
a : ℕ
l : List ℕ
h : a ∈ l
n : ℕ := List.length l
h1 : List.length l = n
⊢ a ∣ prod l
Tactic:
show a ∣ prod l from list_elt_dvd_prod_by_length a n l h1 h
State after:
no goals

State before:
a : ℕ
l : List ℕ
h : a ∈ l
n : ℕ := List.length l
⊢ List.length l = n
Tactic:
rfl
State after:
no goals