[GOAL]
S✝ : Type u'
T : Type u''
R✝ : Type u
M✝ : Type v
inst✝⁵ : SMul R✝ M✝
inst✝⁴ : SetLike S✝ M✝
hS : SMulMemClass S✝ R✝ M✝
s : S✝
R : Type u_1
M : Type u_2
S : Type u_3
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : SetLike S M
inst✝ : SMulMemClass S R M
N : S
x : M
h : ∀ (a : R), a • x ∈ N
⊢ x ∈ N
[PROOFSTEP]
simpa using h 1
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p q : SubMulAction R M
h : p.carrier = q.carrier
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
q : SubMulAction R M
carrier✝ : Set M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ carrier✝ → c • x ∈ carrier✝
h : { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, smul_mem' := smul_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
carrier✝¹ : Set M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ carrier✝¹ → c • x ∈ carrier✝¹
carrier✝ : Set M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ carrier✝ → c • x ∈ carrier✝
h :
  { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ }.carrier = { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ } = { carrier := carrier✝, smul_mem' := smul_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p : SubMulAction R M
r : R
x : M
⊢ { x // x ∈ p } →[R] M
[PROOFSTEP]
refine' { toFun := Subtype.val .. }
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p : SubMulAction R M
r : R
x : M
⊢ ∀ (m : R) (x : { x // x ∈ p }), ↑(m • x) = m • ↑x
[PROOFSTEP]
simp [val_smul]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ s • x ∈ p
[PROOFSTEP]
rw [← one_smul R x, ← smul_assoc]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ (s • 1) • x ∈ p
[PROOFSTEP]
exact p.smul_mem _ h
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
⊢ MulAction.Stabilizer.submonoid R m = MulAction.Stabilizer.submonoid R ↑m
[PROOFSTEP]
ext
[GOAL]
case h
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
x✝ : R
⊢ x✝ ∈ MulAction.Stabilizer.submonoid R m ↔ x✝ ∈ MulAction.Stabilizer.submonoid R ↑m
[PROOFSTEP]
simp only [MulAction.mem_stabilizer_submonoid_iff, ← SubMulAction.val_smul, SetLike.coe_eq_coe]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
⊢ MulAction.stabilizer R m = MulAction.stabilizer R ↑m
[PROOFSTEP]
rw [← Subgroup.toSubmonoid_eq]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
⊢ (MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R ↑m).toSubmonoid
[PROOFSTEP]
exact stabilizer_of_subMul.submonoid m
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : SubMulAction R M
r : R
x y : M
hx : x ∈ p
⊢ -x ∈ p
[PROOFSTEP]
rw [← neg_one_smul R]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : SubMulAction R M
r : R
x y : M
hx : x ∈ p
⊢ -1 • x ∈ p
[PROOFSTEP]
exact p.smul_mem _ hx
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : SubMulAction R M
r : R
x y : M
h : -x ∈ p
⊢ x ∈ p
[PROOFSTEP]
rw [← neg_neg x]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : SubMulAction R M
r : R
x y : M
h : -x ∈ p
⊢ - -x ∈ p
[PROOFSTEP]
exact neg_mem _ h


[GOAL]
M : Type u_1
inst✝ : Monoid M
⊢ SMulCommClass { x // x ∈ center M } { x // x ∈ center M } M
[PROOFSTEP]
infer_instance


[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


[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
⊢ 1 * a = a
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ x ∈ 1 * a ↔ x ∈ a
[PROOFSTEP]
simp only [mem_mul, mem_one, smul_mul_assoc, exists_and_left, exists_exists_eq_and, one_mul]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ a_1 x_1, x_1 ∈ a ∧ a_1 • x_1 = x) ↔ x ∈ a
[PROOFSTEP]
refine' ⟨_, fun hx => ⟨1, x, hx, one_smul _ _⟩⟩
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ a_1 x_1, x_1 ∈ a ∧ a_1 • x_1 = x) → x ∈ a
[PROOFSTEP]
rintro ⟨r, y, hy, rfl⟩
[GOAL]
case h.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
r : R
y : M
hy : y ∈ a
⊢ r • y ∈ a
[PROOFSTEP]
exact smul_mem _ _ hy
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
⊢ a * 1 = a
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ x ∈ a * 1 ↔ x ∈ a
[PROOFSTEP]
simp only [mem_mul, mem_one, mul_smul_comm, exists_and_left, exists_exists_eq_and, mul_one]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ y, y ∈ a ∧ ∃ a, a • y = x) ↔ x ∈ a
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ y, y ∈ a ∧ ∃ a, a • y = x) → x ∈ a
[PROOFSTEP]
rintro ⟨y, hy, r, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
y : M
hy : y ∈ a
r : R
⊢ r • y ∈ a
[PROOFSTEP]
exact smul_mem _ _ hy
[GOAL]
case h.mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ x ∈ a → ∃ y, y ∈ a ∧ ∃ a, a • y = x
[PROOFSTEP]
intro hx
[GOAL]
case h.mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
hx : x ∈ a
⊢ ∃ y, y ∈ a ∧ ∃ a, a • y = x
[PROOFSTEP]
exact ⟨x, hx, 1, one_smul _ _⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
x✝ : 1 ≠ 0
⊢ ↑(p ^ 1) = ↑p ^ 1
[PROOFSTEP]
rw [pow_one, pow_one]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ↑(p ^ (n + 2)) = ↑p ^ (n + 2)
[PROOFSTEP]
rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ ↑p ^ 0 ⊆ ↑(p ^ 0)
[PROOFSTEP]
rw [pow_zero, pow_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ 1 ⊆ ↑1
[PROOFSTEP]
exact subset_coe_one
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
⊢ ↑p ^ (n + 1) ⊆ ↑(p ^ (n + 1))
[PROOFSTEP]
rw [← Nat.succ_eq_add_one, coe_pow _ n.succ_ne_zero]


[GOAL]
β : Type u_1
M : Type ?u.36709
α : Type ?u.36708
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
⊢ ↑mk.symm c₁ • a = ↑mk.symm c₂ • a
[PROOFSTEP]
rcases exists_pair_ne β with ⟨x, y, hne⟩
[GOAL]
case intro.intro
β : Type u_1
M : Type ?u.36709
α : Type ?u.36708
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : x ≠ y
⊢ ↑mk.symm c₁ • a = ↑mk.symm c₂ • a
[PROOFSTEP]
contrapose! hne
[GOAL]
case intro.intro
β : Type u_1
M : Type ?u.36709
α : Type ?u.36708
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : ↑mk.symm c₁ • a ≠ ↑mk.symm c₂ • a
⊢ x = y
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
case intro.intro
β : Type u_1
M : Type ?u.36709
α : Type ?u.36708
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : ↑mk.symm c₁ • a ≠ ↑mk.symm c₂ • a
this : DecidableEq α
⊢ x = y
[PROOFSTEP]
replace h := congr_fun (h (update (const α x) (mk.symm c₂ • a) y)) a
[GOAL]
case intro.intro
β : Type u_1
M : Type ?u.36709
α : Type ?u.36708
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
a : α
x y : β
hne : ↑mk.symm c₁ • a ≠ ↑mk.symm c₂ • a
this : DecidableEq α
h : (c₁ • update (const α x) (↑mk.symm c₂ • a) y) a = (c₂ • update (const α x) (↑mk.symm c₂ • a) y) a
⊢ x = y
[PROOFSTEP]
simpa [smul_apply, hne] using h


[GOAL]
M₀ : Type ?u.8
inst✝ : MonoidWithZero M₀
⊢ 1 ∈
    { carrier := {x | ∀ (y : M₀), y * x = 0 → y = 0},
        mul_mem' :=
          (_ :
            ∀ {x y : M₀},
              x ∈ {x | ∀ (y : M₀), y * x = 0 → y = 0} →
                y ∈ {x | ∀ (y : M₀), y * x = 0 → y = 0} → ∀ (z : M₀), z * (x * y) = 0 → z = 0) }.carrier
[PROOFSTEP]
simp
[GOAL]
M₀ : Type ?u.2171
inst✝ : MonoidWithZero M₀
⊢ 1 ∈
    { carrier := {x | ∀ (y : M₀), x * y = 0 → y = 0},
        mul_mem' :=
          (_ :
            ∀ {x y : M₀},
              x ∈ {x | ∀ (y : M₀), x * y = 0 → y = 0} →
                y ∈ {x | ∀ (y : M₀), x * y = 0 → y = 0} → ∀ (z : M₀), x * y * z = 0 → z = 0) }.carrier
[PROOFSTEP]
simp
[GOAL]
M₀✝ : Type ?u.4317
inst✝¹ : MonoidWithZero M₀✝
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀
[PROOFSTEP]
ext x
[GOAL]
case h
M₀✝ : Type ?u.4317
inst✝¹ : MonoidWithZero M₀✝
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
x : M₀
⊢ x ∈ nonZeroDivisorsLeft M₀ ↔ x ∈ nonZeroDivisorsRight M₀
[PROOFSTEP]
simp [mul_comm x]
[GOAL]
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
⊢ ↑(nonZeroDivisorsLeft M₀) = {x | x ≠ 0}
[PROOFSTEP]
ext x
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsLeft M₀) ↔ x ∈ {x | x ≠ 0}
[PROOFSTEP]
simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, forall_eq_or_imp, true_and, Set.mem_setOf_eq]
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ (∀ (a : M₀), x = 0 → a = 0) ↔ x ≠ 0
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun hx y hx' ↦ by contradiction⟩
[GOAL]
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
hx : x ≠ 0
y : M₀
hx' : x = 0
⊢ y = 0
[PROOFSTEP]
contradiction
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : ∀ (a : M₀), x = 0 → a = 0
⊢ x ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ a, x = 0 ∧ a ≠ 0
[PROOFSTEP]
exact ⟨1, h, one_ne_zero⟩
[GOAL]
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
⊢ ↑(nonZeroDivisorsRight M₀) = {x | x ≠ 0}
[PROOFSTEP]
ext x
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsRight M₀) ↔ x ∈ {x | x ≠ 0}
[PROOFSTEP]
simp only [SetLike.mem_coe, mem_nonZeroDivisorsRight_iff, mul_eq_zero, Set.mem_setOf_eq]
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ (∀ (y : M₀), x = 0 ∨ y = 0 → y = 0) ↔ x ≠ 0
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun hx y hx' ↦ by aesop⟩
[GOAL]
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
hx : x ≠ 0
y : M₀
hx' : x = 0 ∨ y = 0
⊢ y = 0
[PROOFSTEP]
aesop
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : ∀ (y : M₀), x = 0 ∨ y = 0 → y = 0
⊢ x ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ y, (x = 0 ∨ y = 0) ∧ y ≠ 0
[PROOFSTEP]
exact ⟨1, Or.inl h, one_ne_zero⟩


[GOAL]
M✝ : Type u_1
N : Type u_2
A✝ : Type u_3
inst✝⁴ : MulOneClass M✝
s : Set M✝
inst✝³ : AddZeroClass A✝
t : Set A✝
M : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ x ^ 0 ∈ S
[PROOFSTEP]
rw [pow_zero]
[GOAL]
M✝ : Type u_1
N : Type u_2
A✝ : Type u_3
inst✝⁴ : MulOneClass M✝
s : Set M✝
inst✝³ : AddZeroClass A✝
t : Set A✝
M : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ 1 ∈ S
[PROOFSTEP]
exact OneMemClass.one_mem S
[GOAL]
M✝ : Type u_1
N : Type u_2
A✝ : Type u_3
inst✝⁴ : MulOneClass M✝
s : Set M✝
inst✝³ : AddZeroClass A✝
t : Set A✝
M : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ (n + 1) ∈ S
[PROOFSTEP]
rw [pow_succ]
[GOAL]
M✝ : Type u_1
N : Type u_2
A✝ : Type u_3
inst✝⁴ : MulOneClass M✝
s : Set M✝
inst✝³ : AddZeroClass A✝
t : Set A✝
M : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x * x ^ n ∈ S
[PROOFSTEP]
exact mul_mem hx (pow_mem hx n)
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
p q : Submonoid M
h : (fun s => s.carrier) p = (fun s => s.carrier) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
q : Submonoid M
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
h : (fun s => s.carrier) { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ } = (fun s => s.carrier) q
⊢ { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
toSubsemigroup✝¹ : Subsemigroup M
one_mem'✝¹ : 1 ∈ toSubsemigroup✝¹.carrier
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
h :
  (fun s => s.carrier) { toSubsemigroup := toSubsemigroup✝¹, one_mem' := one_mem'✝¹ } =
    (fun s => s.carrier) { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
⊢ { toSubsemigroup := toSubsemigroup✝¹, one_mem' := one_mem'✝¹ } =
    { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSubsemigroup
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
toSubsemigroup✝¹ : Subsemigroup M
one_mem'✝¹ : 1 ∈ toSubsemigroup✝¹.carrier
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
h :
  (fun s => s.carrier) { toSubsemigroup := toSubsemigroup✝¹, one_mem' := one_mem'✝¹ } =
    (fun s => s.carrier) { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
⊢ toSubsemigroup✝¹ = toSubsemigroup✝
[PROOFSTEP]
exact SetLike.coe_injective' h
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
a✝ b✝ : M
ha : a✝ ∈ {1}
hb : b✝ ∈ {1}
⊢ a✝ * b✝ ∈ {1}
[PROOFSTEP]
simp only [Set.mem_singleton_iff] at *
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
a✝ b✝ : M
ha : a✝ = 1
hb : b✝ = 1
⊢ a✝ * b✝ = 1
[PROOFSTEP]
rw [ha, hb, mul_one]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set (Submonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ (t : Submonoid M) (_ : t ∈ s), ↑t
hy : b✝ ∈ ⋂ (t : Submonoid M) (_ : t ∈ s), ↑t
i : Submonoid M
h : i ∈ s
⊢ a✝ ∈ i
[PROOFSTEP]
apply Set.mem_iInter₂.1 hx i h
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set (Submonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ (t : Submonoid M) (_ : t ∈ s), ↑t
hy : b✝ ∈ ⋂ (t : Submonoid M) (_ : t ∈ s), ↑t
i : Submonoid M
h : i ∈ s
⊢ b✝ ∈ i
[PROOFSTEP]
apply Set.mem_iInter₂.1 hy i h
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S✝ : Submonoid M
ι : Sort u_4
S : ι → Submonoid M
x : M
⊢ x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i
[PROOFSTEP]
simp only [iInf, mem_sInf, Set.forall_range_iff]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S✝ : Submonoid M
ι : Sort u_4
S : ι → Submonoid M
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
[PROOFSTEP]
simp only [iInf, coe_sInf, Set.biInter_range]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
h : Subsingleton M
x y : Submonoid M
i : M
⊢ 1 ∈ x ↔ 1 ∈ y
[PROOFSTEP]
simp [Submonoid.one_mem]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set M
p : (x : M) → x ∈ closure s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H1 : p 1 (_ : 1 ∈ closure s)
Hmul : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
x : M
hx : x ∈ closure s
⊢ p x hx
[PROOFSTEP]
refine' Exists.elim _ fun (hx : x ∈ closure s) (hc : p x hx) => hc
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set M
p : (x : M) → x ∈ closure s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H1 : p 1 (_ : 1 ∈ closure s)
Hmul : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
x : M
hx : x ∈ closure s
⊢ ∃ x_1, p x x_1
[PROOFSTEP]
exact closure_induction hx (fun x hx => ⟨_, Hs x hx⟩) ⟨_, H1⟩ fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ => ⟨_, Hmul _ _ _ _ hx hy⟩
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
H1 : p 1
Hmul : ∀ (x y : M), p x → p y → p (x * y)
⊢ p x
[PROOFSTEP]
have : ∀ x ∈ closure s, p x := fun x hx => closure_induction hx Hs H1 Hmul
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
H1 : p 1
Hmul : ∀ (x y : M), p x → p y → p (x * y)
this : ∀ (x : M), x ∈ closure s → p x
⊢ p x
[PROOFSTEP]
simpa [hs] using this x
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
m : M
p : Submonoid M
⊢ closure {m} ≤ p ↔ m ∈ p
[PROOFSTEP]
rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ m ∈ ⨆ (i : ι), p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
[PROOFSTEP]
rw [← closure_singleton_le_iff_mem, le_iSup_iff]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ (∀ (b : Submonoid M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
[PROOFSTEP]
simp only [closure_singleton_le_iff_mem]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
ι : Sort u_4
p : ι → Submonoid M
⊢ ⨆ (i : ι), p i = closure (⋃ (i : ι), ↑(p i))
[PROOFSTEP]
simp_rw [Submonoid.closure_iUnion, Submonoid.closure_eq]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S p₁ p₂ : Submonoid M
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
[PROOFSTEP]
simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : MulOneClass M
s : Set M
inst✝¹ : AddZeroClass A
t : Set A
inst✝ : MulOneClass N
f g : M →* N
a✝ b✝ : M
hx : ↑f a✝ = ↑g a✝
hy : ↑f b✝ = ↑g b✝
⊢ a✝ * b✝ ∈ {x | ↑f x = ↑g x}
[PROOFSTEP]
simp [*]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : MulOneClass M
s : Set M
inst✝¹ : AddZeroClass A
t : Set A
inst✝ : MulOneClass N
f g : M →* N
⊢ 1 ∈
    { carrier := {x | ↑f x = ↑g x},
        mul_mem' := (_ : ∀ {a b : M}, ↑f a = ↑g a → ↑f b = ↑g b → ↑f (a * b) = ↑g (a * b)) }.carrier
[PROOFSTEP]
rw [Set.mem_setOf_eq, f.map_one, g.map_one]
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ ∀ {a b : M}, a ∈ setOf IsUnit → b ∈ setOf IsUnit → a * b ∈ setOf IsUnit
[PROOFSTEP]
intro a b ha hb
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a b : M
ha : a ∈ setOf IsUnit
hb : b ∈ setOf IsUnit
⊢ a * b ∈ setOf IsUnit
[PROOFSTEP]
rw [Set.mem_setOf_eq] at *
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a b : M
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b)
[PROOFSTEP]
exact IsUnit.mul ha hb
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ 1 ∈
    { carrier := setOf IsUnit,
        mul_mem' := (_ : ∀ {a b : M}, a ∈ setOf IsUnit → b ∈ setOf IsUnit → a * b ∈ setOf IsUnit) }.carrier
[PROOFSTEP]
simp only [isUnit_one, Set.mem_setOf_eq]
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ submonoid M ↔ IsUnit a
[PROOFSTEP]
change a ∈ setOf IsUnit ↔ IsUnit a
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ setOf IsUnit ↔ IsUnit a
[PROOFSTEP]
rw [Set.mem_setOf_eq]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.38168
N : Type ?u.38171
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x * y) = f x * f y
x y : M
⊢ f (1 * y) = f 1 * f y
[PROOFSTEP]
rw [one_mul, h1, one_mul]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.38168
N : Type ?u.38171
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
⊢ f (a * b * y) = f (a * b) * f y
[PROOFSTEP]
rw [mul_assoc, ha, ha, hb, mul_assoc]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.40855
N : Type ?u.40858
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x y : M
⊢ ∀ (x : M),
    OneHom.toFun { toFun := f, map_one' := h1 } (x * 1) =
      OneHom.toFun { toFun := f, map_one' := h1 } x * OneHom.toFun { toFun := f, map_one' := h1 } 1
[PROOFSTEP]
simp [h1]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.40855
N : Type ?u.40858
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x✝ y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ OneHom.toFun { toFun := f, map_one' := h1 } (x * (y₁ * y₂)) =
    OneHom.toFun { toFun := f, map_one' := h1 } x * OneHom.toFun { toFun := f, map_one' := h1 } (y₁ * y₂)
[PROOFSTEP]
simp [← mul_assoc, h₁, h₂]


[GOAL]
M : Type u_1
inst✝ : CommMonoid M
src✝ : Group { x // x ∈ IsUnit.submonoid M } := inferInstanceAs (Group { x // x ∈ IsUnit.submonoid M })
a b : { x // x ∈ IsUnit.submonoid M }
⊢ a * b = b * a
[PROOFSTEP]
convert mul_comm a b
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
a _b : M
x✝¹ : a ∈ {x | ∃ y, x * ↑y = 1}
x✝ : _b ∈ {x | ∃ y, x * ↑y = 1}
a' : { x // x ∈ S }
ha : a * ↑a' = 1
b' : { x // x ∈ S }
hb : _b * ↑b' = 1
⊢ a * _b * ↑(b' * a') = 1
[PROOFSTEP]
simp only [coe_mul, ← mul_assoc, mul_assoc a, hb, mul_one, ha]
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
⊢ leftInv (leftInv S) ≤ S
[PROOFSTEP]
rintro x ⟨⟨y, z, h₁⟩, h₂ : x * y = 1⟩
[GOAL]
case intro.mk.intro
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : { x // x ∈ S }
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x ∈ S
[PROOFSTEP]
convert z.prop
[GOAL]
case h.e'_4
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : { x // x ∈ S }
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x = ↑z
[PROOFSTEP]
rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ leftInv (leftInv S) = S
[PROOFSTEP]
refine' le_antisymm S.leftInv_leftInv_le _
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S ≤ leftInv (leftInv S)
[PROOFSTEP]
intro x hx
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x ∈ leftInv (leftInv S)
[PROOFSTEP]
have : x = ((hS hx).unit⁻¹⁻¹ : Mˣ) := by
  rw [inv_inv (hS hx).unit]
  rfl
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹
[PROOFSTEP]
rw [inv_inv (hS hx).unit]
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹
⊢ x ∈ leftInv (leftInv S)
[PROOFSTEP]
rw [this]
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹
⊢ ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹ ∈ leftInv (leftInv S)
[PROOFSTEP]
exact S.leftInv.unit_mem_leftInv _ (S.unit_mem_leftInv _ hx)
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : { x // x ∈ leftInv S }
⊢ ↑(fromLeftInv S x) * ↑x = 1
[PROOFSTEP]
rw [mul_comm, mul_fromLeftInv]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : { x // x ∈ leftInv S }
b : M
⊢ ↑(fromLeftInv S a) = b ↔ ↑a * b = 1
[PROOFSTEP]
rw [← IsUnit.mul_right_inj (leftInv_le_isUnit _ a.prop), S.mul_fromLeftInv, eq_comm]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : { x // x ∈ leftInv S }
⊢ ↑(OneHom.toFun { toFun := fromLeftInv S, map_one' := (_ : fromLeftInv S 1 = 1) } (x * y)) =
    ↑(OneHom.toFun { toFun := fromLeftInv S, map_one' := (_ : fromLeftInv S 1 = 1) } x *
        OneHom.toFun { toFun := fromLeftInv S, map_one' := (_ : fromLeftInv S 1 = 1) } y)
[PROOFSTEP]
rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ← mul_assoc (x : M),
  mul_fromLeftInv, one_mul, mul_fromLeftInv]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ { x // x ∈ leftInv S }
[PROOFSTEP]
choose x' hx using hS x.prop
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
x' : Mˣ
hx : ↑x' = ↑x
⊢ { x // x ∈ leftInv S }
[PROOFSTEP]
exact ⟨x'.inv, x, hx ▸ x'.inv_val⟩
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
⊢ ↑((fun x =>
          (fun x' hx => { val := x'.inv, property := (_ : ∃ y, x'.inv * ↑y = 1) })
            (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M))
            (_ : ↑(Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)) = ↑x))
        (OneHom.toFun (↑src✝) x)) =
    ↑x
[PROOFSTEP]
dsimp only
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
⊢ (Classical.choose (_ : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M)).inv = ↑x
[PROOFSTEP]
generalize_proofs h
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
⊢ (Classical.choose h).inv = ↑x
[PROOFSTEP]
rw [← h.choose.mul_left_inj]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
⊢ (Classical.choose h).inv * ↑(Exists.choose h) = ↑x * ↑(Exists.choose h)
[PROOFSTEP]
conv => rhs; rw [h.choose_spec]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
| (Classical.choose h).inv * ↑(Exists.choose h) = ↑x * ↑(Exists.choose h)
[PROOFSTEP]
rhs; rw [h.choose_spec]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
| (Classical.choose h).inv * ↑(Exists.choose h) = ↑x * ↑(Exists.choose h)
[PROOFSTEP]
rhs; rw [h.choose_spec]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
| (Classical.choose h).inv * ↑(Exists.choose h) = ↑x * ↑(Exists.choose h)
[PROOFSTEP]
rhs
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
| ↑x * ↑(Exists.choose h)
[PROOFSTEP]
rw [h.choose_spec]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
⊢ (Classical.choose h).inv * ↑(Exists.choose h) = ↑x * ↑(OneHom.toFun (↑(fromCommLeftInv S)) x)
[PROOFSTEP]
exact h.choose.inv_val.trans (S.mul_fromLeftInv x).symm
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ OneHom.toFun (↑src✝)
      ((fun x =>
          (fun x' hx => { val := x'.inv, property := (_ : ∃ y, x'.inv * ↑y = 1) })
            (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M))
            (_ : ↑(Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)) = ↑x))
        x) =
    x
[PROOFSTEP]
dsimp only [fromCommLeftInv]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ fromLeftInv S
      { val := (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv,
        property := (_ : ∃ y, (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv * ↑y = 1) } =
    x
[PROOFSTEP]
ext
[GOAL]
case a
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ ↑(fromLeftInv S
        { val := (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv,
          property := (_ : ∃ y, (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv * ↑y = 1) }) =
    ↑x
[PROOFSTEP]
rw [fromLeftInv_eq_iff]
[GOAL]
case a
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ ↑{ val := (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv,
          property := (_ : ∃ y, (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv * ↑y = 1) } *
      ↑x =
    1
[PROOFSTEP]
convert (hS x.prop).choose.inv_val
[GOAL]
case h.e'_2.h.e'_6
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ ↑x = ↑(Exists.choose (_ : ↑x ∈ IsUnit.submonoid M))
[PROOFSTEP]
exact (hS x.prop).choose_spec.symm
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ leftInv S }
⊢ ↑(↑(leftInvEquiv S hS) x) * ↑x = 1
[PROOFSTEP]
simpa only [leftInvEquiv_apply, fromCommLeftInv] using fromLeftInv_mul S x
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ leftInv S }
⊢ ↑x * ↑(↑(leftInvEquiv S hS) x) = 1
[PROOFSTEP]
simp only [leftInvEquiv_apply, fromCommLeftInv, mul_fromLeftInv]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ ↑(↑(MulEquiv.symm (leftInvEquiv S hS)) x) * ↑x = 1
[PROOFSTEP]
convert S.mul_leftInvEquiv hS ((S.leftInvEquiv hS).symm x)
[GOAL]
case h.e'_2.h.e'_6.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ x = ↑(leftInvEquiv S hS) (↑(MulEquiv.symm (leftInvEquiv S hS)) x)
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ ↑x * ↑(↑(MulEquiv.symm (leftInvEquiv S hS)) x) = 1
[PROOFSTEP]
convert S.leftInvEquiv_mul hS ((S.leftInvEquiv hS).symm x)
[GOAL]
case h.e'_2.h.e'_5.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ x = ↑(leftInvEquiv S hS) (↑(MulEquiv.symm (leftInvEquiv S hS)) x)
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝ : Group M
S : Submonoid M
x : { x // x ∈ leftInv S }
⊢ ↑(fromLeftInv S x) = (↑x)⁻¹
[PROOFSTEP]
rw [← mul_right_inj (x : M), mul_right_inv, mul_fromLeftInv]
[GOAL]
M : Type u_1
inst✝ : CommGroup M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ ↑(↑(MulEquiv.symm (leftInvEquiv S hS)) x) = (↑x)⁻¹
[PROOFSTEP]
rw [← mul_right_inj (x : M), mul_right_inv, mul_leftInvEquiv_symm]