import Mathlib.Algebra.GroupPower.Lemmas
import Mathlib.Algebra.Group.Prod
import Mathlib.Data.Int.Cast.Lemmas
import Mathlib.Algebra.Ring.Basic
import UnitConjecture.EnumDecide

/-!

## Free groups

The definition of a free group on a basis, along with a few properties.

Free groups are defined constructively to allow automatic equality checking of 
homomorphisms on finitely generated free groups.

## Overview
- `AddFreeGroup` - the main definition.
- `decideHomsEqual` - the crucial result that allows the 
  automatic comparison of homomorphisms by checking their values on the basis.
- `ℤFree` - a proof that the additive group of integers is a free group on the one-element type.
- `prodFree` - a proof that the product of free groups is free.
-/

/-- Free (Additive) Groups, implemented as a typeclass.
    A free additive group with a basis `X` is an additive group `F` with an inclusion map `ι : X → F`,
    such that any map `f : X → A` from the basis to any Abelian group `A`
    extends *uniquely* to an *additive group homomorphism* `φ : F →+ A`. -/
class AddFreeGroup: {F : Type u_1} →
  [inst : AddCommGroup F] →
    {X : Type u_2} →
      (ι : X → F) →
        (inducedHom : (A : Type) → [inst_1 : AddCommGroup A] → (X → A) → F →+ A) →
          (∀ {A : Type} [inst_1 : AddCommGroup A] (f : X → A), ↑(inducedHom A f) ∘ ι = f) →
            (∀ {A : Type} [inst_1 : AddCommGroup A] (f g : F →+ A), ↑f ∘ ι = ↑g ∘ ι → f = g) → AddFreeGroup F X
AddFreeGroup (F: Type ?u.2
F : Type _: Type (?u.2+1)
Type _) [AddCommGroup: Type ?u.5 → Type ?u.5
AddCommGroup F: Type ?u.2
F] (X: Type ?u.8
X : Type _: Type (?u.8+1)
Type _) where
  /-- The inclusion map from the basis to the free group. -/
  ι: {F : Type u_1} → [inst : AddCommGroup F] → {X : Type u_2} → [self : AddFreeGroup F X] → X → F
ι : X: Type ?u.8
X → F: Type ?u.2
F
  /-- The homomorphism from the free group induced by a map from the basis. -/
  inducedHom: {F : Type u_1} →
  [inst : AddCommGroup F] →
    {X : Type u_2} → [self : AddFreeGroup F X] → (A : Type) → [inst_1 : AddCommGroup A] → (X → A) → F →+ A
inducedHom : (A: Type
A : Type: Type 1
Type) → [AddCommGroup: Type ?u.21 → Type ?u.21
AddCommGroup A: Type
A] → (X: Type ?u.8
X → A: Type
A) → (F: Type ?u.2
F →+ A: Type
A)
  /-- A proof that the induced homomorphism extends the map from the basis. -/
  induced_extends: ∀ {F : Type u_1} [inst : AddCommGroup F] {X : Type u_2} [self : AddFreeGroup F X] {A : Type} [inst_1 : AddCommGroup A]
  (f : X → A), ↑(AddFreeGroup.inducedHom A f) ∘ AddFreeGroup.ι = f
induced_extends {A: Type
A : Type: Type 1
Type} [AddCommGroup: Type ?u.464 → Type ?u.464
AddCommGroup A: Type
A] : ∀ f: X → A
f : X: Type ?u.8
X → A: Type
A, (inducedHom: (A : Type) → [inst : AddCommGroup A] → (X → A) → F →+ A
inducedHom A: Type
A f: X → A
f) ∘ ι: X → F
ι = f: X → A
f
  /-- A proof that any homomorphism extending a map from the basis must be unique. -/
  unique_extension: ∀ {F : Type u_1} [inst : AddCommGroup F] {X : Type u_2} [self : AddFreeGroup F X] {A : Type} [inst_1 : AddCommGroup A]
  (f g : F →+ A), ↑f ∘ AddFreeGroup.ι = ↑g ∘ AddFreeGroup.ι → f = g
unique_extension {A: Type
A : Type: Type 1
Type} [AddCommGroup: Type ?u.1275 → Type ?u.1275
AddCommGroup A: Type
A] (f: F →+ A
f g: F →+ A
g : F: Type ?u.2
F →+ A: Type
A) : f: F →+ A
f ∘ ι: X → F
ι = g: F →+ A
g ∘ ι: X → F
ι → f: F →+ A
f = g: F →+ A
g


/-- The additive group of integers `ℤ` is the free group on a singleton basis. -/
instance ℤFree: AddFreeGroup ℤ Unit
ℤFree : AddFreeGroup: (F : Type ?u.3359) → [inst : AddCommGroup F] → Type ?u.3358 → Type (max(max1?u.3359)?u.3358)
AddFreeGroup ℤ: Type
ℤ Unit: Type
Unit where
  ι := fun _: ?m.3377
_ => 1: ?m.3380
1
  inducedHom := fun A: ?m.3393
A _: ?m.3396
_ f: ?m.3399
f => (zmultiplesHom: (A : Type ?u.3402) → [inst : AddGroup A] → A ≃ (ℤ →+ A)
zmultiplesHom A: ?m.3393
A).toFun: {α : Sort ?u.3485} → {β : Sort ?u.3484} → α ≃ β → α → β
toFun (f: ?m.3399
f (): Unit
())
  induced_extends := by
    
∀ {A : Type} [inst : AddCommGroup A] (f : Unit → A),
  (↑((fun A x f => Equiv.toFun (zmultiplesHom A) (f ())) A inst f) ∘ fun x => 1) = fintro A: Type
A _: AddCommGroup A
_ f: Unit → A
fA: Type

inst✝: AddCommGroup A

f: Unit → A

(↑((fun A x f => Equiv.toFun (zmultiplesHom A) (f ())) A inst✝ f) ∘ fun x => 1) = f
    
∀ {A : Type} [inst : AddCommGroup A] (f : Unit → A),
  (↑((fun A x f => Equiv.toFun (zmultiplesHom A) (f ())) A inst f) ∘ fun x => 1) = ffunext u: ?α
uA: Type

inst✝: AddCommGroup A

f: Unit → A

u: Unit

hFunction.comp (↑((fun A x f => Equiv.toFun (zmultiplesHom A) (f ())) A inst✝ f)) (fun x => 1) u = f u;A: Type

inst✝: AddCommGroup A

f: Unit → A

u: Unit

hFunction.comp (↑((fun A x f => Equiv.toFun (zmultiplesHom A) (f ())) A inst✝ f)) (fun x => 1) u = f u 
∀ {A : Type} [inst : AddCommGroup A] (f : Unit → A),
  (↑((fun A x f => Equiv.toFun (zmultiplesHom A) (f ())) A inst f) ∘ fun x => 1) = fcases u: ?α
uA: Type

inst✝: AddCommGroup A

f: Unit → A

h.unitFunction.comp (↑((fun A x f => Equiv.toFun (zmultiplesHom A) (f ())) A inst✝ f)) (fun x => 1) PUnit.unit = f PUnit.unit
    
∀ {A : Type} [inst : AddCommGroup A] (f : Unit → A),
  (↑((fun A x f => Equiv.toFun (zmultiplesHom A) (f ())) A inst f) ∘ fun x => 1) = fsimp [one_zsmul: ∀ {G : Type ?u.3590} [inst : SubNegMonoid G] (a : G), 1 • a = a
one_zsmul]
Goals accomplished! 🐙
  unique_extension := by
    
∀ {A : Type} [inst : AddCommGroup A] (f g : ℤ →+ A), ((↑f ∘ fun x => 1) = ↑g ∘ fun x => 1) → f = gintro A: Type
A abg: AddCommGroup A
abg f: ℤ →+ A
f g: ℤ →+ A
g hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1
hypA: Type

abg: AddCommGroup A

f, g: ℤ →+ A

hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1

f = g
    
∀ {A : Type} [inst : AddCommGroup A] (f g : ℤ →+ A), ((↑f ∘ fun x => 1) = ↑g ∘ fun x => 1) → f = glet hyp': ?m.6070
hyp' := congrFun: ∀ {α : Sort ?u.6072} {β : α → Sort ?u.6071} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congrFun hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1
hyp (): Unit
()A: Type

abg: AddCommGroup A

f, g: ℤ →+ A

hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1

hyp':= congrFun hyp (): Function.comp (↑f) (fun x => 1) () = Function.comp (↑g) (fun x => 1) ()

f = g
    
∀ {A : Type} [inst : AddCommGroup A] (f g : ℤ →+ A), ((↑f ∘ fun x => 1) = ↑g ∘ fun x => 1) → f = gdsimp at hyp': ?m.6070
hyp'A: Type

abg: AddCommGroup A

f, g: ℤ →+ A

hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1

hyp':= congrFun hyp (): ↑f 1 = ↑g 1

f = g
    
∀ {A : Type} [inst : AddCommGroup A] (f g : ℤ →+ A), ((↑f ∘ fun x => 1) = ↑g ∘ fun x => 1) → f = grwa [A: Type

abg: AddCommGroup A

f, g: ℤ →+ A

hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1

hyp':= congrFun hyp (): ↑f 1 = ↑g 1

f = g← zmultiplesHom_symm_apply: ∀ {A : Type ?u.6132} [inst : AddGroup A] (f : ℤ →+ A), ↑(Equiv.symm (zmultiplesHom A)) f = ↑f 1
zmultiplesHom_symm_apply,A: Type

abg: AddCommGroup A

f, g: ℤ →+ A

hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1

hyp': ↑(Equiv.symm (zmultiplesHom A)) f = ↑g 1

f = g A: Type

abg: AddCommGroup A

f, g: ℤ →+ A

hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1

hyp':= congrFun hyp (): ↑f 1 = ↑g 1

f = g← zmultiplesHom_symm_apply: ∀ {A : Type ?u.6271} [inst : AddGroup A] (f : ℤ →+ A), ↑(Equiv.symm (zmultiplesHom A)) f = ↑f 1
zmultiplesHom_symm_apply,A: Type

abg: AddCommGroup A

f, g: ℤ →+ A

hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1

hyp': ↑(Equiv.symm (zmultiplesHom A)) f = ↑(Equiv.symm (zmultiplesHom A)) g

f = g A: Type

abg: AddCommGroup A

f, g: ℤ →+ A

hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1

hyp':= congrFun hyp (): ↑f 1 = ↑g 1

f = gEquiv.apply_eq_iff_eq: ∀ {α : Sort ?u.6439} {β : Sort ?u.6438} (f : α ≃ β) {x y : α}, ↑f x = ↑f y ↔ x = y
Equiv.apply_eq_iff_eqA: Type

abg: AddCommGroup A

f, g: ℤ →+ A

hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1

hyp': f = g

f = g]A: Type

abg: AddCommGroup A

f, g: ℤ →+ A

hyp: (↑f ∘ fun x => 1) = ↑g ∘ fun x => 1

hyp': f = g

f = g at hyp': ↑(Equiv.symm (zmultiplesHom A)) f = ↑(Equiv.symm (zmultiplesHom A)) g
hyp'
Goals accomplished! 🐙


open EnumDecide in
/-- Equality of homomorphisms from a free group on an exhaustively searchable basis is decidable. -/
@[instance] def decideHomsEqual: {F : Type ?u.6984} →
  [inst : AddCommGroup F] →
    {X : Type ?u.6990} →
      [inst_1 : DecideForall X] →
        [fgp : AddFreeGroup F X] →
          {A : Type ?u.7008} → [inst_2 : AddCommGroup A] → [inst_3 : DecidableEq A] → DecidableEq (F →+ A)
decideHomsEqual {F: Type ?u.6984
F : Type _: Type (?u.6984+1)
Type _} [AddCommGroup: Type ?u.6987 → Type ?u.6987
AddCommGroup F: Type ?u.6984
F] {X: Type ?u.6990
X : Type _: Type (?u.6990+1)
Type _} [DecideForall: Type ?u.6993 → Type ?u.6993
DecideForall X: Type ?u.6990
X] [fgp: AddFreeGroup F X
fgp : AddFreeGroup: (F : Type ?u.6997) → [inst : AddCommGroup F] → Type ?u.6996 → Type (max(max1?u.6997)?u.6996)
AddFreeGroup F: Type ?u.6984
F X: Type ?u.6990
X] 
    {A: Type ?u.7008
A : Type _: Type (?u.7008+1)
Type _} [AddCommGroup: Type ?u.7011 → Type ?u.7011
AddCommGroup A: Type ?u.7008
A] [DecidableEq: Sort ?u.7014 → Sort (max1?u.7014)
DecidableEq A: Type ?u.7008
A] : DecidableEq: Sort ?u.7023 → Sort (max1?u.7023)
DecidableEq (F: Type ?u.6984
F →+ A: Type ?u.7008
A) := fun f: ?m.7478
f g: ?m.7481
g =>
  if c: ?m.9157
c : ∀ x: X
x : X: Type ?u.6990
X, f: ?m.7478
f (fgp: AddFreeGroup F X
fgp.ι: {F : Type ?u.8274} → [inst : AddCommGroup F] → {X : Type ?u.8273} → [self : AddFreeGroup F X] → X → F
ι x: X
x) = g: ?m.7481
g (fgp: AddFreeGroup F X
fgp.ι: {F : Type ?u.9052} → [inst : AddCommGroup F] → {X : Type ?u.9051} → [self : AddFreeGroup F X] → X → F
ι x: X
x) then by
    F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type ?u.7008

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

Decidable (f = g)apply Decidable.isTrue: {p : Prop} → p → Decidable p
Decidable.isTrueF: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type ?u.7008

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

hf = g
    F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type ?u.7008

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

Decidable (f = g)apply fgp: AddFreeGroup F X
fgp.unique_extension: ∀ {F : Type ?u.9175} [inst : AddCommGroup F] {X : Type ?u.9174} [self : AddFreeGroup F X] {A : Type}
  [inst_1 : AddCommGroup A] (f g : F →+ A), ↑f ∘ AddFreeGroup.ι = ↑g ∘ AddFreeGroup.ι → f = g
unique_extensionF: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

h.a↑f ∘ AddFreeGroup.ι = ↑g ∘ AddFreeGroup.ι
    F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type ?u.7008

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

Decidable (f = g)funext x: ?α
xF: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

x: X

h.a.hFunction.comp (↑f) AddFreeGroup.ι x = Function.comp (↑g) AddFreeGroup.ι x
    F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type ?u.7008

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

Decidable (f = g)exact c: ∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)
c x: ?α
x
Goals accomplished! 🐙
  else by
    F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

Decidable (f = g)apply Decidable.isFalse: {p : Prop} → ¬p → Decidable p
Decidable.isFalseF: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

h¬f = g
    F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

Decidable (f = g)intro contra: f = g
contraF: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

contra: f = g

hFalse
    F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

Decidable (f = g)let c': ∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)
c' : ∀ (x: X
x : X: Type ?u.6990
X), f: F →+ A
f (fgp: AddFreeGroup F X
fgp.ι: {F : Type ?u.10051} → [inst : AddCommGroup F] → {X : Type ?u.10050} → [self : AddFreeGroup F X] → X → F
ι x: X
x) = g: F →+ A
g (fgp: AddFreeGroup F X
fgp.ι: {F : Type ?u.10824} → [inst : AddCommGroup F] → {X : Type ?u.10823} → [self : AddFreeGroup F X] → X → F
ι x: X
x) := F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

contra: f = g

hFalseby
      F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

contra: f = g

∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)introF: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

contra: f = g

x✝: X

↑f (AddFreeGroup.ι x✝) = ↑g (AddFreeGroup.ι x✝);F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

contra: f = g

x✝: X

↑f (AddFreeGroup.ι x✝) = ↑g (AddFreeGroup.ι x✝) F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

contra: f = g

∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)apply congrFun: ∀ {α : Sort ?u.10842} {β : α → Sort ?u.10841} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congrFun (congrArg: ∀ {α : Sort ?u.10848} {β : Sort ?u.10847} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congrArg _: ?m.10849 → ?m.10850
_ contra: f = g
contra)
Goals accomplished! 🐙
    F: Type ?u.6984

inst✝³: AddCommGroup F

X: Type ?u.6990

inst✝²: DecideForall X

fgp: AddFreeGroup F X

A: Type

inst✝¹: AddCommGroup A

inst✝: DecidableEq A

f, g: F →+ A

c: ¬∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x)

Decidable (f = g)contradiction
Goals accomplished! 🐙

namespace AddFreeGroup.Product

variable {A: Type ?u.14585
A B: Type ?u.11319
B : Type _: Type (?u.12604+1)
Type _} [AddCommGroup: Type ?u.11322 → Type ?u.11322
AddCommGroup A: Type ?u.11328
A] [AddCommGroup: Type ?u.11355 → Type ?u.11355
AddCommGroup B: Type ?u.14588
B]
variable {X_A: Type ?u.11358
X_A X_B: Type ?u.14600
X_B : Type _: Type (?u.11358+1)
Type _}
variable [FAb_A: AddFreeGroup A X_A
FAb_A : AddFreeGroup: (F : Type ?u.11365) → [inst : AddCommGroup F] → Type ?u.11364 → Type (max(max1?u.11365)?u.11364)
AddFreeGroup A: Type ?u.11346
A X_A: Type ?u.11358
X_A] [FAb_B: AddFreeGroup B X_B
FAb_B : AddFreeGroup: (F : Type ?u.11377) → [inst : AddCommGroup F] → Type ?u.11376 → Type (max(max1?u.11377)?u.11376)
AddFreeGroup B: Type ?u.12604
B X_B: Type ?u.11361
X_B]

/-- The inclusion map from the direct sum of the bases of two free groups into their product. -/
def ι: X_A ⊕ X_B → A × B
ι : (X_A: Type ?u.11400
X_A ⊕ X_B: Type ?u.11403
X_B) → A: Type ?u.11388
A × B: Type ?u.11391
B
  | Sum.inl: {α : Type ?u.11441} → {β : Type ?u.11440} → α → α ⊕ β
Sum.inl x_a: X_A
x_a => (FAb_A: AddFreeGroup A X_A
FAb_A.ι: {F : Type ?u.11467} → [inst : AddCommGroup F] → {X : Type ?u.11466} → [self : AddFreeGroup F X] → X → F
ι x_a: X_A
x_a, 0: ?m.11482
0)
  | Sum.inr: {α : Type ?u.11833} → {β : Type ?u.11832} → β → α ⊕ β
Sum.inr x_b: X_B
x_b => (0: ?m.11855
0, FAb_B: AddFreeGroup B X_B
FAb_B.ι: {F : Type ?u.12204} → [inst : AddCommGroup F] → {X : Type ?u.12203} → [self : AddFreeGroup F X] → X → F
ι x_b: X_B
x_b)

/-- The group homomorphism from the product of two free groups induced by a map from the basis. -/
def inducedProdHom: (G : Type ?u.12643) → [inst : AddCommGroup G] → (X_A ⊕ X_B → G) → A × B →+ G
inducedProdHom (G: Type ?u.12643
G : Type _: Type (?u.12643+1)
Type _) [AddCommGroup: Type ?u.12646 → Type ?u.12646
AddCommGroup G: Type ?u.12643
G] (f: X_A ⊕ X_B → G
f : X_A: Type ?u.12613
X_A ⊕ X_B: Type ?u.12616
X_B → G: Type ?u.12643
G) : A: Type ?u.12601
A × B: Type ?u.12604
B →+ G: Type ?u.12643
G :=
    let f_A: X_A → G
f_A : X_A: Type ?u.12613
X_A → G: Type ?u.12643
G := f: X_A ⊕ X_B → G
f ∘ Sum.inl: {α : Type ?u.13332} → {β : Type ?u.13331} → α → α ⊕ β
Sum.inl
    let f_B: X_B → G
f_B : X_B: Type ?u.12616
X_B → G: Type ?u.12643
G := f: X_A ⊕ X_B → G
f ∘ Sum.inr: {α : Type ?u.13359} → {β : Type ?u.13358} → β → α ⊕ β
Sum.inr
    AddMonoidHom.coprod: {M : Type ?u.13371} →
  {N : Type ?u.13370} →
    {P : Type ?u.13369} →
      [inst : AddZeroClass M] →
        [inst_1 : AddZeroClass N] → [inst_2 : AddCommMonoid P] → (M →+ P) → (N →+ P) → M × N →+ P
AddMonoidHom.coprod 
      (FAb_A: AddFreeGroup A X_A
FAb_A.inducedHom: {F : Type ?u.13712} →
  [inst : AddCommGroup F] →
    {X : Type ?u.13711} → [self : AddFreeGroup F X] → (A : Type) → [inst_1 : AddCommGroup A] → (X → A) → F →+ A
inducedHom G: Type ?u.12643
G f_A: X_A → G
f_A) 
      (FAb_B: AddFreeGroup B X_B
FAb_B.inducedHom: {F : Type ?u.13762} →
  [inst : AddCommGroup F] →
    {X : Type ?u.13761} → [self : AddFreeGroup F X] → (A : Type) → [inst_1 : AddCommGroup A] → (X → A) → F →+ A
inducedHom G: Type ?u.12643
G f_B: X_B → G
f_B)

/-- The product of free groups is free. -/
instance prodFree: AddFreeGroup (A × B) (X_A ⊕ X_B)
prodFree : AddFreeGroup: (F : Type ?u.14628) → [inst : AddCommGroup F] → Type ?u.14627 → Type (max(max1?u.14628)?u.14627)
AddFreeGroup (A: Type ?u.14585
A × B: Type ?u.14588
B) (X_A: Type ?u.14597
X_A ⊕ X_B: Type ?u.14600
X_B)  :=
  {
    ι := ι: {A : Type ?u.14696} →
  {B : Type ?u.14695} →
    [inst : AddCommGroup A] →
      [inst_1 : AddCommGroup B] →
        {X_A : Type ?u.14694} →
          {X_B : Type ?u.14693} → [FAb_A : AddFreeGroup A X_A] → [FAb_B : AddFreeGroup B X_B] → X_A ⊕ X_B → A × B
ι
    inducedHom := inducedProdHom: {A : Type ?u.14775} →
  {B : Type ?u.14774} →
    [inst : AddCommGroup A] →
      [inst_1 : AddCommGroup B] →
        {X_A : Type ?u.14773} →
          {X_B : Type ?u.14772} →
            [FAb_A : AddFreeGroup A X_A] →
              [FAb_B : AddFreeGroup B X_B] → (G : Type) → [inst_2 : AddCommGroup G] → (X_A ⊕ X_B → G) → A × B →+ G
inducedProdHom
    induced_extends := by
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f : X_A ⊕ X_B → A_1), ↑(inducedProdHom A_1 f) ∘ ι = fintro _: Type
_ _: AddCommGroup A✝
_ f: X_A ⊕ X_B → A✝
fA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

↑(inducedProdHom A✝ f) ∘ ι = f
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f : X_A ⊕ X_B → A_1), ↑(inducedProdHom A_1 f) ∘ ι = ffunext x: ?α
xA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

x: X_A ⊕ X_B

hFunction.comp (↑(inducedProdHom A✝ f)) ι x = f x;A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

x: X_A ⊕ X_B

hFunction.comp (↑(inducedProdHom A✝ f)) ι x = f x A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f : X_A ⊕ X_B → A_1), ↑(inducedProdHom A_1 f) ∘ ι = fcases x: ?α
xA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

val✝: X_A

h.inlFunction.comp (↑(inducedProdHom A✝ f)) ι (Sum.inl val✝) = f (Sum.inl val✝)
A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

val✝: X_B

h.inrFunction.comp (↑(inducedProdHom A✝ f)) ι (Sum.inr val✝) = f (Sum.inr val✝) A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

x: X_A ⊕ X_B

hFunction.comp (↑(inducedProdHom A✝ f)) ι x = f x<;>A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

val✝: X_A

h.inlFunction.comp (↑(inducedProdHom A✝ f)) ι (Sum.inl val✝) = f (Sum.inl val✝)
A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

val✝: X_B

h.inrFunction.comp (↑(inducedProdHom A✝ f)) ι (Sum.inr val✝) = f (Sum.inr val✝) A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

x: X_A ⊕ X_B

hFunction.comp (↑(inducedProdHom A✝ f)) ι x = f xsimp [inducedProdHom: {A : Type ?u.15023} →
  {B : Type ?u.15022} →
    [inst : AddCommGroup A] →
      [inst_1 : AddCommGroup B] →
        {X_A : Type ?u.15021} →
          {X_B : Type ?u.15020} →
            [FAb_A : AddFreeGroup A X_A] →
              [FAb_B : AddFreeGroup B X_B] → (G : Type) → [inst_2 : AddCommGroup G] → (X_A ⊕ X_B → G) → A × B →+ G
inducedProdHom, ι: {A : Type ?u.15028} →
  {B : Type ?u.15027} →
    [inst : AddCommGroup A] →
      [inst_1 : AddCommGroup B] →
        {X_A : Type ?u.15026} →
          {X_B : Type ?u.15025} → [FAb_A : AddFreeGroup A X_A] → [FAb_B : AddFreeGroup B X_B] → X_A ⊕ X_B → A × B
ι]A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

val✝: X_B

h.inr↑(inducedHom A✝ (f ∘ Sum.inr)) (AddFreeGroup.ι val✝) = f (Sum.inr val✝)
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f : X_A ⊕ X_B → A_1), ↑(inducedProdHom A_1 f) ∘ ι = f· A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

val✝: X_A

h.inl↑(inducedHom A✝ (f ∘ Sum.inl)) (AddFreeGroup.ι val✝) = f (Sum.inl val✝)
A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

val✝: X_B

h.inr↑(inducedHom A✝ (f ∘ Sum.inr)) (AddFreeGroup.ι val✝) = f (Sum.inr val✝)apply congrFun: ∀ {α : Sort ?u.21873} {β : α → Sort ?u.21872} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congrFun <| FAb_A: AddFreeGroup A X_A
FAb_A.induced_extends: ∀ {F : Type ?u.21879} [inst : AddCommGroup F] {X : Type ?u.21878} [self : AddFreeGroup F X] {A : Type}
  [inst_1 : AddCommGroup A] (f : X → A), ↑(inducedHom A f) ∘ AddFreeGroup.ι = f
induced_extends (f: X_A ⊕ X_B → A✝
f ∘ Sum.inl: {α : Type ?u.21900} → {β : Type ?u.21899} → α → α ⊕ β
Sum.inl)
Goals accomplished! 🐙
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f : X_A ⊕ X_B → A_1), ↑(inducedProdHom A_1 f) ∘ ι = f· A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f: X_A ⊕ X_B → A✝

val✝: X_B

h.inr↑(inducedHom A✝ (f ∘ Sum.inr)) (AddFreeGroup.ι val✝) = f (Sum.inr val✝)apply congrFun: ∀ {α : Sort ?u.21957} {β : α → Sort ?u.21956} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congrFun <| FAb_B: AddFreeGroup B X_B
FAb_B.induced_extends: ∀ {F : Type ?u.21963} [inst : AddCommGroup F] {X : Type ?u.21962} [self : AddFreeGroup F X] {A : Type}
  [inst_1 : AddCommGroup A] (f : X → A), ↑(inducedHom A f) ∘ AddFreeGroup.ι = f
induced_extends (f: X_A ⊕ X_B → A✝
f ∘ Sum.inr: {α : Type ?u.21984} → {β : Type ?u.21983} → β → α ⊕ β
Sum.inr)
Goals accomplished! 🐙
    unique_extension := by
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f g : A × B →+ A_1), ↑f ∘ ι = ↑g ∘ ι → f = gintro _: Type
_ _: AddCommGroup A✝
_ f: A × B →+ A✝
f g: A × B →+ A✝
g hyp: ↑f ∘ ι = ↑g ∘ ι
hypA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

f = g
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f g : A × B →+ A_1), ↑f ∘ ι = ↑g ∘ ι → f = gext ⟨a, b⟩: ?M
⟨a: A
a⟨a, b⟩: ?M
, b: B
b⟨a, b⟩: ?M
⟩A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

h.mk↑f (a, b) = ↑g (a, b)
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f g : A × B →+ A_1), ↑f ∘ ι = ↑g ∘ ι → f = grw [A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

h.mk↑f (a, b) = ↑g (a, b)show (a: A
a, b: B
b) = (a: A
a, 0: ?m.22629
0) + (0: ?m.22643
0, b: B
b) by A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

h.mk↑f (a, b) = ↑g (a, b)simp
Goals accomplished! 🐙,A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

h.mk↑f ((a, 0) + (0, b)) = ↑g ((a, 0) + (0, b)) A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

h.mk↑f (a, b) = ↑g (a, b)map_add: ∀ {M : Type ?u.25062} {N : Type ?u.25063} {F : Type ?u.25061} [inst : Add M] [inst_1 : Add N]
  [inst_2 : AddHomClass F M N] (f : F) (x y : M), ↑f (x + y) = ↑f x + ↑f y
map_add,A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

h.mk↑f (a, 0) + ↑f (0, b) = ↑g ((a, 0) + (0, b)) A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

h.mk↑f (a, b) = ↑g (a, b)map_add: ∀ {M : Type ?u.26112} {N : Type ?u.26113} {F : Type ?u.26111} [inst : Add M] [inst_1 : Add N]
  [inst_2 : AddHomClass F M N] (f : F) (x y : M), ↑f (x + y) = ↑f x + ↑f y
map_addA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

h.mk↑f (a, 0) + ↑f (0, b) = ↑g (a, 0) + ↑g (0, b)]A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

h.mk↑f (a, 0) + ↑f (0, b) = ↑g (a, 0) + ↑g (0, b)
      
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f g : A × B →+ A_1), ↑f ∘ ι = ↑g ∘ ι → f = ghave A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)
A_unique : f: A × B →+ A✝
f.comp: {M : Type ?u.27242} →
  {N : Type ?u.27241} →
    {P : Type ?u.27240} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp (.inl: (M : Type ?u.27262) → (N : Type ?u.27261) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M →+ M × N
.inl A: Type ?u.14585
A B: Type ?u.14588
B) = g: A × B →+ A✝
g.comp: {M : Type ?u.28265} →
  {N : Type ?u.28264} →
    {P : Type ?u.28263} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp (.inl: (M : Type ?u.28281) → (N : Type ?u.28280) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M →+ M × N
.inl A: Type ?u.14585
A B: Type ?u.14588
B) := A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

h.mk↑f (a, 0) + ↑f (0, b) = ↑g (a, 0) + ↑g (0, b)by
        A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)apply FAb_A: AddFreeGroup A X_A
FAb_A.unique_extension: ∀ {F : Type ?u.29121} [inst : AddCommGroup F] {X : Type ?u.29120} [self : AddFreeGroup F X] {A : Type}
  [inst_1 : AddCommGroup A] (f g : F →+ A), ↑f ∘ AddFreeGroup.ι = ↑g ∘ AddFreeGroup.ι → f = g
unique_extensionA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

a↑(AddMonoidHom.comp f (AddMonoidHom.inl A B)) ∘ AddFreeGroup.ι =   ↑(AddMonoidHom.comp g (AddMonoidHom.inl A B)) ∘ AddFreeGroup.ι;A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

a↑(AddMonoidHom.comp f (AddMonoidHom.inl A B)) ∘ AddFreeGroup.ι =   ↑(AddMonoidHom.comp g (AddMonoidHom.inl A B)) ∘ AddFreeGroup.ι A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)funext x_A: ?α
x_AA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

x_A: X_A

a.hFunction.comp (↑(AddMonoidHom.comp f (AddMonoidHom.inl A B))) AddFreeGroup.ι x_A =   Function.comp (↑(AddMonoidHom.comp g (AddMonoidHom.inl A B))) AddFreeGroup.ι x_A;A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

x_A: X_A

a.hFunction.comp (↑(AddMonoidHom.comp f (AddMonoidHom.inl A B))) AddFreeGroup.ι x_A =   Function.comp (↑(AddMonoidHom.comp g (AddMonoidHom.inl A B))) AddFreeGroup.ι x_A A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)apply congrFun: ∀ {α : Sort ?u.29198} {β : α → Sort ?u.29197} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congrFun hyp: ↑f ∘ ι = ↑g ∘ ι
hyp (Sum.inl: {α : Type ?u.29215} → {β : Type ?u.29214} → α → α ⊕ β
Sum.inl x_A: ?α
x_A)
Goals accomplished! 🐙
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f g : A × B →+ A_1), ↑f ∘ ι = ↑g ∘ ι → f = ghave B_unique: AddMonoidHom.comp f (AddMonoidHom.inr A B) = AddMonoidHom.comp g (AddMonoidHom.inr A B)
B_unique : f: A × B →+ A✝
f.comp: {M : Type ?u.29269} →
  {N : Type ?u.29268} →
    {P : Type ?u.29267} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp (.inr: (M : Type ?u.29285) → (N : Type ?u.29284) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → N →+ M × N
.inr A: Type ?u.14585
A B: Type ?u.14588
B) = g: A × B →+ A✝
g.comp: {M : Type ?u.30288} →
  {N : Type ?u.30287} →
    {P : Type ?u.30286} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp (.inr: (M : Type ?u.30304) → (N : Type ?u.30303) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → N →+ M × N
.inr A: Type ?u.14585
A B: Type ?u.14588
B) := A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

h.mk↑f (a, 0) + ↑f (0, b) = ↑g (a, 0) + ↑g (0, b)by
        A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

AddMonoidHom.comp f (AddMonoidHom.inr A B) = AddMonoidHom.comp g (AddMonoidHom.inr A B)apply FAb_B: AddFreeGroup B X_B
FAb_B.unique_extension: ∀ {F : Type ?u.31144} [inst : AddCommGroup F] {X : Type ?u.31143} [self : AddFreeGroup F X] {A : Type}
  [inst_1 : AddCommGroup A] (f g : F →+ A), ↑f ∘ AddFreeGroup.ι = ↑g ∘ AddFreeGroup.ι → f = g
unique_extensionA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

a↑(AddMonoidHom.comp f (AddMonoidHom.inr A B)) ∘ AddFreeGroup.ι =   ↑(AddMonoidHom.comp g (AddMonoidHom.inr A B)) ∘ AddFreeGroup.ι;A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

a↑(AddMonoidHom.comp f (AddMonoidHom.inr A B)) ∘ AddFreeGroup.ι =   ↑(AddMonoidHom.comp g (AddMonoidHom.inr A B)) ∘ AddFreeGroup.ι A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

AddMonoidHom.comp f (AddMonoidHom.inr A B) = AddMonoidHom.comp g (AddMonoidHom.inr A B)funext x_B: ?α
x_BA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

x_B: X_B

a.hFunction.comp (↑(AddMonoidHom.comp f (AddMonoidHom.inr A B))) AddFreeGroup.ι x_B =   Function.comp (↑(AddMonoidHom.comp g (AddMonoidHom.inr A B))) AddFreeGroup.ι x_B;A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

x_B: X_B

a.hFunction.comp (↑(AddMonoidHom.comp f (AddMonoidHom.inr A B))) AddFreeGroup.ι x_B =   Function.comp (↑(AddMonoidHom.comp g (AddMonoidHom.inr A B))) AddFreeGroup.ι x_B A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

AddMonoidHom.comp f (AddMonoidHom.inr A B) = AddMonoidHom.comp g (AddMonoidHom.inr A B)apply congrFun: ∀ {α : Sort ?u.31219} {β : α → Sort ?u.31218} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congrFun hyp: ↑f ∘ ι = ↑g ∘ ι
hyp (Sum.inr: {α : Type ?u.31233} → {β : Type ?u.31232} → β → α ⊕ β
Sum.inr x_B: ?α
x_B)
Goals accomplished! 🐙
   
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f g : A × B →+ A_1), ↑f ∘ ι = ↑g ∘ ι → f = gshow f: A × B →+ A✝
f.comp: {M : Type ?u.31276} →
  {N : Type ?u.31275} →
    {P : Type ?u.31274} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp (.inl: (M : Type ?u.31292) → (N : Type ?u.31291) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M →+ M × N
.inl _: Type ?u.31292
_ _: Type ?u.31291
_) a: A
a + f: A × B →+ A✝
f.comp: {M : Type ?u.33435} →
  {N : Type ?u.33434} →
    {P : Type ?u.33433} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp (.inr: (M : Type ?u.33451) → (N : Type ?u.33450) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → N →+ M × N
.inr _: Type ?u.33451
_ _: Type ?u.33450
_) b: B
b =
           g: A × B →+ A✝
g.comp: {M : Type ?u.35414} →
  {N : Type ?u.35413} →
    {P : Type ?u.35412} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp (.inl: (M : Type ?u.35430) → (N : Type ?u.35429) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M →+ M × N
.inl _: Type ?u.35430
_ _: Type ?u.35429
_) a: A
a + g: A × B →+ A✝
g.comp: {M : Type ?u.37389} →
  {N : Type ?u.37388} →
    {P : Type ?u.37387} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp (.inr: (M : Type ?u.37405) → (N : Type ?u.37404) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → N →+ M × N
.inr _: Type ?u.37405
_ _: Type ?u.37404
_) b: B
bA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

B_unique: AddMonoidHom.comp f (AddMonoidHom.inr A B) = AddMonoidHom.comp g (AddMonoidHom.inr A B)

h.mk↑(AddMonoidHom.comp f (AddMonoidHom.inl A B)) a + ↑(AddMonoidHom.comp f (AddMonoidHom.inr A B)) b =   ↑(AddMonoidHom.comp g (AddMonoidHom.inl A B)) a + ↑(AddMonoidHom.comp g (AddMonoidHom.inr A B)) b 
      A: Type ?u.14585

B: Type ?u.14588

inst✝¹: AddCommGroup A

inst✝: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

∀ {A_1 : Type} [inst : AddCommGroup A_1] (f g : A × B →+ A_1), ↑f ∘ ι = ↑g ∘ ι → f = grw [A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

B_unique: AddMonoidHom.comp f (AddMonoidHom.inr A B) = AddMonoidHom.comp g (AddMonoidHom.inr A B)

h.mk↑(AddMonoidHom.comp f (AddMonoidHom.inl A B)) a + ↑(AddMonoidHom.comp f (AddMonoidHom.inr A B)) b =   ↑(AddMonoidHom.comp g (AddMonoidHom.inl A B)) a + ↑(AddMonoidHom.comp g (AddMonoidHom.inr A B)) bA_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)
A_unique,A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

B_unique: AddMonoidHom.comp f (AddMonoidHom.inr A B) = AddMonoidHom.comp g (AddMonoidHom.inr A B)

h.mk↑(AddMonoidHom.comp g (AddMonoidHom.inl A B)) a + ↑(AddMonoidHom.comp f (AddMonoidHom.inr A B)) b =   ↑(AddMonoidHom.comp g (AddMonoidHom.inl A B)) a + ↑(AddMonoidHom.comp g (AddMonoidHom.inr A B)) b A: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

B_unique: AddMonoidHom.comp f (AddMonoidHom.inr A B) = AddMonoidHom.comp g (AddMonoidHom.inr A B)

h.mk↑(AddMonoidHom.comp f (AddMonoidHom.inl A B)) a + ↑(AddMonoidHom.comp f (AddMonoidHom.inr A B)) b =   ↑(AddMonoidHom.comp g (AddMonoidHom.inl A B)) a + ↑(AddMonoidHom.comp g (AddMonoidHom.inr A B)) bB_unique: AddMonoidHom.comp f (AddMonoidHom.inr A B) = AddMonoidHom.comp g (AddMonoidHom.inr A B)
B_uniqueA: Type ?u.14585

B: Type ?u.14588

inst✝²: AddCommGroup A

inst✝¹: AddCommGroup B

X_A: Type ?u.14597

X_B: Type ?u.14600

FAb_A: AddFreeGroup A X_A

FAb_B: AddFreeGroup B X_B

A✝: Type

inst✝: AddCommGroup A✝

f, g: A × B →+ A✝

hyp: ↑f ∘ ι = ↑g ∘ ι

a: A

b: B

A_unique: AddMonoidHom.comp f (AddMonoidHom.inl A B) = AddMonoidHom.comp g (AddMonoidHom.inl A B)

B_unique: AddMonoidHom.comp f (AddMonoidHom.inr A B) = AddMonoidHom.comp g (AddMonoidHom.inr A B)

h.mk↑(AddMonoidHom.comp g (AddMonoidHom.inl A B)) a + ↑(AddMonoidHom.comp g (AddMonoidHom.inr A B)) b =   ↑(AddMonoidHom.comp g (AddMonoidHom.inl A B)) a + ↑(AddMonoidHom.comp g (AddMonoidHom.inr A B)) b]
Goals accomplished! 🐙
  }
  
end AddFreeGroup.Product