[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]
