[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f g : X →[M'] Y
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
g : X →[M'] Y
toFun✝ : X → Y
map_smul'✝ : ∀ (m : M') (x : X), toFun✝ (m • x) = m • toFun✝ x
h : { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_smul' := map_smul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
toFun✝¹ : X → Y
map_smul'✝¹ : ∀ (m : M') (x : X), toFun✝¹ (m • x) = m • toFun✝¹ x
toFun✝ : X → Y
map_smul'✝ : ∀ (m : M') (x : X), toFun✝ (m • x) = m • toFun✝ x
h : { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }.toFun = { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } = { toFun := toFun✝, map_smul' := map_smul'✝ }
[PROOFSTEP]
congr
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
g : Y →[M'] Z
f : X →[M'] Y
m : M'
x : X
⊢ ↑g (↑f (m • x)) = ↑g (m • ↑f x)
[PROOFSTEP]
rw [f.map_smul]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f : X →[M'] Y
x : X
⊢ ↑(comp (MulActionHom.id M') f) x = ↑f x
[PROOFSTEP]
rw [comp_apply, id_apply]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f : X →[M'] Y
x : X
⊢ ↑(comp f (MulActionHom.id M')) x = ↑f x
[PROOFSTEP]
rw [comp_apply, id_apply]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f : A →[M] B
g : B → A
h₁ : Function.LeftInverse g ↑f
h₂ : Function.RightInverse g ↑f
m : M
x : B
⊢ g (m • x) = g (m • ↑f (g x))
[PROOFSTEP]
rw [h₂]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f : A →[M] B
g : B → A
h₁ : Function.LeftInverse g ↑f
h₂ : Function.RightInverse g ↑f
m : M
x : B
⊢ g (m • ↑f (g x)) = g (↑f (m • g x))
[PROOFSTEP]
rw [f.map_smul]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f : A →[M] B
g : B → A
h₁ : Function.LeftInverse g ↑f
h₂ : Function.RightInverse g ↑f
m : M
x : B
⊢ g (↑f (m • g x)) = m • g x
[PROOFSTEP]
rw [h₁]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f g : A →+[M] B
h : (fun m => m.toFun) f = (fun m => m.toFun) g
⊢ f = g
[PROOFSTEP]
rcases f with ⟨tF, _, _⟩
[GOAL]
case mk
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
g : A →+[M] B
tF : A →[M] B
map_zero'✝ : MulActionHom.toFun tF 0 = 0
map_add'✝ : ∀ (x y : A), MulActionHom.toFun tF (x + y) = MulActionHom.toFun tF x + MulActionHom.toFun tF y
h : (fun m => m.toFun) { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ } = (fun m => m.toFun) g
⊢ { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
[PROOFSTEP]
rcases g with ⟨tG, _, _⟩
[GOAL]
case mk.mk
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
tF : A →[M] B
map_zero'✝¹ : MulActionHom.toFun tF 0 = 0
map_add'✝¹ : ∀ (x y : A), MulActionHom.toFun tF (x + y) = MulActionHom.toFun tF x + MulActionHom.toFun tF y
tG : A →[M] B
map_zero'✝ : MulActionHom.toFun tG 0 = 0
map_add'✝ : ∀ (x y : A), MulActionHom.toFun tG (x + y) = MulActionHom.toFun tG x + MulActionHom.toFun tG y
h :
  (fun m => m.toFun) { toMulActionHom := tF, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun m => m.toFun) { toMulActionHom := tG, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ { toMulActionHom := tF, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    { toMulActionHom := tG, map_zero' := map_zero'✝, map_add' := map_add'✝ }
[PROOFSTEP]
cases tF
[GOAL]
case mk.mk.mk
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
tG : A →[M] B
map_zero'✝¹ : MulActionHom.toFun tG 0 = 0
map_add'✝¹ : ∀ (x y : A), MulActionHom.toFun tG (x + y) = MulActionHom.toFun tG x + MulActionHom.toFun tG y
toFun✝ : A → B
map_smul'✝ : ∀ (m : M) (x : A), toFun✝ (m • x) = m • toFun✝ x
map_zero'✝ : MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } 0 = 0
map_add'✝ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } (x + y) =
      MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } x +
        MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } y
h :
  (fun m => m.toFun)
      { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
        map_add' := map_add'✝ } =
    (fun m => m.toFun) { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }
⊢ { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝, map_add' := map_add'✝ } =
    { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }
[PROOFSTEP]
cases tG
[GOAL]
case mk.mk.mk.mk
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
toFun✝¹ : A → B
map_smul'✝¹ : ∀ (m : M) (x : A), toFun✝¹ (m • x) = m • toFun✝¹ x
map_zero'✝¹ : MulActionHom.toFun { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } (x + y) =
      MulActionHom.toFun { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } x +
        MulActionHom.toFun { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } y
toFun✝ : A → B
map_smul'✝ : ∀ (m : M) (x : A), toFun✝ (m • x) = m • toFun✝ x
map_zero'✝ : MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } 0 = 0
map_add'✝ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } (x + y) =
      MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } x +
        MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } y
h :
  (fun m => m.toFun)
      { toMulActionHom := { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
        map_add' := map_add'✝¹ } =
    (fun m => m.toFun)
      { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ { toMulActionHom := { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
      map_add' := map_add'✝¹ } =
    { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝, map_add' := map_add'✝ }
[PROOFSTEP]
congr
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f g : A →+[M] B
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
ext a
[GOAL]
case a
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f g : A →+[M] B
h : ↑f = ↑g
a : A
⊢ ↑f a = ↑g a
[PROOFSTEP]
exact MulActionHom.congr_fun h a
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f g : A →+[M] B
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
ext a
[GOAL]
case a
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f g : A →+[M] B
h : ↑f = ↑g
a : A
⊢ ↑f a = ↑g a
[PROOFSTEP]
exact FunLike.congr_fun h a
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
x : A
⊢ ↑(DistribMulActionHom.id M) x = x
[PROOFSTEP]
rfl
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
src✝ : A →+ B := 0
m : M
x✝ : A
⊢ ZeroHom.toFun (↑src✝) (m • x✝) = m • ZeroHom.toFun (↑src✝) x✝
[PROOFSTEP]
change (0 : B) = m • (0 : B)
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
src✝ : A →+ B := 0
m : M
x✝ : A
⊢ 0 = m • 0
[PROOFSTEP]
rw [smul_zero]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f : A →+[M] B
x : A
⊢ ↑(comp (DistribMulActionHom.id M) f) x = ↑f x
[PROOFSTEP]
rw [comp_apply, id_apply]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f : A →+[M] B
x : A
⊢ ↑(comp f (DistribMulActionHom.id M)) x = ↑f x
[PROOFSTEP]
rw [comp_apply, id_apply]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²⁵ : SMul M' X
Y : Type u_3
inst✝²⁴ : SMul M' Y
Z : Type u_4
inst✝²³ : SMul M' Z
M : Type u_5
inst✝²² : Monoid M
A : Type u_6
inst✝²¹ : AddMonoid A
inst✝²⁰ : DistribMulAction M A
A' : Type u_7
inst✝¹⁹ : AddGroup A'
inst✝¹⁸ : DistribMulAction M A'
B : Type u_8
inst✝¹⁷ : AddMonoid B
inst✝¹⁶ : DistribMulAction M B
B' : Type u_9
inst✝¹⁵ : AddGroup B'
inst✝¹⁴ : DistribMulAction M B'
C : Type u_10
inst✝¹³ : AddMonoid C
inst✝¹² : DistribMulAction M C
R : Type u_11
inst✝¹¹ : Semiring R
inst✝¹⁰ : MulSemiringAction M R
R' : Type u_12
inst✝⁹ : Ring R'
inst✝⁸ : MulSemiringAction M R'
S : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : MulSemiringAction M S
S' : Type u_14
inst✝⁵ : Ring S'
inst✝⁴ : MulSemiringAction M S'
T : Type u_15
inst✝³ : Semiring T
inst✝² : MulSemiringAction M T
inst✝¹ : AddMonoid M'
inst✝ : DistribMulAction R M'
f g : R →+[R] M'
h : ↑f 1 = ↑g 1
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case a
M' : Type u_1
X : Type u_2
inst✝²⁵ : SMul M' X
Y : Type u_3
inst✝²⁴ : SMul M' Y
Z : Type u_4
inst✝²³ : SMul M' Z
M : Type u_5
inst✝²² : Monoid M
A : Type u_6
inst✝²¹ : AddMonoid A
inst✝²⁰ : DistribMulAction M A
A' : Type u_7
inst✝¹⁹ : AddGroup A'
inst✝¹⁸ : DistribMulAction M A'
B : Type u_8
inst✝¹⁷ : AddMonoid B
inst✝¹⁶ : DistribMulAction M B
B' : Type u_9
inst✝¹⁵ : AddGroup B'
inst✝¹⁴ : DistribMulAction M B'
C : Type u_10
inst✝¹³ : AddMonoid C
inst✝¹² : DistribMulAction M C
R : Type u_11
inst✝¹¹ : Semiring R
inst✝¹⁰ : MulSemiringAction M R
R' : Type u_12
inst✝⁹ : Ring R'
inst✝⁸ : MulSemiringAction M R'
S : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : MulSemiringAction M S
S' : Type u_14
inst✝⁵ : Ring S'
inst✝⁴ : MulSemiringAction M S'
T : Type u_15
inst✝³ : Semiring T
inst✝² : MulSemiringAction M T
inst✝¹ : AddMonoid M'
inst✝ : DistribMulAction R M'
f g : R →+[R] M'
h : ↑f 1 = ↑g 1
x : R
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [← mul_one x, ← smul_eq_mul R, f.map_smul, g.map_smul, h]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f g : R →+*[M] S
h : (fun m => m.toFun) f = (fun m => m.toFun) g
⊢ f = g
[PROOFSTEP]
rcases f with ⟨⟨tF, _, _⟩, _, _⟩
[GOAL]
case mk.mk
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
g : R →+*[M] S
tF : R →[M] S
map_zero'✝ : MulActionHom.toFun tF 0 = 0
map_add'✝ : ∀ (x y : R), MulActionHom.toFun tF (x + y) = MulActionHom.toFun tF x + MulActionHom.toFun tF y
map_one'✝ :
  MulActionHom.toFun { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toMulActionHom 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    MulActionHom.toFun { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toMulActionHom (x * y) =
      MulActionHom.toFun { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toMulActionHom x *
        MulActionHom.toFun { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toMulActionHom y
h :
  (fun m => m.toFun)
      { toDistribMulActionHom := { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ },
        map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    (fun m => m.toFun) g
⊢ { toDistribMulActionHom := { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ },
      map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    g
[PROOFSTEP]
rcases g with ⟨⟨tG, _, _⟩, _, _⟩
[GOAL]
case mk.mk.mk.mk
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
tF : R →[M] S
map_zero'✝¹ : MulActionHom.toFun tF 0 = 0
map_add'✝¹ : ∀ (x y : R), MulActionHom.toFun tF (x + y) = MulActionHom.toFun tF x + MulActionHom.toFun tF y
map_one'✝¹ :
  MulActionHom.toFun { toMulActionHom := tF, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toMulActionHom 1 = 1
map_mul'✝¹ :
  ∀ (x y : R),
    MulActionHom.toFun { toMulActionHom := tF, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun { toMulActionHom := tF, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toMulActionHom x *
        MulActionHom.toFun { toMulActionHom := tF, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toMulActionHom y
tG : R →[M] S
map_zero'✝ : MulActionHom.toFun tG 0 = 0
map_add'✝ : ∀ (x y : R), MulActionHom.toFun tG (x + y) = MulActionHom.toFun tG x + MulActionHom.toFun tG y
map_one'✝ :
  MulActionHom.toFun { toMulActionHom := tG, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toMulActionHom 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    MulActionHom.toFun { toMulActionHom := tG, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toMulActionHom (x * y) =
      MulActionHom.toFun { toMulActionHom := tG, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toMulActionHom x *
        MulActionHom.toFun { toMulActionHom := tG, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toMulActionHom y
h :
  (fun m => m.toFun)
      { toDistribMulActionHom := { toMulActionHom := tF, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
        map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun m => m.toFun)
      { toDistribMulActionHom := { toMulActionHom := tG, map_zero' := map_zero'✝, map_add' := map_add'✝ },
        map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toDistribMulActionHom := { toMulActionHom := tF, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
      map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toDistribMulActionHom := { toMulActionHom := tG, map_zero' := map_zero'✝, map_add' := map_add'✝ },
      map_one' := map_one'✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
cases tF
[GOAL]
case mk.mk.mk.mk.mk
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
tG : R →[M] S
map_zero'✝¹ : MulActionHom.toFun tG 0 = 0
map_add'✝¹ : ∀ (x y : R), MulActionHom.toFun tG (x + y) = MulActionHom.toFun tG x + MulActionHom.toFun tG y
map_one'✝¹ :
  MulActionHom.toFun { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toMulActionHom 1 = 1
map_mul'✝¹ :
  ∀ (x y : R),
    MulActionHom.toFun { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toMulActionHom x *
        MulActionHom.toFun { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toMulActionHom y
toFun✝ : R → S
map_smul'✝ : ∀ (m : M) (x : R), toFun✝ (m • x) = m • toFun✝ x
map_zero'✝ : MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } 0 = 0
map_add'✝ :
  ∀ (x y : R),
    MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } (x + y) =
      MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } x +
        MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } y
map_one'✝ :
  MulActionHom.toFun
      { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
          map_add' := map_add'✝ }.toMulActionHom
      1 =
    1
map_mul'✝ :
  ∀ (x y : R),
    MulActionHom.toFun
        { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
            map_add' := map_add'✝ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          y
h :
  (fun m => m.toFun)
      {
        toDistribMulActionHom :=
          { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
            map_add' := map_add'✝ },
        map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    (fun m => m.toFun)
      { toDistribMulActionHom := { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
        map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }
⊢ {
      toDistribMulActionHom :=
        { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
          map_add' := map_add'✝ },
      map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    { toDistribMulActionHom := { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
      map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }
[PROOFSTEP]
cases tG
[GOAL]
case mk.mk.mk.mk.mk.mk
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
toFun✝¹ : R → S
map_smul'✝¹ : ∀ (m : M) (x : R), toFun✝¹ (m • x) = m • toFun✝¹ x
map_zero'✝¹ : MulActionHom.toFun { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } 0 = 0
map_add'✝¹ :
  ∀ (x y : R),
    MulActionHom.toFun { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } (x + y) =
      MulActionHom.toFun { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } x +
        MulActionHom.toFun { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } y
map_one'✝¹ :
  MulActionHom.toFun
      { toMulActionHom := { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
          map_add' := map_add'✝¹ }.toMulActionHom
      1 =
    1
map_mul'✝¹ :
  ∀ (x y : R),
    MulActionHom.toFun
        { toMulActionHom := { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
            map_add' := map_add'✝¹ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ }.toMulActionHom
          y
toFun✝ : R → S
map_smul'✝ : ∀ (m : M) (x : R), toFun✝ (m • x) = m • toFun✝ x
map_zero'✝ : MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } 0 = 0
map_add'✝ :
  ∀ (x y : R),
    MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } (x + y) =
      MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } x +
        MulActionHom.toFun { toFun := toFun✝, map_smul' := map_smul'✝ } y
map_one'✝ :
  MulActionHom.toFun
      { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
          map_add' := map_add'✝ }.toMulActionHom
      1 =
    1
map_mul'✝ :
  ∀ (x y : R),
    MulActionHom.toFun
        { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
            map_add' := map_add'✝ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          y
h :
  (fun m => m.toFun)
      {
        toDistribMulActionHom :=
          { toMulActionHom := { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
            map_add' := map_add'✝¹ },
        map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun m => m.toFun)
      {
        toDistribMulActionHom :=
          { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
            map_add' := map_add'✝ },
        map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ {
      toDistribMulActionHom :=
        { toMulActionHom := { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
          map_add' := map_add'✝¹ },
      map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    {
      toDistribMulActionHom :=
        { toMulActionHom := { toFun := toFun✝, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
          map_add' := map_add'✝ },
      map_one' := map_one'✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f : R →+*[M] S
x : R
⊢ ↑(comp (MulSemiringActionHom.id M) f) x = ↑f x
[PROOFSTEP]
rw [comp_apply, id_apply]
[GOAL]
M' : Type u_1
X : Type u_2
inst✝²³ : SMul M' X
Y : Type u_3
inst✝²² : SMul M' Y
Z : Type u_4
inst✝²¹ : SMul M' Z
M : Type u_5
inst✝²⁰ : Monoid M
A : Type u_6
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type u_7
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_8
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type u_9
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type u_10
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_11
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_12
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_13
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type u_14
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type u_15
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f : R →+*[M] S
x : R
⊢ ↑(comp f (MulSemiringActionHom.id M)) x = ↑f x
[PROOFSTEP]
rw [comp_apply, id_apply]


[GOAL]
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsLeftRegular (a * b)
⊢ Function.Injective (?m.3122 ab ∘ fun x => b * x)
[PROOFSTEP]
rwa [comp_mul_left a b]
[GOAL]
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
⊢ IsRightRegular b
[PROOFSTEP]
refine' fun x y xy => ab (_ : x * (b * a) = y * (b * a))
[GOAL]
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x => x * b) x = (fun x => x * b) y
⊢ x * (b * a) = y * (b * a)
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc]
[GOAL]
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x => x * b) x = (fun x => x * b) y
⊢ x * b * a = y * b * a
[PROOFSTEP]
exact congr_fun (congr_arg (· * ·) xy) a
[GOAL]
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b
[PROOFSTEP]
rintro ⟨ab, ba⟩
[GOAL]
case refine'_1.intro
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRegular (a * b)
ba : IsRegular (b * a)
⊢ IsRegular a ∧ IsRegular b
[PROOFSTEP]
exact
  ⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
    ⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case refine'_2.intro
R : Type u_1
inst✝ : Semigroup R
a b : R
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a * b) ∧ IsRegular (b * a)
[PROOFSTEP]
exact
  ⟨⟨(mul_isLeftRegular_iff _ ha.left).mpr hb.left, (mul_isRightRegular_iff _ hb.right).mpr ha.right⟩,
    ⟨(mul_isLeftRegular_iff _ hb.left).mpr ha.left, (mul_isRightRegular_iff _ ha.right).mpr hb.right⟩⟩
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ ¬IsLeftRegular 0 ↔ Nontrivial R
[PROOFSTEP]
rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y
[PROOFSTEP]
push_neg
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ ¬IsRightRegular 0 ↔ Nontrivial R
[PROOFSTEP]
rw [nontrivial_iff, not_iff_comm, isRightRegular_zero_iff_subsingleton, subsingleton_iff]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y
[PROOFSTEP]
push_neg
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
inst✝¹ : MulZeroClass R
a b : R
inst✝ : Nontrivial R
la : IsLeftRegular a
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
la : IsLeftRegular 0
⊢ False
[PROOFSTEP]
rcases exists_pair_ne R with ⟨x, y, xy⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ False
[PROOFSTEP]
refine'
  xy
    (la (_ : 0 * x = 0 * y))
      -- Porting note: lean4 seems to need the type signature
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ 0 * x = 0 * y
[PROOFSTEP]
rw [zero_mul, zero_mul]
[GOAL]
R : Type u_1
inst✝¹ : MulZeroClass R
a b : R
inst✝ : Nontrivial R
ra : IsRightRegular a
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
⊢ False
[PROOFSTEP]
rcases exists_pair_ne R with ⟨x, y, xy⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ False
[PROOFSTEP]
refine' xy (ra (_ : x * 0 = y * 0))
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ x * 0 = y * 0
[PROOFSTEP]
rw [mul_zero, mul_zero]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = 0 ↔ a = 0
[PROOFSTEP]
nth_rw 1 [← mul_zero b]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = b * 0 ↔ a = 0
[PROOFSTEP]
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha, mul_zero]⟩
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
ha : a = 0
⊢ b * a = b * 0
[PROOFSTEP]
rw [ha, mul_zero]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 ↔ a = 0
[PROOFSTEP]
nth_rw 1 [← zero_mul b]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 * b ↔ a = 0
[PROOFSTEP]
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha, zero_mul]⟩
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
ha : a = 0
⊢ a * b = 0 * b
[PROOFSTEP]
rw [ha, zero_mul]
[GOAL]
R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b
[PROOFSTEP]
refine' Iff.trans _ isRegular_mul_and_mul_iff
[GOAL]
R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)
[PROOFSTEP]
refine' ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩
[GOAL]
R : Type u_1
inst✝ : CommSemigroup R
a b : R
ab : IsRegular (a * b)
⊢ IsRegular (b * a)
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular (?m.12942 h * a)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1
[PROOFSTEP]
exact isRegular_one.left
[GOAL]
R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular (a * ?m.13480 h)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular 1
[PROOFSTEP]
exact isRegular_one.right
[GOAL]
R : Type u_1
inst✝ : Monoid R
a b : R
ua : IsUnit a
⊢ IsRegular a
[PROOFSTEP]
rcases ua with ⟨a, rfl⟩
[GOAL]
case intro
R : Type u_1
inst✝ : Monoid R
b : R
a : Rˣ
⊢ IsRegular ↑a
[PROOFSTEP]
exact Units.isRegular a


[GOAL]
α : Type u_1
inst✝¹ : Group α
inst✝ : HasDistribNeg α
a : α
⊢ (-a)⁻¹ = -a⁻¹
[PROOFSTEP]
rw [eq_comm, eq_inv_iff_mul_eq_one, neg_mul, mul_neg, neg_neg, mul_left_inv]
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
[PROOFSTEP]
have : c = x * (b - x) := (eq_neg_of_add_eq_zero_right h).trans (by simp [mul_sub, mul_comm])
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
⊢ -(x * x - b * x) = x * (b - x)
[PROOFSTEP]
simp [mul_sub, mul_comm]
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
[PROOFSTEP]
refine' ⟨b - x, _, by simp, by rw [this]⟩
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x + (b - x) = b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x * (b - x) = c
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ (b - x) * (b - x) - b * (b - x) + c = 0
[PROOFSTEP]
rw [this, sub_add, ← sub_mul, sub_self]
[GOAL]
α : Type u_1
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a + 1 = a
⊢ a + 1 = a + 0
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a - 1 = a
⊢ a + -1 = a + -0
[PROOFSTEP]
simp [← sub_eq_add_neg, h]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : x = 0
⊢ x = 0 ∨ y = 0
case neg α : Type u_1 inst✝¹ : Ring α inst✝ : IsLeftCancelMulZero α x y : α h : x * y = 0 hx : ¬x = 0 ⊢ x = 0 ∨ y = 0
[PROOFSTEP]
{ left
  exact hx
}
[GOAL]
case pos
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : x = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
left
[GOAL]
case pos.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : x = 0
⊢ x = 0
[PROOFSTEP]
exact hx
[GOAL]
case neg
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : ¬x = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
{ right
  rw [← sub_zero (x * y), ← mul_zero x, ← mul_sub] at h
  have := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero) hx h
  rwa [sub_zero] at this
}
[GOAL]
case neg
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : ¬x = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
right
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : ¬x = 0
⊢ y = 0
[PROOFSTEP]
rw [← sub_zero (x * y), ← mul_zero x, ← mul_sub] at h
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * (y - 0) = x * 0
hx : ¬x = 0
⊢ y = 0
[PROOFSTEP]
have := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero) hx h
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * (y - 0) = x * 0
hx : ¬x = 0
this : y - 0 = 0
⊢ y = 0
[PROOFSTEP]
rwa [sub_zero] at this
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : y = 0
⊢ x = 0 ∨ y = 0
case neg α : Type u_1 inst✝¹ : Ring α inst✝ : IsRightCancelMulZero α x y : α h : x * y = 0 hy : ¬y = 0 ⊢ x = 0 ∨ y = 0
[PROOFSTEP]
{ right
  exact hy
}
[GOAL]
case pos
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
right
[GOAL]
case pos.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : y = 0
⊢ y = 0
[PROOFSTEP]
exact hy
[GOAL]
case neg
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
{ left
  rw [← sub_zero (x * y), ← zero_mul y, ← sub_mul] at h
  have := (IsRightCancelMulZero.mul_right_cancel_of_ne_zero) hy h
  rwa [sub_zero] at this
}
[GOAL]
case neg
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
left
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : ¬y = 0
⊢ x = 0
[PROOFSTEP]
rw [← sub_zero (x * y), ← zero_mul y, ← sub_mul] at h
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : (x - 0) * y = 0 * y
hy : ¬y = 0
⊢ x = 0
[PROOFSTEP]
have := (IsRightCancelMulZero.mul_right_cancel_of_ne_zero) hy h
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : (x - 0) * y = 0 * y
hy : ¬y = 0
this : x - 0 = 0
⊢ x = 0
[PROOFSTEP]
rwa [sub_zero] at this
[GOAL]
α : Type ?u.21715
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
a✝ b✝ c✝ : α
ha : a✝ ≠ 0
h : a✝ * b✝ = a✝ * c✝
⊢ b✝ = c✝
[PROOFSTEP]
rw [← sub_eq_zero, ← mul_sub] at h
[GOAL]
α : Type ?u.21715
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
a✝ b✝ c✝ : α
ha : a✝ ≠ 0
h✝ : a✝ * b✝ = a✝ * c✝
h : a✝ * (b✝ - c✝) = 0
⊢ b✝ = c✝
[PROOFSTEP]
exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left ha)
[GOAL]
α : Type ?u.21715
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
a✝ b✝ c✝ : α
hb : b✝ ≠ 0
h : a✝ * b✝ = c✝ * b✝
⊢ a✝ = c✝
[PROOFSTEP]
rw [← sub_eq_zero, ← sub_mul] at h
[GOAL]
α : Type ?u.21715
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
a✝ b✝ c✝ : α
hb : b✝ ≠ 0
h✝ : a✝ * b✝ = c✝ * b✝
h : (a✝ - c✝) * b✝ = 0
⊢ a✝ = c✝
[PROOFSTEP]
exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hb)


[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Distrib R
a x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x + x') (y + y')
[PROOFSTEP]
simp only [SemiconjBy, left_distrib, right_distrib, h.eq, h'.eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Distrib R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a + b) x y
[PROOFSTEP]
simp only [SemiconjBy, left_distrib, right_distrib, ha.eq, hb.eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy a (-x) (-y)
[PROOFSTEP]
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy (-a) x y
[PROOFSTEP]
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing R
a b x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x - x') (y - y')
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h.add_right h'.neg_right
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing R
a b x y x' y' : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a - b) x y
[PROOFSTEP]
simpa only [sub_eq_add_neg] using ha.add_left hb.neg_left


[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
R : Type u_9
M : Type u_10
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
r : R
neZero : NeZero (↑f r)
h : r = 0
⊢ ↑f r = 0
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
R : Type u_9
M : Type u_10
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
r : R
neZero : NeZero (↑f r)
h : r = 0
⊢ ↑f 0 = 0
[PROOFSTEP]
exact ZeroHomClass.map_zero f
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
R : Type u_9
M : Type u_10
inst✝³ : Zero R
r : R
inst✝² : NeZero r
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
hf : Function.Injective ↑f
⊢ ↑f r ≠ 0
[PROOFSTEP]
rw [← ZeroHomClass.map_zero f]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
R : Type u_9
M : Type u_10
inst✝³ : Zero R
r : R
inst✝² : NeZero r
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
hf : Function.Injective ↑f
⊢ ↑f r ≠ ↑f 0
[PROOFSTEP]
exact hf.ne NeZero.out
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : One M
inst✝ : One N
f g : OneHom M N
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : One M
inst✝ : One N
g : OneHom M N
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝, map_one' := map_one'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_one' := map_one'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : One M
inst✝ : One N
toFun✝¹ : M → N
map_one'✝¹ : toFun✝¹ 1 = 1
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun = { toFun := toFun✝, map_one' := map_one'✝ }.toFun
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹ } = { toFun := toFun✝, map_one' := map_one'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : Mul N
f g : M →ₙ* N
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : Mul N
g : M →ₙ* N
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_mul' := map_mul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : Mul N
toFun✝¹ : M → N
map_mul'✝¹ : ∀ (x y : M), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun = { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } = { toFun := toFun✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f g : M →* N
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
g : M →* N
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
h : (fun f => f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ } = (fun f => f.toFun) g
⊢ { toOneHom := toOneHom✝, map_mul' := map_mul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), OneHom.toFun toOneHom✝¹ (x * y) = OneHom.toFun toOneHom✝¹ x * OneHom.toFun toOneHom✝¹ y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
h :
  (fun f => f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } = { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toOneHom
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), OneHom.toFun toOneHom✝¹ (x * y) = OneHom.toFun toOneHom✝¹ x * OneHom.toFun toOneHom✝¹ y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
h :
  (fun f => f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ toOneHom✝¹ = toOneHom✝
[PROOFSTEP]
apply FunLike.coe_injective'
[GOAL]
case mk.mk.e_toOneHom.a
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), OneHom.toFun toOneHom✝¹ (x * y) = OneHom.toFun toOneHom✝¹ x * OneHom.toFun toOneHom✝¹ y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
h :
  (fun f => f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ ↑toOneHom✝¹ = ↑toOneHom✝
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ ↑f a * ↑f b = 1
[PROOFSTEP]
rw [← map_mul, h, map_one]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (a : G), ↑f a⁻¹ = (↑f a)⁻¹
a b : G
⊢ ↑f (a / b) = ↑f a / ↑f b
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, map_mul, hf]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
a b : G
⊢ ↑f (a * b⁻¹) = ↑f a * (↑f b)⁻¹
[PROOFSTEP]
rw [map_mul, map_inv]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
⊢ ↑f (a ^ 0) = ↑f a ^ 0
[PROOFSTEP]
rw [pow_zero, pow_zero, map_one]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
n : ℕ
⊢ ↑f (a ^ (n + 1)) = ↑f a ^ (n + 1)
[PROOFSTEP]
rw [pow_succ, pow_succ, map_mul, map_pow f a n]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), ↑f x⁻¹ = (↑f x)⁻¹
a : G
n : ℕ
⊢ ↑f (a ^ ↑n) = ↑f a ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, map_pow, zpow_ofNat]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), ↑f x⁻¹ = (↑f x)⁻¹
a : G
n : ℕ
⊢ ↑f (a ^ Int.negSucc n) = ↑f a ^ Int.negSucc n
[PROOFSTEP]
rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc, ← zpow_negSucc]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
f g : M →*₀ N
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
g : M →*₀ N
toZeroHom✝ : ZeroHom M N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h : (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = (fun f => f.toFun) g
⊢ { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
toZeroHom✝¹ : ZeroHom M N
map_one'✝¹ : ZeroHom.toFun toZeroHom✝¹ 1 = 1
map_mul'✝¹ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝¹ (x * y) = ZeroHom.toFun toZeroHom✝¹ x * ZeroHom.toFun toZeroHom✝¹ y
toZeroHom✝ : ZeroHom M N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h :
  (fun f => f.toFun) { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toZeroHom
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
toZeroHom✝¹ : ZeroHom M N
map_one'✝¹ : ZeroHom.toFun toZeroHom✝¹ 1 = 1
map_mul'✝¹ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝¹ (x * y) = ZeroHom.toFun toZeroHom✝¹ x * ZeroHom.toFun toZeroHom✝¹ y
toZeroHom✝ : ZeroHom M N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h :
  (fun f => f.toFun) { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ toZeroHom✝¹ = toZeroHom✝
[PROOFSTEP]
apply FunLike.coe_injective'
[GOAL]
case mk.mk.e_toZeroHom.a
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
toZeroHom✝¹ : ZeroHom M N
map_one'✝¹ : ZeroHom.toFun toZeroHom✝¹ 1 = 1
map_mul'✝¹ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝¹ (x * y) = ZeroHom.toFun toZeroHom✝¹ x * ZeroHom.toFun toZeroHom✝¹ y
toZeroHom✝ : ZeroHom M N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h :
  (fun f => f.toFun) { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ ↑toZeroHom✝¹ = ↑toZeroHom✝
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
hnp : OneHom N P
hmn : OneHom M N
⊢ (↑hnp ∘ ↑hmn) 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
hnp : N →ₙ* P
hmn : M →ₙ* N
x y : M
⊢ (↑hnp ∘ ↑hmn) (x * y) = (↑hnp ∘ ↑hmn) x * (↑hnp ∘ ↑hmn) y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
hnp : N →* P
hmn : M →* N
⊢ (↑hnp ∘ ↑hmn) 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
hnp : N →* P
hmn : M →* N
⊢ ∀ (x y : M),
    OneHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_one' := (_ : ↑hnp (↑hmn 1) = 1) } (x * y) =
      OneHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_one' := (_ : ↑hnp (↑hmn 1) = 1) } x *
        OneHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_one' := (_ : ↑hnp (↑hmn 1) = 1) } y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulZeroOneClass M
inst✝¹ : MulZeroOneClass N
inst✝ : MulZeroOneClass P
hnp : N →*₀ P
hmn : M →*₀ N
⊢ (↑hnp ∘ ↑hmn) 0 = 0
[PROOFSTEP]
rw [Function.comp_apply, map_zero, map_zero]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulZeroOneClass M
inst✝¹ : MulZeroOneClass N
inst✝ : MulZeroOneClass P
hnp : N →*₀ P
hmn : M →*₀ N
⊢ ZeroHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_zero' := (_ : (↑hnp ∘ ↑hmn) 0 = 0) } 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulZeroOneClass M
inst✝¹ : MulZeroOneClass N
inst✝ : MulZeroOneClass P
hnp : N →*₀ P
hmn : M →*₀ N
⊢ ∀ (x y : M),
    ZeroHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_zero' := (_ : (↑hnp ∘ ↑hmn) 0 = 0) } (x * y) =
      ZeroHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_zero' := (_ : (↑hnp ∘ ↑hmn) 0 = 0) } x *
        ZeroHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_zero' := (_ : (↑hnp ∘ ↑hmn) 0 = 0) } y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Function.Injective ↑g
h : comp g f₁ = comp g f₂
x : M
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← OneHom.comp_apply, h, OneHom.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
hg : Function.Injective ↑g
h : comp g f₁ = comp g f₂
x : M
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← MulHom.comp_apply, h, MulHom.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
g : N →* P
f₁ f₂ : M →* N
hg : Function.Injective ↑g
h : comp g f₁ = comp g f₂
x : M
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulZeroOneClass M
inst✝¹ : MulZeroOneClass N
inst✝ : MulZeroOneClass P
g : N →*₀ P
f₁ f₂ : M →*₀ N
hg : Function.Injective ↑g
h : comp g f₁ = comp g f₂
x : M
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← MonoidWithZeroHom.comp_apply, h, MonoidWithZeroHom.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
⊢ comp f 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
x✝ : M
⊢ ↑(comp f 1) x✝ = ↑1 x✝
[PROOFSTEP]
simp only [OneHom.map_one, OneHom.coe_comp, Function.comp_apply, OneHom.one_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ (fun m => ↑f m * ↑g m) (x * y) = (fun m => ↑f m * ↑g m) x * (fun m => ↑f m * ↑g m) y
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ (fun m => ↑f m * ↑g m) (x * y) = (fun m => ↑f m * ↑g m) x * (fun m => ↑f m * ↑g m) y
[PROOFSTEP]
show f (x * y) * g (x * y) = f x * g x * (f y * g y)
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ ↑f (x * y) * ↑g (x * y) = ↑f x * ↑g x * (↑f y * ↑g y)
[PROOFSTEP]
rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
⊢ comp g (f₁ * f₂) = comp g f₁ * comp g f₂
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
x✝ : M
⊢ ↑(comp g (f₁ * f₂)) x✝ = ↑(comp g f₁ * comp g f₂) x✝
[PROOFSTEP]
simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H
M : Type ?u.198672
N : Type ?u.198675
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
⊢ ↑f 1 * ↑g 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H
M : Type ?u.198672
N : Type ?u.198675
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } (x * y) =
    OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } x *
      OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } y
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H
M : Type ?u.198672
N : Type ?u.198675
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } (x * y) =
    OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } x *
      OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } y
[PROOFSTEP]
show f (x * y) * g (x * y) = f x * g x * (f y * g y)
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H
M : Type ?u.198672
N : Type ?u.198675
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ ↑f (x * y) * ↑g (x * y) = ↑f x * ↑g x * (↑f y * ↑g y)
[PROOFSTEP]
rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
⊢ comp f 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
x✝ : M
⊢ ↑(comp f 1) x✝ = ↑1 x✝
[PROOFSTEP]
simp only [map_one, coe_comp, Function.comp_apply, one_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
⊢ comp g (f₁ * f₂) = comp g f₁ * comp g f₂
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
x✝ : M
⊢ ↑(comp g (f₁ * f₂)) x✝ = ↑(comp g f₁ * comp g f₂) x✝
[PROOFSTEP]
simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H
inst✝¹ : Group α
inst✝ : DivisionMonoid β
f : α →* β
g h : α
⊢ ↑f (g * h⁻¹) = ↑f g * (↑f h)⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G✝ : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝⁴ : Group G✝
inst✝³ : CommGroup H✝
G : Type u_9
H : Type u_10
inst✝² : Group G
inst✝¹ : MulOneClass H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), ↑f a = 1 → a = 1
x y : G
hxy : ↑f x = ↑f y
⊢ ↑f (x * y⁻¹) = 1
[PROOFSTEP]
rw [map_mul, hxy, ← map_mul, mul_inv_self, map_one]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : Group G
inst✝¹ : CommGroup H
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f 1 * ?m.224335 f map_mul = ?m.224335 f map_mul
[PROOFSTEP]
rw [← map_mul, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f (x * y) = f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹
[PROOFSTEP]
{simp only [one_mul, inv_one, ← map_div, inv_inv]
}
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f (x * y) = f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹
[PROOFSTEP]
simp only [one_mul, inv_one, ← map_div, inv_inv]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹ = f x * f y
[PROOFSTEP]
{ simp only [map_div]
  simp only [mul_right_inv, one_mul, inv_inv]
}
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹ = f x * f y
[PROOFSTEP]
simp only [map_div]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f 1 * (f 1)⁻¹ * (f y)⁻¹)⁻¹ = f x * f y
[PROOFSTEP]
simp only [mul_right_inv, one_mul, inv_inv]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
hf : ∀ (x y : G), f (x / y) = f x / f y
⊢ ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G✝ : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G✝
inst✝³ : CommGroup H
inst✝² : MulOneClass M✝
M : Type ?u.229390
G : Type ?u.229393
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
f : M →* G
a b : M
⊢ (↑f (a * b))⁻¹ = (↑f a)⁻¹ * (↑f b)⁻¹
[PROOFSTEP]
rw [← mul_inv, f.map_mul]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_9
N : Type u_10
A : Type u_11
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommGroup A
φ : N →* A
ψ : M →* N
⊢ comp φ⁻¹ ψ = (comp φ ψ)⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_9
N : Type u_10
A : Type u_11
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommGroup A
φ : N →* A
ψ : M →* N
x✝ : M
⊢ ↑(comp φ⁻¹ ψ) x✝ = ↑(comp φ ψ)⁻¹ x✝
[PROOFSTEP]
simp only [Function.comp_apply, inv_apply, coe_comp]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_9
A : Type u_10
B : Type u_11
inst✝² : MulOneClass M
inst✝¹ : CommGroup A
inst✝ : CommGroup B
φ : A →* B
ψ : M →* A
⊢ comp φ ψ⁻¹ = (comp φ ψ)⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_9
A : Type u_10
B : Type u_11
inst✝² : MulOneClass M
inst✝¹ : CommGroup A
inst✝ : CommGroup B
φ : A →* B
ψ : M →* A
x✝ : M
⊢ ↑(comp φ ψ⁻¹) x✝ = ↑(comp φ ψ)⁻¹ x✝
[PROOFSTEP]
simp only [Function.comp_apply, inv_apply, map_inv, coe_comp]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G✝ : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G✝
inst✝³ : CommGroup H
inst✝² : MulOneClass M✝
M : Type ?u.233732
G : Type ?u.233735
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
f g : M →* G
a b : M
⊢ ↑f (a * b) / ↑g (a * b) = ↑f a / ↑g a * (↑f b / ↑g b)
[PROOFSTEP]
simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : CommMonoidWithZero N
f g : M →*₀ N
src✝ : M →* N := ↑f * ↑g
⊢ (fun a => ↑f a * ↑g a) 0 = 0
[PROOFSTEP]
dsimp only []
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : CommMonoidWithZero N
f g : M →*₀ N
src✝ : M →* N := ↑f * ↑g
⊢ ↑f 0 * ↑g 0 = 0
[PROOFSTEP]
rw [map_zero, zero_mul]