case refine'_1
α✝ : Type u
α : 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
α : 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
α : 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
α : 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)
α✝ : Type u
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ ↑(↑lift (f + g)) a = ↑(↑lift f) a + ↑(↑lift g) a
refine' FreeAbelianGroup.induction_on a _ _ _ _
no goals
case refine'_1
α✝ : Type u
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ ↑(↑lift (f + g)) 0 = ↑(↑lift f) 0 + ↑(↑lift g) 0
simp only [(lift _).map_zero, zero_add]
case refine'_2
α✝ : Type u
α : 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'_2
α✝ : Type u
α : 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)
intro x
no goals
case refine'_2
α✝ : Type u
α : 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)
simp only [lift.of, Pi.add_apply]
case refine'_3
α✝ : Type u
α : 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)
case refine'_3
α✝ : Type u
α : 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)
intro x _
no goals
case refine'_3
α✝ : Type u
α : 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)
simp only [map_neg, lift.of, Pi.add_apply, neg_add]
case refine'_4
α✝ : Type u
α : 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)
case refine'_4
α✝ : Type u
α : 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)
intro x y hx hy
no goals
case refine'_4
α✝ : Type u
α : 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)
simp only [(lift _).map_add, hx, hy, add_add_add_comm]