-- Mathlib/GroupTheory/FreeAbelianGroup.lean
theorem lift.add' {α β} [AddCommGroup β] (a : FreeAbelianGroup α) (f g : α → β) :
    lift (f + g) a = lift f a + lift g a

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ ∀ (x : α), (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x)

Tactic:
intro x

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
x : α
⊢ (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x)

Proof state:
case refine_4
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
x y : FreeAbelianGroup α
hx : (lift (f + g)) x = (lift f) x + (lift g) x
hy : (lift (f + g)) y = (lift f) y + (lift g) y
⊢ (lift (f + g)) (x + y) = (lift f) (x + y) + (lift g) (x + y)

Tactic:
simp only [(lift _).map_add, hx, hy, add_add_add_comm]

Result:
no goals

Proof state:
case refine_4
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ ∀ (x y : FreeAbelianGroup α),
    (lift (f + g)) x = (lift f) x + (lift g) x →
      (lift (f + g)) y = (lift f) y + (lift g) y → (lift (f + g)) (x + y) = (lift f) (x + y) + (lift g) (x + y)

Tactic:
intro x y hx hy

Result:
case refine_4
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
x y : FreeAbelianGroup α
hx : (lift (f + g)) x = (lift f) x + (lift g) x
hy : (lift (f + g)) y = (lift f) y + (lift g) y
⊢ (lift (f + g)) (x + y) = (lift f) (x + y) + (lift g) (x + y)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
x : α
⊢ (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x)

Tactic:
simp only [lift.of, Pi.add_apply]

Result:
no goals

Proof state:
case refine_3
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ ∀ (x : α),
    (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x) →
      (lift (f + g)) (-of x) = (lift f) (-of x) + (lift g) (-of x)

Tactic:
intro x _

Result:
case refine_3
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
x : α
a✝ : (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x)
⊢ (lift (f + g)) (-of x) = (lift f) (-of x) + (lift g) (-of x)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ (lift (f + g)) 0 = (lift f) 0 + (lift g) 0

Tactic:
simp only [(lift _).map_zero, zero_add]

Result:
no goals

Proof state:
case refine_3
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
x : α
a✝ : (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x)
⊢ (lift (f + g)) (-of x) = (lift f) (-of x) + (lift g) (-of x)

Tactic:
simp only [map_neg, lift.of, Pi.add_apply, neg_add]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ (lift (f + g)) a = (lift f) a + (lift g) a

Tactic:
refine FreeAbelianGroup.induction_on a ?_ ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ (lift (f + g)) 0 = (lift f) 0 + (lift g) 0

case refine_2
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ ∀ (x : α), (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x)

case refine_3
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ ∀ (x : α),
    (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x) →
      (lift (f + g)) (-of x) = (lift f) (-of x) + (lift g) (-of x)

case refine_4
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ ∀ (x y : FreeAbelianGroup α),
    (lift (f + g)) x = (lift f) x + (lift g) x →
      (lift (f + g)) y = (lift f) y + (lift g) y → (lift (f + g)) (x + y) = (lift f) (x + y) + (lift g) (x + y)