Theorem: List.ext'Iff (GMLInit/Data/List/Basic.lean)

State before:
α : Type u_1
as₁ as₂ : List α
⊢ All (as₁.ext'Aux as₂) ↔ as₁ = as₂
Tactic:
constructor
State after:
case mp
α : Type u_1
as₁ as₂ : List α
⊢ All (as₁.ext'Aux as₂) → as₁ = as₂

case mpr
α : Type u_1
as₁ as₂ : List α
⊢ as₁ = as₂ → All (as₁.ext'Aux as₂)

State before:
case mp
α : Type u_1
as₁ as₂ : List α
⊢ All (as₁.ext'Aux as₂) → as₁ = as₂

case mpr
α : Type u_1
as₁ as₂ : List α
⊢ as₁ = as₂ → All (as₁.ext'Aux as₂)
Tactic:
exact List.ext' as₁ as₂
State after:
case mpr
α : Type u_1
as₁ as₂ : List α
⊢ as₁ = as₂ → All (as₁.ext'Aux as₂)

State before:
case mpr
α : Type u_1
as₁ as₂ : List α
⊢ as₁ = as₂ → All (as₁.ext'Aux as₂)
Tactic:
intro h
State after:
case mpr
α : Type u_1
as₁ as₂ : List α
h : as₁ = as₂
⊢ All (as₁.ext'Aux as₂)

State before:
case mpr
α : Type u_1
as₁ as₂ : List α
h : as₁ = as₂
⊢ All (as₁.ext'Aux as₂)
Tactic:
cases h
State after:
case mpr.refl
α : Type u_1
as₁ : List α
⊢ All (as₁.ext'Aux as₁)

State before:
case mpr.refl
α : Type u_1
as₁ : List α
⊢ All (as₁.ext'Aux as₁)
Tactic:
induction as₁ with
| nil => exact All.nil
| cons _ _ H => exact All.cons rfl H
State after:
no goals

State before:
case mpr.refl.nil
α : Type u_1
⊢ All ([].ext'Aux [])
Tactic:
exact All.nil
State after:
no goals

State before:
case mpr.refl.cons
α : Type u_1
head✝ : α
tail✝ : List α
H : All (tail✝.ext'Aux tail✝)
⊢ All ((head✝ :: tail✝).ext'Aux (head✝ :: tail✝))
Tactic:
exact All.cons rfl H
State after:
no goals