-- Mathlib/Data/List/Sigma.lean
theorem kerase_kerase {a a'} {l : List (Sigma β)} :
    (kerase a' l).kerase a = (kerase a l).kerase a'

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)

Tactic:
subst a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ kerase a (kerase a l) = kerase a (kerase a l)

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
subst a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
h : ¬a = x.fst
tail_ih✝ : kerase a (kerase x.fst xs) = kerase x.fst (kerase a xs)
⊢ kerase a (kerase x.fst (x :: xs)) = kerase x.fst (kerase a (x :: xs))

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a' : α
x : Sigma β
xs : List (Sigma β)
h✝ : ¬a' = x.fst
h : ¬x.fst = a'
tail_ih✝ : kerase x.fst (kerase a' xs) = kerase a' (kerase x.fst xs)
⊢ kerase x.fst (kerase a' (x :: xs)) = kerase a' (kerase x.fst (x :: xs))

Tactic:
simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
by_cases h' : a = x.1

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
h' : a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
h' : ¬a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Proof state:
case neg.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
⊢ kerase a (kerase a' []) = kerase a' (kerase a [])

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
h' : a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
subst a

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a' : α
x : Sigma β
xs : List (Sigma β)
h✝ : ¬a' = x.fst
h : ¬x.fst = a'
tail_ih✝ : kerase x.fst (kerase a' xs) = kerase a' (kerase x.fst xs)
⊢ kerase x.fst (kerase a' (x :: xs)) = kerase a' (kerase x.fst (x :: xs))

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ kerase a (kerase a l) = kerase a (kerase a l)

Tactic:
rfl

Result:
no goals

Proof state:
case neg.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
by_cases a' = x.1

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
h : ¬a = x.fst
tail_ih✝ : kerase a (kerase x.fst xs) = kerase x.fst (kerase a xs)
⊢ kerase a (kerase x.fst (x :: xs)) = kerase x.fst (kerase a (x :: xs))

Tactic:
simp [kerase_cons_ne h, kerase_cons_eq rfl]

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : ¬a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)

Tactic:
induction' l with x xs

Result:
case neg.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
⊢ kerase a (kerase a' []) = kerase a' (kerase a [])

case neg.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
h' : ¬a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
simp [kerase_cons_ne, *]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)

Tactic:
by_cases h : a = a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : ¬a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)