[GOAL]
α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
⊢ ↑(↑lift f) (of x) = f x
[PROOFSTEP]
convert Abelianization.lift.of (FreeGroup.lift f (β := Multiplicative β)) (FreeGroup.of x) using 1
[GOAL]
case h.e'_3.h
α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
e_1✝ : (fun x => β) (of x) = (fun x => Multiplicative β) (↑Abelianization.of (FreeGroup.of x))
⊢ f x = ↑(↑FreeGroup.lift f) (FreeGroup.of x)
[PROOFSTEP]
exact (FreeGroup.lift.of (β := Multiplicative β)).symm
[GOAL]
α✝ : Type u
β✝ : Type v
inst✝² : AddCommGroup β✝
f✝ : α✝ → β✝
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ ↑g (↑(↑lift f) a) = ↑(↑lift (↑g ∘ f)) a
[PROOFSTEP]
show (g.comp (lift f)) a = lift (g ∘ f) a
[GOAL]
α✝ : Type u
β✝ : Type v
inst✝² : AddCommGroup β✝
f✝ : α✝ → β✝
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ ↑(AddMonoidHom.comp g (↑lift f)) a = ↑(↑lift (↑g ∘ f)) a
[PROOFSTEP]
apply lift.unique
[GOAL]
case hg
α✝ : Type u
β✝ : Type v
inst✝² : AddCommGroup β✝
f✝ : α✝ → β✝
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ ∀ (x : α), ↑(AddMonoidHom.comp g (↑lift f)) (of x) = (↑g ∘ f) x
[PROOFSTEP]
intro a
[GOAL]
case hg
α✝ : Type u
β✝ : Type v
inst✝² : AddCommGroup β✝
f✝ : α✝ → β✝
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a✝ : FreeAbelianGroup α
f : α → β
g : β →+ γ
a : α
⊢ ↑(AddMonoidHom.comp g (↑lift f)) (of a) = (↑g ∘ f) a
[PROOFSTEP]
show g ((lift f) (of a)) = g (f a)
[GOAL]
case hg
α✝ : Type u
β✝ : Type v
inst✝² : AddCommGroup β✝
f✝ : α✝ → β✝
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a✝ : FreeAbelianGroup α
f : α → β
g : β →+ γ
a : α
⊢ ↑g (↑(↑lift f) (of a)) = ↑g (f a)
[PROOFSTEP]
simp only [(· ∘ ·), lift.of]
[GOAL]
α✝ : Type u
α : Type u_1
β : Type u_2
inst✝ : AddCommGroup β
a : FreeAbelianGroup α
f g : α → β
⊢ ↑(↑lift (f + g)) a = ↑(↑lift f) a + ↑(↑lift g) a
[PROOFSTEP]
refine' FreeAbelianGroup.induction_on a _ _ _ _
[GOAL]
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
[PROOFSTEP]
simp only [(lift _).map_zero, zero_add]
[GOAL]
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)
[PROOFSTEP]
intro x
[GOAL]
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)
[PROOFSTEP]
simp only [lift.of, Pi.add_apply]
[GOAL]
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)
[PROOFSTEP]
intro x _
[GOAL]
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)
[PROOFSTEP]
simp only [map_neg, lift.of, Pi.add_apply, neg_add]
[GOAL]
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)
[PROOFSTEP]
intro x y hx hy
[GOAL]
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)
[PROOFSTEP]
simp only [(lift _).map_add, hx, hy, add_add_add_comm]
[GOAL]
α β : Type u
f : FreeAbelianGroup (α → β)
x y : FreeAbelianGroup α
⊢ ↑(↑lift fun x_1 => x_1 <$> (x + y)) f =
    (fun x x_1 => Seq.seq x fun x => x_1) f x + (fun x x_1 => Seq.seq x fun x => x_1) f y
[PROOFSTEP]
simp only [FreeAbelianGroup.map_add]
[GOAL]
α β : Type u
f : FreeAbelianGroup (α → β)
x y : FreeAbelianGroup α
⊢ ↑(↑lift fun x_1 => x_1 <$> x + x_1 <$> y) f = (Seq.seq f fun x_1 => x) + Seq.seq f fun x => y
[PROOFSTEP]
exact lift.add' f _ _
[GOAL]
α β α✝ : Type u
x✝ : FreeAbelianGroup α✝
x : α✝
ih : id <$> pure x = pure x
⊢ id <$> (-pure x) = -pure x
[PROOFSTEP]
rw [FreeAbelianGroup.map_neg, ih]
[GOAL]
α β α✝ : Type u
x✝ x y : FreeAbelianGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ id <$> (x + y) = x + y
[PROOFSTEP]
rw [FreeAbelianGroup.map_add, ihx, ihy]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
⊢ 0 >>= f >>= g = 0 >>= fun x => f x >>= g
[PROOFSTEP]
iterate 3 rw [zero_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
⊢ 0 >>= f >>= g = 0 >>= fun x => f x >>= g
[PROOFSTEP]
rw [zero_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
⊢ 0 >>= g = 0 >>= fun x => f x >>= g
[PROOFSTEP]
rw [zero_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
⊢ 0 = 0 >>= fun x => f x >>= g
[PROOFSTEP]
rw [zero_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
⊢ pure x >>= f >>= g = pure x >>= fun x => f x >>= g
[PROOFSTEP]
iterate 2 rw [pure_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
⊢ pure x >>= f >>= g = pure x >>= fun x => f x >>= g
[PROOFSTEP]
rw [pure_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
⊢ f x >>= g = pure x >>= fun x => f x >>= g
[PROOFSTEP]
rw [pure_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x => f x >>= g
⊢ -pure x >>= f >>= g = -pure x >>= fun x => f x >>= g
[PROOFSTEP]
iterate 3 rw [neg_bind] <;> try rw [ih]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x => f x >>= g
⊢ -pure x >>= f >>= g = -pure x >>= fun x => f x >>= g
[PROOFSTEP]
rw [neg_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x => f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x => f x >>= g
[PROOFSTEP]
try rw [ih]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x => f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x => f x >>= g
[PROOFSTEP]
rw [ih]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x => f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x => f x >>= g
[PROOFSTEP]
rw [neg_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x => f x >>= g
⊢ -(pure x >>= f >>= g) = -pure x >>= fun x => f x >>= g
[PROOFSTEP]
try rw [ih]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x => f x >>= g
⊢ -(pure x >>= f >>= g) = -pure x >>= fun x => f x >>= g
[PROOFSTEP]
rw [ih]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x => f x >>= g
⊢ -(pure x >>= fun x => f x >>= g) = -pure x >>= fun x => f x >>= g
[PROOFSTEP]
rw [neg_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x => f x >>= g
ihy : y >>= f >>= g = y >>= fun x => f x >>= g
⊢ x + y >>= f >>= g = x + y >>= fun x => f x >>= g
[PROOFSTEP]
iterate 3 rw [add_bind] <;> try rw [ihx, ihy]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x => f x >>= g
ihy : y >>= f >>= g = y >>= fun x => f x >>= g
⊢ x + y >>= f >>= g = x + y >>= fun x => f x >>= g
[PROOFSTEP]
rw [add_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x => f x >>= g
ihy : y >>= f >>= g = y >>= fun x => f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x => f x >>= g
[PROOFSTEP]
try rw [ihx, ihy]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x => f x >>= g
ihy : y >>= f >>= g = y >>= fun x => f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x => f x >>= g
[PROOFSTEP]
rw [ihx, ihy]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x => f x >>= g
ihy : y >>= f >>= g = y >>= fun x => f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x => f x >>= g
[PROOFSTEP]
rw [add_bind]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x => f x >>= g
ihy : y >>= f >>= g = y >>= fun x => f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun x => f x >>= g
[PROOFSTEP]
try rw [ihx, ihy]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x => f x >>= g
ihy : y >>= f >>= g = y >>= fun x => f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun x => f x >>= g
[PROOFSTEP]
rw [ihx, ihy]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x => f x >>= g
ihy : y >>= f >>= g = y >>= fun x => f x >>= g
⊢ (x >>= fun x => f x >>= g) + (y >>= fun x => f x >>= g) = x + y >>= fun x => f x >>= g
[PROOFSTEP]
rw [add_bind]
[GOAL]
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
⊢ (Seq.seq (Prod.mk <$> x) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x_1 => x
[PROOFSTEP]
refine' FreeAbelianGroup.induction_on' x _ _ _ _
[GOAL]
case refine'_1
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
⊢ (Seq.seq (Prod.mk <$> 0) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x => 0
[PROOFSTEP]
rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]
[GOAL]
case refine'_2
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
⊢ ∀ (x : α✝), (Seq.seq (Prod.mk <$> pure x) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x_1 => pure x
[PROOFSTEP]
intro p
[GOAL]
case refine'_2
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
p : α✝
⊢ (Seq.seq (Prod.mk <$> pure p) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x => pure p
[PROOFSTEP]
rw [map_pure, pure_seq]
[GOAL]
case refine'_2
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
p : α✝
⊢ Prod.mk p <$> y = Seq.seq ((fun b a => (a, b)) <$> y) fun x => pure p
[PROOFSTEP]
exact
  FreeAbelianGroup.induction_on' y (by rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq])
    (fun q ↦ by rw [map_pure, map_pure, pure_seq, map_pure])
    (fun q ih ↦ by rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]) fun y₁ y₂ ih1 ih2 ↦ by
    rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
[GOAL]
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
p : α✝
⊢ Prod.mk p <$> 0 = Seq.seq ((fun b a => (a, b)) <$> 0) fun x => pure p
[PROOFSTEP]
rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]
[GOAL]
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
p : α✝
q : β✝
⊢ Prod.mk p <$> pure q = Seq.seq ((fun b a => (a, b)) <$> pure q) fun x => pure p
[PROOFSTEP]
rw [map_pure, map_pure, pure_seq, map_pure]
[GOAL]
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
p : α✝
q : β✝
ih : Prod.mk p <$> pure q = Seq.seq ((fun b a => (a, b)) <$> pure q) fun x => pure p
⊢ Prod.mk p <$> (-pure q) = Seq.seq ((fun b a => (a, b)) <$> (-pure q)) fun x => pure p
[PROOFSTEP]
rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
[GOAL]
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
p : α✝
y₁ y₂ : FreeAbelianGroup β✝
ih1 : Prod.mk p <$> y₁ = Seq.seq ((fun b a => (a, b)) <$> y₁) fun x => pure p
ih2 : Prod.mk p <$> y₂ = Seq.seq ((fun b a => (a, b)) <$> y₂) fun x => pure p
⊢ Prod.mk p <$> (y₁ + y₂) = Seq.seq ((fun b a => (a, b)) <$> (y₁ + y₂)) fun x => pure p
[PROOFSTEP]
rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
[GOAL]
case refine'_3
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
⊢ ∀ (x : α✝),
    ((Seq.seq (Prod.mk <$> pure x) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x_1 => pure x) →
      (Seq.seq (Prod.mk <$> (-pure x)) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x_1 => -pure x
[PROOFSTEP]
intro p ih
[GOAL]
case refine'_3
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
p : α✝
ih : (Seq.seq (Prod.mk <$> pure p) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x => pure p
⊢ (Seq.seq (Prod.mk <$> (-pure p)) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x => -pure p
[PROOFSTEP]
rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
[GOAL]
case refine'_4
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
⊢ ∀ (x y_1 : FreeAbelianGroup α✝),
    ((Seq.seq (Prod.mk <$> x) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x_1 => x) →
      ((Seq.seq (Prod.mk <$> y_1) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x => y_1) →
        (Seq.seq (Prod.mk <$> (x + y_1)) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x_1 => x + y_1
[PROOFSTEP]
intro x₁ x₂ ih1 ih2
[GOAL]
case refine'_4
α β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
x₁ x₂ : FreeAbelianGroup α✝
ih1 : (Seq.seq (Prod.mk <$> x₁) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x => x₁
ih2 : (Seq.seq (Prod.mk <$> x₂) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x => x₂
⊢ (Seq.seq (Prod.mk <$> (x₁ + x₂)) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> y) fun x => x₁ + x₂
[PROOFSTEP]
rw [FreeAbelianGroup.map_add, add_seq, seq_add, ih1, ih2]
[GOAL]
α✝ : 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)
[PROOFSTEP]
apply FreeAbelianGroup.induction_on (C := fun x ↦ lift (g ∘ f) x = lift g (map f x)) x
[GOAL]
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)
[PROOFSTEP]
simp only [map_zero]
[GOAL]
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))
[PROOFSTEP]
intro _
[GOAL]
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✝))
[PROOFSTEP]
simp only [lift.of, map, Function.comp]
[GOAL]
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))
[PROOFSTEP]
intro _ h
[GOAL]
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✝))
[PROOFSTEP]
simp only [h, AddMonoidHom.map_neg]
[GOAL]
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))
[PROOFSTEP]
intro _ _ h₁ h₂
[GOAL]
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✝))
[PROOFSTEP]
simp only [h₁, h₂, AddMonoidHom.map_add]
[GOAL]
α : Type u
β : Type v
γ : Type w
x : FreeAbelianGroup α
⊢ ↑(map id) x = x
[PROOFSTEP]
rw [map_id]
[GOAL]
α : Type u
β : Type v
γ : Type w
x : FreeAbelianGroup α
⊢ ↑(AddMonoidHom.id (FreeAbelianGroup α)) x = x
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x✝ : α
⊢ ↑(AddMonoidHom.comp (map g) (map f)) (of x✝) = ↑(map (g ∘ f)) (of x✝)
[PROOFSTEP]
simp [map]
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ↑(map (g ∘ f)) x = ↑(map g) (↑(map f) x)
[PROOFSTEP]
rw [map_comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ↑(AddMonoidHom.comp (map g) (map f)) x = ↑(map g) (↑(map f) x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Mul α
x y : α
⊢ of x * of y = of (x * y)
[PROOFSTEP]
rw [mul_def, lift.of, lift.of]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Mul α
src✝¹ : Mul (FreeAbelianGroup α) := mul α
src✝ : AddCommGroup (FreeAbelianGroup α) := addCommGroup α
x y z : FreeAbelianGroup α
⊢ (x + y) * z = x * z + y * z
[PROOFSTEP]
simp only [(· * ·), Mul.mul, map_add, ← Pi.add_def, lift.add']
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Mul α
src✝¹ : Distrib (FreeAbelianGroup α) := distrib
src✝ : AddCommGroup (FreeAbelianGroup α) := addCommGroup α
a : FreeAbelianGroup α
⊢ 0 * a = 0
[PROOFSTEP]
have h : 0 * a + 0 * a = 0 * a := by simp [← add_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Mul α
src✝¹ : Distrib (FreeAbelianGroup α) := distrib
src✝ : AddCommGroup (FreeAbelianGroup α) := addCommGroup α
a : FreeAbelianGroup α
⊢ 0 * a + 0 * a = 0 * a
[PROOFSTEP]
simp [← add_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Mul α
src✝¹ : Distrib (FreeAbelianGroup α) := distrib
src✝ : AddCommGroup (FreeAbelianGroup α) := addCommGroup α
a : FreeAbelianGroup α
h : 0 * a + 0 * a = 0 * a
⊢ 0 * a = 0
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
⊢ x * y * z = x * (y * z)
[PROOFSTEP]
refine' FreeAbelianGroup.induction_on z (by simp only [mul_zero]) (fun L3 ↦ _) (fun L3 ih ↦ _) fun z₁ z₂ ih₁ ih₂ ↦ _
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
⊢ x * y * 0 = x * (y * 0)
[PROOFSTEP]
simp only [mul_zero]
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
L3 : α
⊢ x * y * of L3 = x * (y * of L3)
[PROOFSTEP]
refine'
  FreeAbelianGroup.induction_on y (by simp only [mul_zero, zero_mul]) (fun L2 ↦ _) (fun L2 ih ↦ _) fun y₁ y₂ ih₁ ih₂ ↦ _
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
L3 : α
⊢ x * 0 * of L3 = x * (0 * of L3)
[PROOFSTEP]
simp only [mul_zero, zero_mul]
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
L3 L2 : α
⊢ x * of L2 * of L3 = x * (of L2 * of L3)
[PROOFSTEP]
refine' FreeAbelianGroup.induction_on x (by simp only [zero_mul]) (fun L1 ↦ _) (fun L1 ih ↦ _) fun x₁ x₂ ih₁ ih₂ ↦ _
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
L3 L2 : α
⊢ 0 * of L2 * of L3 = 0 * (of L2 * of L3)
[PROOFSTEP]
simp only [zero_mul]
[GOAL]
case refine'_1.refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
L3 L2 L1 : α
⊢ of L1 * of L2 * of L3 = of L1 * (of L2 * of L3)
[PROOFSTEP]
rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
[GOAL]
case refine'_1.refine'_1.refine'_2
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
L3 L2 L1 : α
ih : of L1 * of L2 * of L3 = of L1 * (of L2 * of L3)
⊢ -of L1 * of L2 * of L3 = -of L1 * (of L2 * of L3)
[PROOFSTEP]
rw [neg_mul, neg_mul, neg_mul, ih]
[GOAL]
case refine'_1.refine'_1.refine'_3
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
L3 L2 : α
x₁ x₂ : FreeAbelianGroup α
ih₁ : x₁ * of L2 * of L3 = x₁ * (of L2 * of L3)
ih₂ : x₂ * of L2 * of L3 = x₂ * (of L2 * of L3)
⊢ (x₁ + x₂) * of L2 * of L3 = (x₁ + x₂) * (of L2 * of L3)
[PROOFSTEP]
rw [add_mul, add_mul, add_mul, ih₁, ih₂]
[GOAL]
case refine'_1.refine'_2
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ x * -of L2 * of L3 = x * (-of L2 * of L3)
[PROOFSTEP]
rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
[GOAL]
case refine'_1.refine'_3
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ x * (y₁ + y₂) * of L3 = x * ((y₁ + y₂) * of L3)
[PROOFSTEP]
rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ x * y * -of L3 = x * (y * -of L3)
[PROOFSTEP]
rw [mul_neg, mul_neg, mul_neg, ih]
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
inst✝ : Semigroup α
src✝ : NonUnitalNonAssocRing (FreeAbelianGroup α) := nonUnitalNonAssocRing
x y z z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))
[PROOFSTEP]
rw [mul_add, mul_add, mul_add, ih₁, ih₂]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
⊢ 1 * x = x
[PROOFSTEP]
dsimp only [(· * ·), Mul.mul, OfNat.ofNat, One.one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
⊢ ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) x = x
[PROOFSTEP]
refine' FreeAbelianGroup.induction_on x rfl _ _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
⊢ ∀ (x : α), ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) (of x) = of x
[PROOFSTEP]
intro L
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
L : α
⊢ ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) (of L) = of L
[PROOFSTEP]
rw [lift.of, lift.of]
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
L : α
⊢ of (Mul.mul One.one L) = of L
[PROOFSTEP]
congr 1
[GOAL]
case refine'_1.e_x
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
L : α
⊢ Mul.mul One.one L = L
[PROOFSTEP]
exact one_mul L
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
⊢ ∀ (x : α),
    ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) (of x) = of x →
      ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) (-of x) = -of x
[PROOFSTEP]
intro L ih
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
L : α
ih : ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) (of L) = of L
⊢ ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) (-of L) = -of L
[PROOFSTEP]
rw [map_neg, ih]
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
⊢ ∀ (x y : FreeAbelianGroup α),
    ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) x = x →
      ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) y = y →
        ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) (x + y) = x + y
[PROOFSTEP]
intro x1 x2 ih1 ih2
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x x1 x2 : FreeAbelianGroup α
ih1 : ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) x1 = x1
ih2 : ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) x2 = x2
⊢ ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of One.one)) (x1 + x2) = x1 + x2
[PROOFSTEP]
rw [map_add, ih1, ih2]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
⊢ x * 1 = x
[PROOFSTEP]
dsimp only [(· * ·), Mul.mul, OfNat.ofNat, One.one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
⊢ ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) x) (of One.one) = x
[PROOFSTEP]
rw [lift.of]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
⊢ ↑(↑lift fun x₁ => of (Mul.mul x₁ One.one)) x = x
[PROOFSTEP]
refine' FreeAbelianGroup.induction_on x rfl (fun L ↦ _) (fun L ih ↦ _) fun x1 x2 ih1 ih2 ↦ _
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
L : α
⊢ ↑(↑lift fun x₁ => of (Mul.mul x₁ One.one)) (of L) = of L
[PROOFSTEP]
erw [lift.of]
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
L : α
⊢ of (Mul.mul L One.one) = of L
[PROOFSTEP]
congr 1
[GOAL]
case refine'_1.e_x
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
L : α
⊢ Mul.mul L One.one = L
[PROOFSTEP]
exact mul_one L
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x : FreeAbelianGroup α
L : α
ih : ↑(↑lift fun x₁ => of (Mul.mul x₁ One.one)) (of L) = of L
⊢ ↑(↑lift fun x₁ => of (Mul.mul x₁ One.one)) (-of L) = -of L
[PROOFSTEP]
rw [map_neg, ih]
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
src✝¹ : NonUnitalRing (FreeAbelianGroup α) := nonUnitalRing α
src✝ : One (FreeAbelianGroup α) := one α
x x1 x2 : FreeAbelianGroup α
ih1 : ↑(↑lift fun x₁ => of (Mul.mul x₁ One.one)) x1 = x1
ih2 : ↑(↑lift fun x₁ => of (Mul.mul x₁ One.one)) x2 = x2
⊢ ↑(↑lift fun x₁ => of (Mul.mul x₁ One.one)) (x1 + x2) = x1 + x2
[PROOFSTEP]
rw [map_add, ih1, ih2]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
⊢ OneHom.toFun { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) } (x * y) =
    OneHom.toFun { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) } x *
      OneHom.toFun { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) } y
[PROOFSTEP]
simp only
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
⊢ ↑(↑lift ↑f) (x * y) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) y
[PROOFSTEP]
refine' FreeAbelianGroup.induction_on y (by simp only [mul_zero, map_zero]) (fun L2 ↦ _) (fun L2 ih ↦ _) _
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
⊢ ↑(↑lift ↑f) (x * 0) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) 0
[PROOFSTEP]
simp only [mul_zero, map_zero]
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
L2 : α
⊢ ↑(↑lift ↑f) (x * of L2) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) (of L2)
[PROOFSTEP]
refine' FreeAbelianGroup.induction_on x (by simp only [zero_mul, map_zero]) (fun L1 ↦ _) (fun L1 ih ↦ _) _
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
L2 : α
⊢ ↑(↑lift ↑f) (0 * of L2) = ↑(↑lift ↑f) 0 * ↑(↑lift ↑f) (of L2)
[PROOFSTEP]
simp only [zero_mul, map_zero]
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
L2 L1 : α
⊢ ↑(↑lift ↑f) (of L1 * of L2) = ↑(↑lift ↑f) (of L1) * ↑(↑lift ↑f) (of L2)
[PROOFSTEP]
simp_rw [of_mul_of, lift.of]
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
L2 L1 : α
⊢ ↑f (L1 * L2) = ↑f L1 * ↑f L2
[PROOFSTEP]
exact f.map_mul _ _
[GOAL]
case refine'_1.refine'_2
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
L2 L1 : α
ih : ↑(↑lift ↑f) (of L1 * of L2) = ↑(↑lift ↑f) (of L1) * ↑(↑lift ↑f) (of L2)
⊢ ↑(↑lift ↑f) (-of L1 * of L2) = ↑(↑lift ↑f) (-of L1) * ↑(↑lift ↑f) (of L2)
[PROOFSTEP]
simp_rw [neg_mul, map_neg, neg_mul]
[GOAL]
case refine'_1.refine'_2
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
L2 L1 : α
ih : ↑(↑lift ↑f) (of L1 * of L2) = ↑(↑lift ↑f) (of L1) * ↑(↑lift ↑f) (of L2)
⊢ -↑(↑lift ↑f) (of L1 * of L2) = -(↑(↑lift ↑f) (of L1) * ↑(↑lift ↑f) (of L2))
[PROOFSTEP]
exact congr_arg Neg.neg ih
[GOAL]
case refine'_1.refine'_3
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
L2 : α
⊢ ∀ (x y : FreeAbelianGroup α),
    ↑(↑lift ↑f) (x * of L2) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) (of L2) →
      ↑(↑lift ↑f) (y * of L2) = ↑(↑lift ↑f) y * ↑(↑lift ↑f) (of L2) →
        ↑(↑lift ↑f) ((x + y) * of L2) = ↑(↑lift ↑f) (x + y) * ↑(↑lift ↑f) (of L2)
[PROOFSTEP]
intro x1 x2 ih1 ih2
[GOAL]
case refine'_1.refine'_3
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
L2 : α
x1 x2 : FreeAbelianGroup α
ih1 : ↑(↑lift ↑f) (x1 * of L2) = ↑(↑lift ↑f) x1 * ↑(↑lift ↑f) (of L2)
ih2 : ↑(↑lift ↑f) (x2 * of L2) = ↑(↑lift ↑f) x2 * ↑(↑lift ↑f) (of L2)
⊢ ↑(↑lift ↑f) ((x1 + x2) * of L2) = ↑(↑lift ↑f) (x1 + x2) * ↑(↑lift ↑f) (of L2)
[PROOFSTEP]
simp only [add_mul, map_add, ih1, ih2]
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
L2 : α
ih : ↑(↑lift ↑f) (x * of L2) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) (of L2)
⊢ ↑(↑lift ↑f) (x * -of L2) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) (-of L2)
[PROOFSTEP]
rw [mul_neg, map_neg, map_neg, mul_neg, ih]
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y : FreeAbelianGroup α
⊢ ∀ (x_1 y : FreeAbelianGroup α),
    ↑(↑lift ↑f) (x * x_1) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) x_1 →
      ↑(↑lift ↑f) (x * y) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) y →
        ↑(↑lift ↑f) (x * (x_1 + y)) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) (x_1 + y)
[PROOFSTEP]
intro y1 y2 ih1 ih2
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
src✝ : (fun x => FreeAbelianGroup α →+ R) ↑f := ↑lift ↑f
x y y1 y2 : FreeAbelianGroup α
ih1 : ↑(↑lift ↑f) (x * y1) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) y1
ih2 : ↑(↑lift ↑f) (x * y2) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) y2
⊢ ↑(↑lift ↑f) (x * (y1 + y2)) = ↑(↑lift ↑f) x * ↑(↑lift ↑f) (y1 + y2)
[PROOFSTEP]
rw [mul_add, map_add, map_add, mul_add, ih1, ih2]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
⊢ ∀ (x : α),
    ↑((fun F => MonoidHom.comp (↑F) ofMulHom)
            ((fun f =>
                let src := ↑lift ↑f;
                {
                  toMonoidHom :=
                    { toOneHom := { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) },
                      map_mul' :=
                        (_ :
                          ∀ (x y : FreeAbelianGroup α),
                            OneHom.toFun { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) } (x * y) =
                              OneHom.toFun { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) } x *
                                OneHom.toFun { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) } y) },
                  map_zero' := (_ : ZeroHom.toFun (↑src) 0 = 0),
                  map_add' :=
                    (_ :
                      ∀ (x y : FreeAbelianGroup α),
                        ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
              f))
        x =
      ↑f x
[PROOFSTEP]
simp only [RingHom.coe_monoidHom_mk, MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, ofMulHom_coe,
  Function.comp_apply, lift.of, forall_const]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
F : FreeAbelianGroup α →+* R
⊢ (fun f => ↑f)
      ((fun f =>
          let src := ↑lift ↑f;
          {
            toMonoidHom :=
              { toOneHom := { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : FreeAbelianGroup α),
                      OneHom.toFun { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) } (x * y) =
                        OneHom.toFun { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) } x *
                          OneHom.toFun { toFun := ↑(↑lift ↑f), map_one' := (_ : ↑(↑lift ↑f) (of 1) = 1) } y) },
            map_zero' := (_ : ZeroHom.toFun (↑src) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : FreeAbelianGroup α),
                  ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        ((fun F => MonoidHom.comp (↑F) ofMulHom) F)) =
    (fun f => ↑f) F
[PROOFSTEP]
simp only
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
F : FreeAbelianGroup α →+* R
⊢ ↑{
        toMonoidHom :=
          {
            toOneHom :=
              { toFun := ↑(↑lift ↑(MonoidHom.comp (↑F) ofMulHom)),
                map_one' := (_ : ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)) (of 1) = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : FreeAbelianGroup α),
                  OneHom.toFun
                      { toFun := ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)),
                        map_one' := (_ : ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)) (of 1) = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)),
                          map_one' := (_ : ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)) (of 1) = 1) }
                        x *
                      OneHom.toFun
                        { toFun := ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)),
                          map_one' := (_ : ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)) (of 1) = 1) }
                        y) },
        map_zero' := (_ : ZeroHom.toFun (↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F))) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : FreeAbelianGroup α),
              ZeroHom.toFun (↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F))) (x + y) =
                ZeroHom.toFun (↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F))) x +
                  ZeroHom.toFun (↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F))) y) } =
    ↑F
[PROOFSTEP]
rw [← lift.apply_symm_apply (↑F : FreeAbelianGroup α →+ R)]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type u_1
inst✝¹ : Monoid α
inst✝ : Ring R
F : FreeAbelianGroup α →+* R
⊢ ↑{
        toMonoidHom :=
          {
            toOneHom :=
              { toFun := ↑(↑lift ↑(MonoidHom.comp (↑F) ofMulHom)),
                map_one' := (_ : ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)) (of 1) = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : FreeAbelianGroup α),
                  OneHom.toFun
                      { toFun := ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)),
                        map_one' := (_ : ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)) (of 1) = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)),
                          map_one' := (_ : ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)) (of 1) = 1) }
                        x *
                      OneHom.toFun
                        { toFun := ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)),
                          map_one' := (_ : ↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F)) (of 1) = 1) }
                        y) },
        map_zero' := (_ : ZeroHom.toFun (↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F))) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : FreeAbelianGroup α),
              ZeroHom.toFun (↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F))) (x + y) =
                ZeroHom.toFun (↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F))) x +
                  ZeroHom.toFun (↑(↑lift ↑((fun F => MonoidHom.comp (↑F) ofMulHom) F))) y) } =
    ↑lift (↑lift.symm ↑F)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
⊢ x * y = y * x
[PROOFSTEP]
refine' FreeAbelianGroup.induction_on x (zero_mul y) _ _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
⊢ ∀ (x : α), of x * y = y * of x
[PROOFSTEP]
intro s
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s : α
⊢ of s * y = y * of s
[PROOFSTEP]
refine' FreeAbelianGroup.induction_on y (zero_mul _).symm _ _ _
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s : α
⊢ ∀ (x : α), of s * of x = of x * of s
[PROOFSTEP]
intro t
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s t : α
⊢ of s * of t = of t * of s
[PROOFSTEP]
dsimp only [(· * ·), Mul.mul]
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s t : α
⊢ ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of s)) (of t) =
    ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of t)) (of s)
[PROOFSTEP]
iterate 4 rw [lift.of]
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s t : α
⊢ ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of s)) (of t) =
    ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of t)) (of s)
[PROOFSTEP]
rw [lift.of]
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s t : α
⊢ ↑(↑lift fun x₁ => of (Mul.mul x₁ t)) (of s) = ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of t)) (of s)
[PROOFSTEP]
rw [lift.of]
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s t : α
⊢ of (Mul.mul s t) = ↑(↑lift fun x₂ => ↑(↑lift fun x₁ => of (Mul.mul x₁ x₂)) (of t)) (of s)
[PROOFSTEP]
rw [lift.of]
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s t : α
⊢ of (Mul.mul s t) = ↑(↑lift fun x₁ => of (Mul.mul x₁ s)) (of t)
[PROOFSTEP]
rw [lift.of]
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s t : α
⊢ of (Mul.mul s t) = of (Mul.mul t s)
[PROOFSTEP]
congr 1
[GOAL]
case refine'_1.refine'_1.e_x
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s t : α
⊢ Mul.mul s t = Mul.mul t s
[PROOFSTEP]
exact mul_comm _ _
[GOAL]
case refine'_1.refine'_2
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s : α
⊢ ∀ (x : α), of s * of x = of x * of s → of s * -of x = -of x * of s
[PROOFSTEP]
intro t ih
[GOAL]
case refine'_1.refine'_2
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s t : α
ih : of s * of t = of t * of s
⊢ of s * -of t = -of t * of s
[PROOFSTEP]
rw [mul_neg, ih, neg_mul_eq_neg_mul]
[GOAL]
case refine'_1.refine'_3
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s : α
⊢ ∀ (x y : FreeAbelianGroup α), of s * x = x * of s → of s * y = y * of s → of s * (x + y) = (x + y) * of s
[PROOFSTEP]
intro y1 y2 ih1 ih2
[GOAL]
case refine'_1.refine'_3
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : of s * y1 = y1 * of s
ih2 : of s * y2 = y2 * of s
⊢ of s * (y1 + y2) = (y1 + y2) * of s
[PROOFSTEP]
rw [mul_add, add_mul, ih1, ih2]
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
⊢ ∀ (x : α), of x * y = y * of x → -of x * y = y * -of x
[PROOFSTEP]
intro s ih
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
s : α
ih : of s * y = y * of s
⊢ -of s * y = y * -of s
[PROOFSTEP]
rw [neg_mul, ih, neg_mul_eq_mul_neg]
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y : FreeAbelianGroup α
⊢ ∀ (x y_1 : FreeAbelianGroup α), x * y = y * x → y_1 * y = y * y_1 → (x + y_1) * y = y * (x + y_1)
[PROOFSTEP]
intro x1 x2 ih1 ih2
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
inst✝ : CommMonoid α
src✝ : Ring (FreeAbelianGroup α) := ring α
x y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
⊢ (x1 + x2) * y = y * (x1 + x2)
[PROOFSTEP]
rw [add_mul, mul_add, ih1, ih2]
[GOAL]
α : Type u
β : Type v
γ : Type w
x : FreeAbelianGroup PEmpty
⊢ ∀ (x y : FreeAbelianGroup PEmpty), x = default → y = default → x + y = default
[PROOFSTEP]
rintro - - rfl rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
x : FreeAbelianGroup PEmpty
⊢ default + default = default
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
T : Type u_1
inst✝ : Unique T
z : FreeAbelianGroup T
⊢ (fun n => n • of default) (↑(↑lift fun x => 1) 0) = 0
[PROOFSTEP]
simp only [zero_smul, AddMonoidHom.map_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
T : Type u_1
inst✝ : Unique T
z : FreeAbelianGroup T
⊢ (fun n => n • of default) (↑(↑lift fun x => 1) (of default)) = of default
[PROOFSTEP]
simp only [one_smul, lift.of]
[GOAL]
α : Type u
β : Type v
γ : Type w
T : Type u_1
inst✝ : Unique T
z : FreeAbelianGroup T
⊢ (fun n => n • of default) (↑(↑lift fun x => 1) (of default)) = of default →
    (fun n => n • of default) (↑(↑lift fun x => 1) (-of default)) = -of default
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
T : Type u_1
inst✝ : Unique T
z x y : FreeAbelianGroup T
hx : (fun n => n • of default) (↑(↑lift fun x => 1) x) = x
hy : (fun n => n • of default) (↑(↑lift fun x => 1) y) = y
⊢ (fun n => n • of default) (↑(↑lift fun x => 1) (x + y)) = x + y
[PROOFSTEP]
simp only [AddMonoidHom.map_add, add_smul] at *
[GOAL]
α : Type u
β : Type v
γ : Type w
T : Type u_1
inst✝ : Unique T
z x y : FreeAbelianGroup T
hx : ↑(↑lift fun x => 1) x • of default = x
hy : ↑(↑lift fun x => 1) y • of default = y
⊢ ↑(↑lift fun x => 1) x • of default + ↑(↑lift fun x => 1) y • of default = x + y
[PROOFSTEP]
rw [hx, hy]
[GOAL]
α : Type u
β : Type v
γ : Type w
T : Type u_1
inst✝ : Unique T
n : ℤ
⊢ ↑(↑lift fun x => 1) ((fun n => n • of default) n) = n
[PROOFSTEP]
rw [AddMonoidHom.map_zsmul, lift.of]
[GOAL]
α : Type u
β : Type v
γ : Type w
T : Type u_1
inst✝ : Unique T
n : ℤ
⊢ n • 1 = n
[PROOFSTEP]
exact zsmul_int_one n
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α ≃ β
⊢ Function.LeftInverse ↑(map ↑f.symm) ↑(map ↑f)
[PROOFSTEP]
intro x
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α ≃ β
x : FreeAbelianGroup α
⊢ ↑(map ↑f.symm) (↑(map ↑f) x) = x
[PROOFSTEP]
rw [← map_comp_apply, Equiv.symm_comp_self, map_id]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α ≃ β
x : FreeAbelianGroup α
⊢ ↑(AddMonoidHom.id (FreeAbelianGroup α)) x = x
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α ≃ β
⊢ Function.RightInverse ↑(map ↑f.symm) ↑(map ↑f)
[PROOFSTEP]
intro x
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α ≃ β
x : FreeAbelianGroup β
⊢ ↑(map ↑f) (↑(map ↑f.symm) x) = x
[PROOFSTEP]
rw [← map_comp_apply, Equiv.self_comp_symm, map_id]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α ≃ β
x : FreeAbelianGroup β
⊢ ↑(AddMonoidHom.id (FreeAbelianGroup β)) x = x
[PROOFSTEP]
rfl
