case C0
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ↑(↑lift (g ∘ f)) 0 = ↑(↑lift g) (↑(map f) 0)

case C1
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ∀ (x : α), ↑(↑lift (g ∘ f)) (of x) = ↑(↑lift g) (↑(map f) (of x))

case Cn
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ∀ (x : α),
    ↑(↑lift (g ∘ f)) (of x) = ↑(↑lift g) (↑(map f) (of x)) → ↑(↑lift (g ∘ f)) (-of x) = ↑(↑lift g) (↑(map f) (-of x))

case Cp
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ∀ (x y : FreeAbelianGroup α),
    ↑(↑lift (g ∘ f)) x = ↑(↑lift g) (↑(map f) x) →
      ↑(↑lift (g ∘ f)) y = ↑(↑lift g) (↑(map f) y) → ↑(↑lift (g ∘ f)) (x + y) = ↑(↑lift g) (↑(map f) (x + y))
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ↑(↑lift (g ∘ f)) x = ↑(↑lift g) (↑(map f) x)
apply FreeAbelianGroup.induction_on (C := fun x ↦ lift (g ∘ f) x = lift g (map f x)) x
no goals
case C0
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ↑(↑lift (g ∘ f)) 0 = ↑(↑lift g) (↑(map f) 0)
simp only [map_zero]
case C1
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
x✝ : α
⊢ ↑(↑lift (g ∘ f)) (of x✝) = ↑(↑lift g) (↑(map f) (of x✝))
case C1
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ∀ (x : α), ↑(↑lift (g ∘ f)) (of x) = ↑(↑lift g) (↑(map f) (of x))
intro _
no goals
case C1
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
x✝ : α
⊢ ↑(↑lift (g ∘ f)) (of x✝) = ↑(↑lift g) (↑(map f) (of x✝))
simp only [lift.of, map, Function.comp]
case Cn
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
x✝ : α
h : ↑(↑lift (g ∘ f)) (of x✝) = ↑(↑lift g) (↑(map f) (of x✝))
⊢ ↑(↑lift (g ∘ f)) (-of x✝) = ↑(↑lift g) (↑(map f) (-of x✝))
case Cn
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ∀ (x : α),
    ↑(↑lift (g ∘ f)) (of x) = ↑(↑lift g) (↑(map f) (of x)) → ↑(↑lift (g ∘ f)) (-of x) = ↑(↑lift g) (↑(map f) (-of x))
intro _ h
no goals
case Cn
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
x✝ : α
h : ↑(↑lift (g ∘ f)) (of x✝) = ↑(↑lift g) (↑(map f) (of x✝))
⊢ ↑(↑lift (g ∘ f)) (-of x✝) = ↑(↑lift g) (↑(map f) (-of x✝))
simp only [h, AddMonoidHom.map_neg]
case Cp
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x x✝ y✝ : FreeAbelianGroup α
h₁ : ↑(↑lift (g ∘ f)) x✝ = ↑(↑lift g) (↑(map f) x✝)
h₂ : ↑(↑lift (g ∘ f)) y✝ = ↑(↑lift g) (↑(map f) y✝)
⊢ ↑(↑lift (g ∘ f)) (x✝ + y✝) = ↑(↑lift g) (↑(map f) (x✝ + y✝))
case Cp
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ∀ (x y : FreeAbelianGroup α),
    ↑(↑lift (g ∘ f)) x = ↑(↑lift g) (↑(map f) x) →
      ↑(↑lift (g ∘ f)) y = ↑(↑lift g) (↑(map f) y) → ↑(↑lift (g ∘ f)) (x + y) = ↑(↑lift g) (↑(map f) (x + y))
intro _ _ h₁ h₂
no goals
case Cp
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x x✝ y✝ : FreeAbelianGroup α
h₁ : ↑(↑lift (g ∘ f)) x✝ = ↑(↑lift g) (↑(map f) x✝)
h₂ : ↑(↑lift (g ∘ f)) y✝ = ↑(↑lift g) (↑(map f) y✝)
⊢ ↑(↑lift (g ∘ f)) (x✝ + y✝) = ↑(↑lift g) (↑(map f) (x✝ + y✝))
simp only [h₁, h₂, AddMonoidHom.map_add]