[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
⊢ Function.Injective fun f => f.toFun
[PROOFSTEP]
rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h
[GOAL]
case mk.mk.mk.mk.mk.mk
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A → B
map_smul'✝¹ : ∀ (m : R) (x : A), f (m • x) = m • f x
map_zero'✝¹ : MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } (x + y) =
      MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } x +
        MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } y
map_mul'✝¹ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
            map_add' := map_add'✝¹ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ }.toMulActionHom
          y
g : A → B
map_smul'✝ : ∀ (m : R) (x : A), g (m • x) = m • g x
map_zero'✝ : MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } 0 = 0
map_add'✝ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } (x + y) =
      MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } x +
        MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } y
map_mul'✝ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
            map_add' := map_add'✝ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          y
h :
  (fun f => f.toFun)
      {
        toDistribMulActionHom :=
          { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
            map_add' := map_add'✝¹ },
        map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun)
      {
        toDistribMulActionHom :=
          { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝, map_add' := map_add'✝ },
        map_mul' := map_mul'✝ }
⊢ {
      toDistribMulActionHom :=
        { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
          map_add' := map_add'✝¹ },
      map_mul' := map_mul'✝¹ } =
    {
      toDistribMulActionHom :=
        { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝, map_add' := map_add'✝ },
      map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
⊢ Function.Injective FunLike.coe
[PROOFSTEP]
rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h
[GOAL]
case mk.mk.mk.mk.mk.mk
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A → B
map_smul'✝¹ : ∀ (m : R) (x : A), f (m • x) = m • f x
map_zero'✝¹ : MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } (x + y) =
      MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } x +
        MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } y
map_mul'✝¹ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
            map_add' := map_add'✝¹ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ }.toMulActionHom
          y
g : A → B
map_smul'✝ : ∀ (m : R) (x : A), g (m • x) = m • g x
map_zero'✝ : MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } 0 = 0
map_add'✝ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } (x + y) =
      MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } x +
        MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } y
map_mul'✝ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
            map_add' := map_add'✝ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          y
h :
  ↑{
        toDistribMulActionHom :=
          { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
            map_add' := map_add'✝¹ },
        map_mul' := map_mul'✝¹ } =
    ↑{
        toDistribMulActionHom :=
          { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝, map_add' := map_add'✝ },
        map_mul' := map_mul'✝ }
⊢ {
      toDistribMulActionHom :=
        { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
          map_add' := map_add'✝¹ },
      map_mul' := map_mul'✝¹ } =
    {
      toDistribMulActionHom :=
        { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝, map_add' := map_add'✝ },
      map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f g : A →ₙₐ[R] B
⊢ f = g → ∀ (x : A), ↑f x = ↑g x
[PROOFSTEP]
rintro rfl x
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
x : A
⊢ ↑f x = ↑f x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x
h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0
h₃ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) =
      MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y
h₄ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y
⊢ { toDistribMulActionHom := { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
      map_mul' := h₄ } =
    f
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f g : A →ₙₐ[R] B
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f g : A →ₙₐ[R] B
h : ↑f = ↑g
a : A
⊢ ↑f a = ↑g a
[PROOFSTEP]
exact DistribMulActionHom.congr_fun h a
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f g : A →ₙₐ[R] B
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f g : A →ₙₐ[R] B
h : ↑f = ↑g
a : A
⊢ ↑f a = ↑g a
[PROOFSTEP]
exact FunLike.congr_fun h a
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x
h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0
h₃ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) =
      MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y
h₄ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y
⊢ ↑{ toDistribMulActionHom := { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
        map_mul' := h₄ } =
    { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x
h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0
h₃ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) =
      MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y
h₄ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y
⊢ ↑{ toDistribMulActionHom := { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
        map_mul' := h₄ } =
    { toFun := ↑f, map_mul' := h₄ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
src✝ : A →+[R] B := 0
⊢ ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := src✝.toMulActionHom, map_zero' := (_ : MulActionHom.toFun src✝.toMulActionHom 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  MulActionHom.toFun src✝.toMulActionHom (x + y) =
                    MulActionHom.toFun src✝.toMulActionHom x +
                      MulActionHom.toFun src✝.toMulActionHom y) }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := src✝.toMulActionHom, map_zero' := (_ : MulActionHom.toFun src✝.toMulActionHom 0 = 0),
              map_add' :=
                (_ :
                  ∀ (x y : A),
                    MulActionHom.toFun src✝.toMulActionHom (x + y) =
                      MulActionHom.toFun src✝.toMulActionHom x +
                        MulActionHom.toFun src✝.toMulActionHom y) }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := src✝.toMulActionHom, map_zero' := (_ : MulActionHom.toFun src✝.toMulActionHom 0 = 0),
              map_add' :=
                (_ :
                  ∀ (x y : A),
                    MulActionHom.toFun src✝.toMulActionHom (x + y) =
                      MulActionHom.toFun src✝.toMulActionHom x +
                        MulActionHom.toFun src✝.toMulActionHom y) }.toMulActionHom
          y
[PROOFSTEP]
simp
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
c : R
x : A
⊢ Pi.prod (↑f) (↑g) (c • x) = c • Pi.prod (↑f) (↑g) x
[PROOFSTEP]
simp only [Pi.prod, Prod.smul_mk, map_smul, RingHom.id_apply]
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ MulActionHom.toFun
      { toFun := Pi.prod ↑f ↑g, map_smul' := (_ : ∀ (c : R) (x : A), (↑f (c • x), ↑g (c • x)) = (c • ↑f x, c • ↑g x)) }
      0 =
    0
[PROOFSTEP]
simp only [Pi.prod, Prod.zero_eq_mk, map_zero]
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
x y : A
⊢ MulActionHom.toFun
      { toFun := Pi.prod ↑f ↑g, map_smul' := (_ : ∀ (c : R) (x : A), (↑f (c • x), ↑g (c • x)) = (c • ↑f x, c • ↑g x)) }
      (x + y) =
    MulActionHom.toFun
        { toFun := Pi.prod ↑f ↑g,
          map_smul' := (_ : ∀ (c : R) (x : A), (↑f (c • x), ↑g (c • x)) = (c • ↑f x, c • ↑g x)) }
        x +
      MulActionHom.toFun
        { toFun := Pi.prod ↑f ↑g,
          map_smul' := (_ : ∀ (c : R) (x : A), (↑f (c • x), ↑g (c • x)) = (c • ↑f x, c • ↑g x)) }
        y
[PROOFSTEP]
simp only [Pi.prod, Prod.mk_add_mk, map_add]
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
x y : A
⊢ MulActionHom.toFun
      {
          toMulActionHom :=
            { toFun := Pi.prod ↑f ↑g,
              map_smul' := (_ : ∀ (c : R) (x : A), (↑f (c • x), ↑g (c • x)) = (c • ↑f x, c • ↑g x)) },
          map_zero' := (_ : (↑f 0, ↑g 0) = (0, 0)),
          map_add' := (_ : ∀ (x y : A), (↑f (x + y), ↑g (x + y)) = (↑f x + ↑f y, ↑g x + ↑g y)) }.toMulActionHom
      (x * y) =
    MulActionHom.toFun
        {
            toMulActionHom :=
              { toFun := Pi.prod ↑f ↑g,
                map_smul' := (_ : ∀ (c : R) (x : A), (↑f (c • x), ↑g (c • x)) = (c • ↑f x, c • ↑g x)) },
            map_zero' := (_ : (↑f 0, ↑g 0) = (0, 0)),
            map_add' := (_ : ∀ (x y : A), (↑f (x + y), ↑g (x + y)) = (↑f x + ↑f y, ↑g x + ↑g y)) }.toMulActionHom
        x *
      MulActionHom.toFun
        {
            toMulActionHom :=
              { toFun := Pi.prod ↑f ↑g,
                map_smul' := (_ : ∀ (c : R) (x : A), (↑f (c • x), ↑g (c • x)) = (c • ↑f x, c • ↑g x)) },
            map_zero' := (_ : (↑f 0, ↑g 0) = (0, 0)),
            map_add' := (_ : ∀ (x y : A), (↑f (x + y), ↑g (x + y)) = (↑f x + ↑f y, ↑g x + ↑g y)) }.toMulActionHom
        y
[PROOFSTEP]
simp only [Pi.prod, Prod.mk_mul_mk, map_mul]
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ comp (fst R B C) (prod f g) = f
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ comp (snd R B C) (prod f g) = g
[PROOFSTEP]
rfl


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
e f : R ≃+* S
h₁ : (fun f => f.toFun) e = (fun f => f.toFun) f
h₂ : (fun f => f.invFun) e = (fun f => f.invFun) f
⊢ e = f
[PROOFSTEP]
cases e
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
f : R ≃+* S
toEquiv✝ : R ≃ S
map_mul'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
map_add'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x + y) = Equiv.toFun toEquiv✝ x + Equiv.toFun toEquiv✝ y
h₁ : (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ } = (fun f => f.toFun) f
h₂ : (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ } = (fun f => f.invFun) f
⊢ { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ } = f
[PROOFSTEP]
cases f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
toEquiv✝¹ : R ≃ S
map_mul'✝¹ : ∀ (x y : R), Equiv.toFun toEquiv✝¹ (x * y) = Equiv.toFun toEquiv✝¹ x * Equiv.toFun toEquiv✝¹ y
map_add'✝¹ : ∀ (x y : R), Equiv.toFun toEquiv✝¹ (x + y) = Equiv.toFun toEquiv✝¹ x + Equiv.toFun toEquiv✝¹ y
toEquiv✝ : R ≃ S
map_mul'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
map_add'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x + y) = Equiv.toFun toEquiv✝ x + Equiv.toFun toEquiv✝ y
h₁ :
  (fun f => f.toFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
h₂ :
  (fun f => f.invFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
⊢ { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toEquiv
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
toEquiv✝¹ : R ≃ S
map_mul'✝¹ : ∀ (x y : R), Equiv.toFun toEquiv✝¹ (x * y) = Equiv.toFun toEquiv✝¹ x * Equiv.toFun toEquiv✝¹ y
map_add'✝¹ : ∀ (x y : R), Equiv.toFun toEquiv✝¹ (x + y) = Equiv.toFun toEquiv✝¹ x + Equiv.toFun toEquiv✝¹ y
toEquiv✝ : R ≃ S
map_mul'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
map_add'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x + y) = Equiv.toFun toEquiv✝ x + Equiv.toFun toEquiv✝ y
h₁ :
  (fun f => f.toFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
h₂ :
  (fun f => f.invFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
⊢ toEquiv✝¹ = toEquiv✝
[PROOFSTEP]
apply Equiv.coe_fn_injective h₁
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
α : Type ?u.47054
β : Type ?u.47060
inst✝³ : Add α
inst✝² : Mul α
inst✝¹ : Add β
inst✝ : Mul β
f : α ≃+* β
⊢ (fun f =>
        let src := ↑AddEquiv.mulOp.symm (toAddEquiv f);
        let src_1 := ↑MulEquiv.op.symm (toMulEquiv f);
        { toEquiv := src.toEquiv,
          map_mul' :=
            (_ :
              ∀ (x y : α),
                Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
          map_add' :=
            (_ :
              ∀ (x y : α), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
      ((fun f =>
          let src := ↑AddEquiv.mulOp (toAddEquiv f);
          let src_1 := ↑MulEquiv.op (toMulEquiv f);
          { toEquiv := src.toEquiv,
            map_mul' :=
              (_ :
                ∀ (x y : αᵐᵒᵖ),
                  Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
            map_add' :=
              (_ :
                ∀ (x y : αᵐᵒᵖ),
                  Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
α : Type ?u.47054
β : Type ?u.47060
inst✝³ : Add α
inst✝² : Mul α
inst✝¹ : Add β
inst✝ : Mul β
f : α ≃+* β
x✝ : α
⊢ ↑((fun f =>
            let src := ↑AddEquiv.mulOp.symm (toAddEquiv f);
            let src_1 := ↑MulEquiv.op.symm (toMulEquiv f);
            { toEquiv := src.toEquiv,
              map_mul' :=
                (_ :
                  ∀ (x y : α),
                    Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
              map_add' :=
                (_ :
                  ∀ (x y : α),
                    Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
          ((fun f =>
              let src := ↑AddEquiv.mulOp (toAddEquiv f);
              let src_1 := ↑MulEquiv.op (toMulEquiv f);
              { toEquiv := src.toEquiv,
                map_mul' :=
                  (_ :
                    ∀ (x y : αᵐᵒᵖ),
                      Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
                map_add' :=
                  (_ :
                    ∀ (x y : αᵐᵒᵖ),
                      Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
            f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
α : Type ?u.47054
β : Type ?u.47060
inst✝³ : Add α
inst✝² : Mul α
inst✝¹ : Add β
inst✝ : Mul β
f : αᵐᵒᵖ ≃+* βᵐᵒᵖ
⊢ (fun f =>
        let src := ↑AddEquiv.mulOp (toAddEquiv f);
        let src_1 := ↑MulEquiv.op (toMulEquiv f);
        { toEquiv := src.toEquiv,
          map_mul' :=
            (_ :
              ∀ (x y : αᵐᵒᵖ),
                Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
          map_add' :=
            (_ :
              ∀ (x y : αᵐᵒᵖ),
                Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
      ((fun f =>
          let src := ↑AddEquiv.mulOp.symm (toAddEquiv f);
          let src_1 := ↑MulEquiv.op.symm (toMulEquiv f);
          { toEquiv := src.toEquiv,
            map_mul' :=
              (_ :
                ∀ (x y : α),
                  Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
            map_add' :=
              (_ :
                ∀ (x y : α), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
α : Type ?u.47054
β : Type ?u.47060
inst✝³ : Add α
inst✝² : Mul α
inst✝¹ : Add β
inst✝ : Mul β
f : αᵐᵒᵖ ≃+* βᵐᵒᵖ
x✝ : αᵐᵒᵖ
⊢ ↑((fun f =>
            let src := ↑AddEquiv.mulOp (toAddEquiv f);
            let src_1 := ↑MulEquiv.op (toMulEquiv f);
            { toEquiv := src.toEquiv,
              map_mul' :=
                (_ :
                  ∀ (x y : αᵐᵒᵖ),
                    Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
              map_add' :=
                (_ :
                  ∀ (x y : αᵐᵒᵖ),
                    Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
          ((fun f =>
              let src := ↑AddEquiv.mulOp.symm (toAddEquiv f);
              let src_1 := ↑MulEquiv.op.symm (toMulEquiv f);
              { toEquiv := src.toEquiv,
                map_mul' :=
                  (_ :
                    ∀ (x y : α),
                      Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
                map_add' :=
                  (_ :
                    ∀ (x y : α),
                      Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
            f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R ≃+* S
x✝ y x : R
⊢ ↑f x = -1 ↔ x = -1
[PROOFSTEP]
rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R✝ : Type u_4
S✝ : Type u_5
S' : Type u_6
inst✝⁴ : NonUnitalNonAssocSemiring R✝
inst✝³ : NonUnitalNonAssocSemiring S✝
inst✝² : NonUnitalNonAssocSemiring S'
R : Type u_7
S : Type u_8
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑f = ↑g
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
⊢ NonUnitalRingHom.comp (toNonUnitalRingHom e) (toNonUnitalRingHom (RingEquiv.symm e)) = NonUnitalRingHom.id S
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
x✝ : S
⊢ ↑(NonUnitalRingHom.comp (toNonUnitalRingHom e) (toNonUnitalRingHom (RingEquiv.symm e))) x✝ =
    ↑(NonUnitalRingHom.id S) x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
⊢ NonUnitalRingHom.comp (toNonUnitalRingHom (RingEquiv.symm e)) (toNonUnitalRingHom e) = NonUnitalRingHom.id R
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
x✝ : R
⊢ ↑(NonUnitalRingHom.comp (toNonUnitalRingHom (RingEquiv.symm e)) (toNonUnitalRingHom e)) x✝ =
    ↑(NonUnitalRingHom.id R) x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R✝ : Type u_4
S✝ : Type u_5
S' : Type u_6
inst✝⁴ : NonAssocSemiring R✝
inst✝³ : NonAssocSemiring S✝
inst✝² : NonAssocSemiring S'
R : Type u_7
S : Type u_8
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑f = ↑g
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
⊢ RingHom.comp (toRingHom e) (toRingHom (RingEquiv.symm e)) = RingHom.id S
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
x✝ : S
⊢ ↑(RingHom.comp (toRingHom e) (toRingHom (RingEquiv.symm e))) x✝ = ↑(RingHom.id S) x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
⊢ RingHom.comp (toRingHom (RingEquiv.symm e)) (toRingHom e) = RingHom.id R
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
x✝ : R
⊢ ↑(RingHom.comp (toRingHom (RingEquiv.symm e)) (toRingHom e)) x✝ = ↑(RingHom.id R) x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
A : Type u_7
B : Type u_8
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
x y : A
⊢ ↑e (x * y) = ↑e (y * x)
[PROOFSTEP]
rw [map_mul, map_mul, hB.mul_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
A : Type u_7
B : Type u_8
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
a✝ : A
h : a✝ ≠ 0
⊢ ∃ b, a✝ * b = 1
[PROOFSTEP]
obtain ⟨a', he⟩ := hB.mul_inv_cancel ((e.injective.ne h).trans_eq <| map_zero e)
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
A : Type u_7
B : Type u_8
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
a✝ : A
h : a✝ ≠ 0
a' : B
he : ↑e a✝ * a' = 1
⊢ ∃ b, a✝ * b = 1
[PROOFSTEP]
exact ⟨e.symm a', e.injective <| by rw [map_mul, map_one, e.apply_symm_apply, he]⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
A : Type u_7
B : Type u_8
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
a✝ : A
h : a✝ ≠ 0
a' : B
he : ↑e a✝ * a' = 1
⊢ ↑e (a✝ * ↑(symm e) a') = ↑e 1
[PROOFSTEP]
rw [map_mul, map_one, e.apply_symm_apply, he]


[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
rla : IsLeftRegular a
⊢ IsLeftRegular (a ^ n)
[PROOFSTEP]
simp only [IsLeftRegular, ← mul_left_iterate, rla.iterate n]
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
rra : IsRightRegular a
⊢ IsRightRegular (a ^ n)
[PROOFSTEP]
rw [IsRightRegular, ← mul_right_iterate]
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective (fun x => x * a)^[n]
[PROOFSTEP]
exact rra.iterate n
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n) ↔ IsLeftRegular a
[PROOFSTEP]
refine' ⟨_, IsLeftRegular.pow n⟩
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n) → IsLeftRegular a
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ']
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ Nat.pred n * a) → IsLeftRegular a
[PROOFSTEP]
exact IsLeftRegular.of_mul
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) ↔ IsRightRegular a
[PROOFSTEP]
refine' ⟨_, IsRightRegular.pow n⟩
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) → IsRightRegular a
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ]
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ Nat.pred n) → IsRightRegular a
[PROOFSTEP]
exact IsRightRegular.of_mul


[GOAL]
M N : GroupWithZeroCat
f g : M ⟶ N
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
M N : GroupWithZeroCat
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
M N : GroupWithZeroCat
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
M N : GroupWithZeroCat
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
M N : GroupWithZeroCat
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]
α β : GroupWithZeroCat
e : ↑α ≃* ↑β
⊢ ↑e ≫ ↑(MulEquiv.symm e) = 𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : GroupWithZeroCat
e : ↑α ≃* ↑β
x✝ : (forget GroupWithZeroCat).obj α
⊢ ↑(↑e ≫ ↑(MulEquiv.symm e)) x✝ = ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : GroupWithZeroCat
e : ↑α ≃* ↑β
⊢ ↑(MulEquiv.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : GroupWithZeroCat
e : ↑α ≃* ↑β
x✝ : (forget GroupWithZeroCat).obj β
⊢ ↑(↑(MulEquiv.symm e) ≫ ↑e) x✝ = ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
α : Type u
inst✝ : MulZeroClass α
x✝ : ULift α
⊢ ↑Equiv.ulift (0 * x✝) = ↑Equiv.ulift 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : MulZeroClass α
x✝ : ULift α
⊢ ↑Equiv.ulift (x✝ * 0) = ↑Equiv.ulift 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Distrib α
x✝² x✝¹ x✝ : ULift α
⊢ ↑Equiv.ulift (x✝² * (x✝¹ + x✝)) = ↑Equiv.ulift (x✝² * x✝¹ + x✝² * x✝)
[PROOFSTEP]
simp [left_distrib]
[GOAL]
α : Type u
inst✝ : Distrib α
x✝² x✝¹ x✝ : ULift α
⊢ ↑Equiv.ulift ((x✝² + x✝¹) * x✝) = ↑Equiv.ulift (x✝² * x✝ + x✝¹ * x✝)
[PROOFSTEP]
simp [right_distrib]


[GOAL]
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
⊢ HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)
[PROOFSTEP]
suffices DistribMulAction.toAddMonoidHom R[X] m = (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom
  by
  ext1 r
  exact FunLike.congr_fun this r
[GOAL]
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
this : DistribMulAction.toAddMonoidHom R[X] m = RingHom.toAddMonoidHom (mapRingHom (MulSemiringAction.toRingHom M R m))
⊢ HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)
[PROOFSTEP]
ext1 r
[GOAL]
case h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
this : DistribMulAction.toAddMonoidHom R[X] m = RingHom.toAddMonoidHom (mapRingHom (MulSemiringAction.toRingHom M R m))
r : R[X]
⊢ m • r = map (MulSemiringAction.toRingHom M R m) r
[PROOFSTEP]
exact FunLike.congr_fun this r
[GOAL]
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
⊢ DistribMulAction.toAddMonoidHom R[X] m = RingHom.toAddMonoidHom (mapRingHom (MulSemiringAction.toRingHom M R m))
[PROOFSTEP]
ext n r : 2
[GOAL]
case h.h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
n : ℕ
r : R
⊢ ↑(AddMonoidHom.comp (DistribMulAction.toAddMonoidHom R[X] m) (LinearMap.toAddMonoidHom (monomial n))) r =
    ↑(AddMonoidHom.comp (RingHom.toAddMonoidHom (mapRingHom (MulSemiringAction.toRingHom M R m)))
          (LinearMap.toAddMonoidHom (monomial n)))
      r
[PROOFSTEP]
change m • monomial n r = map (MulSemiringAction.toRingHom M R m) (monomial n r)
[GOAL]
case h.h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
n : ℕ
r : R
⊢ m • ↑(monomial n) r = map (MulSemiringAction.toRingHom M R m) (↑(monomial n) r)
[PROOFSTEP]
rw [Polynomial.map_monomial, Polynomial.smul_monomial, MulSemiringAction.toRingHom_apply]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
R : Type u_2
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x r : S
⊢ eval (m • x) (m • ↑C r) = m • eval x (↑C r)
[PROOFSTEP]
rw [smul_C, eval_C, eval_C]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
R : Type u_2
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f✝ : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)
[PROOFSTEP]
rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
R : Type u_2
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (↑C r * X ^ n)) = m • eval x (↑C r * X ^ n)
⊢ eval (m • x) (m • (↑C r * X ^ (n + 1))) = m • eval x (↑C r * X ^ (n + 1))
[PROOFSTEP]
rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_pow, eval_X, eval_mul, eval_C, eval_pow, eval_X,
  smul_mul', smul_pow']
[GOAL]
M : Type u_1
inst✝⁶ : Monoid M
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : MulSemiringAction M R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : MulSemiringAction M S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval (g • x) f = g • eval x (g⁻¹ • f)
[PROOFSTEP]
rw [← smul_eval_smul, smul_inv_smul]
[GOAL]
M : Type u_1
inst✝⁶ : Monoid M
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : MulSemiringAction M R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : MulSemiringAction M S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval x (g • f) = g • eval (g⁻¹ • x) f
[PROOFSTEP]
rw [← smul_eval_smul, smul_inv_smul]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
⊢ ↑↑↑(aeval x) (X - ↑C (ofQuotientStabilizer G x ↑1)) = 0
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
g' : G ⧸ stabilizer G x
⊢ g • (X - ↑C (ofQuotientStabilizer G x g')) = X - ↑C (ofQuotientStabilizer G x ((fun x_1 x_2 => x_1 • x_2) g g'))
[PROOFSTEP]
rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
n : ℕ
⊢ g • Polynomial.coeff (prodXSubSmul G R x) n = Polynomial.coeff (prodXSubSmul G R x) n
[PROOFSTEP]
rw [← Polynomial.coeff_smul, prodXSubSmul.smul]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
⊢ map (↑g) (m • ↑C b) = m • map (↑g) (↑C b)
[PROOFSTEP]
rw [smul_C, map_C, coe_fn_coe, g.map_smul, map_C, coe_fn_coe, smul_C]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p✝ p q : P[X]
ihp : map (↑g) (m • p) = m • map (↑g) p
ihq : map (↑g) (m • q) = m • map (↑g) q
⊢ map (↑g) (m • (p + q)) = m • map (↑g) (p + q)
[PROOFSTEP]
rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (↑C b * X ^ n)) = m • map (↑g) (↑C b * X ^ n)
⊢ map (↑g) (m • (↑C b * X ^ (n + 1))) = m • map (↑g) (↑C b * X ^ (n + 1))
[PROOFSTEP]
rw [smul_mul', smul_C, smul_pow', smul_X, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X, coe_fn_coe, g.map_smul,
  Polynomial.map_mul, map_C, Polynomial.map_pow, map_X, smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]
  -- porting note: added `.toRingHom`


[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
f✝ : R →ₙ+* S
g : R →ₙ+* T
f : R →ₙ+* S × T
x : R
⊢ ↑(NonUnitalRingHom.prod (comp (fst S T) f) (comp (snd S T) f)) x = ↑f x
[PROOFSTEP]
simp only [prod_apply, coe_fst, coe_snd, comp_apply, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
f✝ : R →+* S
g : R →+* T
f : R →+* S × T
x : R
⊢ ↑(RingHom.prod (comp (fst S T) f) (comp (snd S T) f)) x = ↑f x
[PROOFSTEP]
simp only [prod_apply, coe_fst, coe_snd, comp_apply, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
x : R × S
⊢ (fun x => (x, 0)) x.fst = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
fst✝ : R
snd✝ : S
⊢ (fun x => (x, 0)) (fst✝, snd✝).fst = (fst✝, snd✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun x => (x, 0), invFun := Prod.fst,
          left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
          right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
        (x * y) =
      Equiv.toFun
          { toFun := fun x => (x, 0), invFun := Prod.fst,
            left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
            right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
          x *
        Equiv.toFun
          { toFun := fun x => (x, 0), invFun := Prod.fst,
            left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
            right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
          y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun x => (x, 0), invFun := Prod.fst,
          left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
          right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
        (x + y) =
      Equiv.toFun
          { toFun := fun x => (x, 0), invFun := Prod.fst,
            left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
            right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
          x +
        Equiv.toFun
          { toFun := fun x => (x, 0), invFun := Prod.fst,
            left_inv := (_ : ∀ (x : R), ((fun x => (x, 0)) x).fst = ((fun x => (x, 0)) x).fst),
            right_inv := (_ : ∀ (x : R × S), (fun x => (x, 0)) x.fst = x) }
          y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
x : S × R
⊢ (fun x => (0, x)) x.snd = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
fst✝ : S
snd✝ : R
⊢ (fun x => (0, x)) (fst✝, snd✝).snd = (fst✝, snd✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun x => (0, x), invFun := Prod.snd,
          left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
          right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
        (x * y) =
      Equiv.toFun
          { toFun := fun x => (0, x), invFun := Prod.snd,
            left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
            right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
          x *
        Equiv.toFun
          { toFun := fun x => (0, x), invFun := Prod.snd,
            left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
            right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
          y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
S : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun x => (0, x), invFun := Prod.snd,
          left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
          right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
        (x + y) =
      Equiv.toFun
          { toFun := fun x => (0, x), invFun := Prod.snd,
            left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
            right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
          x +
        Equiv.toFun
          { toFun := fun x => (0, x), invFun := Prod.snd,
            left_inv := (_ : ∀ (x : R), ((fun x => (0, x)) x).snd = ((fun x => (0, x)) x).snd),
            right_inv := (_ : ∀ (x : S × R), (fun x => (0, x)) x.snd = x) }
          y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ False
[PROOFSTEP]
have := NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)
[GOAL]
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ (0, 1) * (1, 0) = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : (0, 1) = 0 ∨ (1, 0) = 0
⊢ False
[PROOFSTEP]
rw [Prod.mk_eq_zero, Prod.mk_eq_zero] at this
[GOAL]
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : 0 = 0 ∧ 1 = 0 ∨ 1 = 0 ∧ 0 = 0
⊢ False
[PROOFSTEP]
rcases this with (⟨_, h⟩ | ⟨h, _⟩)
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False
[PROOFSTEP]
exact zero_ne_one h.symm
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
R✝ : Type u_3
R' : Type u_4
S✝ : Type u_5
S' : Type u_6
T : Type u_7
T' : Type u_8
R : Type u_9
S : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False
[PROOFSTEP]
exact zero_ne_one h.symm


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a + a = 0
[PROOFSTEP]
have : a + a = a + a + (a + a) :=
  calc
    a + a = (a + a) * (a + a) := by rw [mul_self]
    _ = a * a + a * a + (a * a + a * a) := by rw [add_mul, mul_add]
    _ = a + a + (a + a) := by rw [mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a + a = (a + a) * (a + a)
[PROOFSTEP]
rw [mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ (a + a) * (a + a) = a * a + a * a + (a * a + a * a)
[PROOFSTEP]
rw [add_mul, mul_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a * a + a * a + (a * a + a * a) = a + a + (a + a)
[PROOFSTEP]
rw [mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
this : a + a = a + a + (a + a)
⊢ a + a = 0
[PROOFSTEP]
rwa [self_eq_add_left] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ -a = -a + 0
[PROOFSTEP]
rw [add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ -a + 0 = -a + -a + a
[PROOFSTEP]
rw [← neg_add_self, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ -a + -a + a = a
[PROOFSTEP]
rw [add_self, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a = -b ↔ a = b
[PROOFSTEP]
rw [neg_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a * b + b * a = 0
[PROOFSTEP]
have : a + b = a + b + (a * b + b * a) :=
  calc
    a + b = (a + b) * (a + b) := by rw [mul_self]
    _ = a * a + a * b + (b * a + b * b) := by rw [add_mul, mul_add, mul_add]
    _ = a + a * b + (b * a + b) := by simp only [mul_self]
    _ = a + b + (a * b + b * a) := by abel
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a + b = (a + b) * (a + b)
[PROOFSTEP]
rw [mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ (a + b) * (a + b) = a * a + a * b + (b * a + b * b)
[PROOFSTEP]
rw [add_mul, mul_add, mul_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a * a + a * b + (b * a + b * b) = a + a * b + (b * a + b)
[PROOFSTEP]
simp only [mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + (b * a + b) = a + b + (a * b + b * a)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + (b * a + b) = a + b + (a * b + b * a)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
this : a + b = a + b + (a * b + b * a)
⊢ a * b + b * a = 0
[PROOFSTEP]
rwa [self_eq_add_right] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a - b = a + b
[PROOFSTEP]
rw [sub_eq_add_neg, add_right_inj, neg_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a * (1 + a) = 0
[PROOFSTEP]
rw [mul_add, mul_one, mul_self, add_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a✝ b✝ : α
src✝ : BooleanRing α := inferInstance
a b : α
⊢ a * b = b * a
[PROOFSTEP]
rw [← add_eq_zero', mul_add_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a ⊔ b = b ⊔ a
[PROOFSTEP]
dsimp only [(· ⊔ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a + b + a * b = b + a + b * a
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a ⊓ b = b ⊓ a
[PROOFSTEP]
dsimp only [(· ⊓ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a * b = b * a
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
[PROOFSTEP]
dsimp only [(· ⊔ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ a + b + a * b + c + (a + b + a * b) * c = a + (b + c + b * c) + a * (b + c + b * c)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
[PROOFSTEP]
dsimp only [(· ⊓ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ a * b * c = a * (b * c)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a ⊔ a ⊓ b = a
[PROOFSTEP]
dsimp only [(· ⊔ ·), (· ⊓ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a + a * b + a * (a * b) = a
[PROOFSTEP]
rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a ⊓ (a ⊔ b) = a
[PROOFSTEP]
dsimp only [(· ⊔ ·), (· ⊓ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a * (a + b + a * b) = a
[PROOFSTEP]
rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ (a + b + a * b) * (a + c + a * c) =
    a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) + (a * b * c + a * a * b * c)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) + (a * b * c + a * a * b * c) =
    a + b * c + a * (b * c)
[PROOFSTEP]
simp only [mul_self, add_self, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c
[PROOFSTEP]
dsimp only [(· ⊔ ·), (· ⊓ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
[PROOFSTEP]
rw [le_sup_inf_aux, add_self, mul_self, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ a * (1 + a) + 0 + a * (1 + a) * 0 = 0
[PROOFSTEP]
norm_num [mul_add, mul_self, add_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ ⊤ ≤ a ⊔ aᶜ
[PROOFSTEP]
change 1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) = a + (1 + a) + a * (1 + a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ 1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) = a + (1 + a) + a * (1 + a)
[PROOFSTEP]
norm_num [mul_add, mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ 1 + (a + (1 + a)) = 0
[PROOFSTEP]
rw [← add_assoc, add_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ a + 1 + a * 1 = 1
[PROOFSTEP]
rw [mul_one, (add_comm a 1), add_assoc, add_self, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ 0 + a + 0 * a = a
[PROOFSTEP]
rw [zero_mul, zero_add, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ (a + b + a * b) * (1 + a * b) = a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b) = a + b
[PROOFSTEP]
simp only [mul_self, add_self, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : AsBoolAlg α
⊢ ↑ofBoolAlg (a ∆ b) = ↑ofBoolAlg a + ↑ofBoolAlg b
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : AsBoolAlg α
⊢ ↑ofBoolAlg ((a ⊔ b) \ (a ⊓ b)) = ↑ofBoolAlg a + ↑ofBoolAlg b
[PROOFSTEP]
exact of_boolalg_symmDiff_aux _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
⊢ (↑toBoolAlg ∘ ↑f ∘ ↑ofBoolAlg) (a ⊔ b) = (↑toBoolAlg ∘ ↑f ∘ ↑ofBoolAlg) a ⊔ (↑toBoolAlg ∘ ↑f ∘ ↑ofBoolAlg) b
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
⊢ ↑toBoolAlg (↑f (↑ofBoolAlg a + ↑ofBoolAlg b + ↑ofBoolAlg a * ↑ofBoolAlg b)) =
    ↑toBoolAlg (↑f (↑ofBoolAlg a)) ⊔ ↑toBoolAlg (↑f (↑ofBoolAlg b))
[PROOFSTEP]
simp_rw [map_add f, map_mul f, toBoolAlg_add_add_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : Bool
⊢ a * 0 = 0
[PROOFSTEP]
cases a
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false * 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true * 0 = 0
[PROOFSTEP]
rfl


[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
s : Fork f 0
⊢ ↑s.pt →+ ↑G
[PROOFSTEP]
exact Fork.ι s
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
s : Fork f 0
c : ↑s.pt
⊢ ↑f (↑(Fork.ι s) c) = 0
[PROOFSTEP]
exact FunLike.congr_fun s.condition c
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
x✝ : Fork f 0
⊢ (fun s => codRestrict (Fork.ι s) (ker f) (_ : ∀ (c : ↑s.pt), ↑(Fork.ι s) c ∈ ker f)) x✝ ≫ Fork.ι (kernelCone f) =
    Fork.ι x✝
[PROOFSTEP]
rfl
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
x✝¹ : Fork f 0
x✝ : x✝¹.pt ⟶ (kernelCone f).pt
h : x✝ ≫ Fork.ι (kernelCone f) = Fork.ι x✝¹
x : ↑x✝¹.pt
⊢ ↑(↑x✝ x) = ↑(↑((fun s => codRestrict (Fork.ι s) (ker f) (_ : ∀ (c : ↑s.pt), ↑(Fork.ι s) c ∈ ker f)) x✝¹) x)
[PROOFSTEP]
exact FunLike.congr_fun h x
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
x✝¹ : Cofork f 0
x✝ : (cokernelCocone f).pt ⟶ x✝¹.pt
h : Cofork.π (cokernelCocone f) ≫ x✝ = Cofork.π x✝¹
this : Epi (Cofork.π (cokernelCocone f))
⊢ ?m.55829 x✝¹ x✝ h this ≫ x✝ =
    ?m.55829 x✝¹ x✝ h this ≫ (fun s => lift (range f) (Cofork.π s) (_ : range f ≤ ker (Cofork.π s))) x✝¹
[PROOFSTEP]
simpa only [parallelPair_obj_one] using h


[GOAL]
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ AddMonoidHom.range f = AddMonoidHom.ker g
[PROOFSTEP]
rw [Abelian.exact_iff' f g (kernelIsLimit _) (cokernelIsColimit _)]
[GOAL]
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g = 0 ∧ Fork.ι (kernelCone g) ≫ Cofork.π (cokernelCocone f) = 0 ↔ AddMonoidHom.range f = AddMonoidHom.ker g
[PROOFSTEP]
exact
  ⟨fun h =>
    ((AddMonoidHom.range_le_ker_iff _ _).mpr h.left).antisymm ((QuotientAddGroup.ker_le_range_iff _ _).mpr h.right),
    fun h => ⟨(AddMonoidHom.range_le_ker_iff _ _).mp h.le, (QuotientAddGroup.ker_le_range_iff _ _).mp h.symm.le⟩⟩
[GOAL]
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ PreservesFiniteLimits colim
[PROOFSTEP]
refine Functor.preservesFiniteLimitsOfMapExact _ fun F G H η γ h => (exact_iff _ _).mpr (le_antisymm ?_ ?_)
[GOAL]
case refine_1
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : Exact η γ
⊢ AddMonoidHom.range (colim.map η) ≤ AddMonoidHom.ker (colim.map γ)
case refine_2
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : Exact η γ
⊢ AddMonoidHom.ker (colim.map γ) ≤ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
all_goals replace h : ∀ j : J, Exact (η.app j) (γ.app j) := fun j => Functor.map_exact ((evaluation _ _).obj j) η γ h
[GOAL]
case refine_1
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : Exact η γ
⊢ AddMonoidHom.range (colim.map η) ≤ AddMonoidHom.ker (colim.map γ)
[PROOFSTEP]
replace h : ∀ j : J, Exact (η.app j) (γ.app j) := fun j => Functor.map_exact ((evaluation _ _).obj j) η γ h
[GOAL]
case refine_2
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : Exact η γ
⊢ AddMonoidHom.ker (colim.map γ) ≤ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
replace h : ∀ j : J, Exact (η.app j) (γ.app j) := fun j => Functor.map_exact ((evaluation _ _).obj j) η γ h
[GOAL]
case refine_1
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
⊢ AddMonoidHom.range (colim.map η) ≤ AddMonoidHom.ker (colim.map γ)
[PROOFSTEP]
rw [AddMonoidHom.range_le_ker_iff, ← comp_def]
[GOAL]
case refine_1
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
⊢ colim.map η ≫ colim.map γ = 0
[PROOFSTEP]
exact colimit.hom_ext fun j => by simp [reassoc_of% (h j).w]
[GOAL]
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
⊢ colimit.ι F j ≫ colim.map η ≫ colim.map γ = colimit.ι F j ≫ 0
[PROOFSTEP]
simp [reassoc_of% (h j).w]
[GOAL]
case refine_2
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
⊢ AddMonoidHom.ker (colim.map γ) ≤ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
intro x (hx : _ = _)
[GOAL]
case refine_2
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
x : ↑(colim.obj G)
hx : ↑(colim.map γ) x = 0
⊢ x ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
rcases Concrete.colimit_exists_rep G x with ⟨j, y, rfl⟩
[GOAL]
case refine_2.intro.intro
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx : ↑(colim.map γ) (↑(colimit.ι G j) y) = 0
⊢ ↑(colimit.ι G j) y ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
erw [← comp_apply, colimit.ι_map, comp_apply, ← map_zero (by exact colimit.ι H j : H.obj j →+ ↑(colimit H))] at hx
[GOAL]
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
⊢ ↑(H.obj j) →+ ↑(colimit H)
[PROOFSTEP]
exact colimit.ι H j
[GOAL]
case refine_2.intro.intro
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
⊢ ↑(colimit.ι G j) y ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
rcases Concrete.colimit_exists_of_rep_eq H _ _ hx with ⟨k, e₁, e₂, hk : _ = H.map e₂ 0⟩
[GOAL]
case refine_2.intro.intro.intro.intro.intro
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
k : J
e₁ e₂ : j ⟶ k
hk : ↑(H.map e₁) (↑(NatTrans.app γ j) y) = ↑(H.map e₂) 0
⊢ ↑(colimit.ι G j) y ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
rw [map_zero, ← comp_apply, ← NatTrans.naturality, comp_apply] at hk
[GOAL]
case refine_2.intro.intro.intro.intro.intro
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
k : J
e₁ e₂ : j ⟶ k
hk : ↑(NatTrans.app γ k) (↑(G.map e₁) y) = 0
⊢ ↑(colimit.ι G j) y ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
rcases((exact_iff _ _).mp <| h k).ge hk with ⟨t, ht⟩
[GOAL]
case refine_2.intro.intro.intro.intro.intro.intro
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
k : J
e₁ e₂ : j ⟶ k
hk : ↑(NatTrans.app γ k) (↑(G.map e₁) y) = 0
t : ↑(F.obj k)
ht : ↑(NatTrans.app η k) t = ↑(G.map e₁) y
⊢ ↑(colimit.ι G j) y ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
use colimit.ι F k t
[GOAL]
case h
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
k : J
e₁ e₂ : j ⟶ k
hk : ↑(NatTrans.app γ k) (↑(G.map e₁) y) = 0
t : ↑(F.obj k)
ht : ↑(NatTrans.app η k) t = ↑(G.map e₁) y
⊢ ↑(colim.map η) (↑(colimit.ι F k) t) = ↑(colimit.ι G j) y
[PROOFSTEP]
erw [← comp_apply, colimit.ι_map, comp_apply, ht]
[GOAL]
case h
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
k : J
e₁ e₂ : j ⟶ k
hk : ↑(NatTrans.app γ k) (↑(G.map e₁) y) = 0
t : ↑(F.obj k)
ht : ↑(NatTrans.app η k) t = ↑(G.map e₁) y
⊢ ↑(colimit.ι G k) (↑(G.map e₁) y) = ↑(colimit.ι G j) y
[PROOFSTEP]
exact colimit.w_apply G e₁ y


[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ factorThruImage f ≫ ι f = f
[PROOFSTEP]
ext
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
x✝ : ↑G
⊢ ↑(factorThruImage f ≫ ι f) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f))) 0 = 0
[PROOFSTEP]
haveI := F'.m_mono
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f))) 0 = 0
[PROOFSTEP]
apply injective_of_mono F'.m
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f))) 0) =
    ↑F'.m 0
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = _
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑0) (_ : ↑0 ∈ AddMonoidHom.range f)) = ↑F'.m 0
[PROOFSTEP]
rw [F'.fac, AddMonoidHom.map_zero]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ ↑f ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑0) (_ : ↑0 ∈ AddMonoidHom.range f)) = 0
[PROOFSTEP]
exact (Classical.indefiniteDescription (fun y => f y = 0) _).2
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ ∀ (x y : ↑(image f)),
    ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        (x + y) =
      ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          x +
        ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          y
[PROOFSTEP]
intro x y
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
        map_zero' :=
          (_ :
            (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                0 =
              0) }
      (x + y) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        x +
      ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        y
[PROOFSTEP]
haveI := F'.m_mono
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
        map_zero' :=
          (_ :
            (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                0 =
              0) }
      (x + y) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        x +
      ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        y
[PROOFSTEP]
apply injective_of_mono F'.m
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑F'.m
      (ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        (x + y)) =
    ↑F'.m
      (ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          x +
        ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          y)
[PROOFSTEP]
rw [AddMonoidHom.map_add]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑F'.m
      (ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        (x + y)) =
    ↑F'.m
        (ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          x) +
      ↑F'.m
        (ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          y)
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑(F'.e ≫ F'.m)
      ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑(x + y)) (_ : ↑(x + y) ∈ AddMonoidHom.range f)) =
    ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)) +
      ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑y) (_ : ↑y ∈ AddMonoidHom.range f))
[PROOFSTEP]
rw [F'.fac]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑f ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑(x + y)) (_ : ↑(x + y) ∈ AddMonoidHom.range f)) =
    ↑f ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)) +
      ↑f ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑y) (_ : ↑y ∈ AddMonoidHom.range f))
[PROOFSTEP]
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑(x + y) =
    ↑f ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)) +
      ↑f ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑y) (_ : ↑y ∈ AddMonoidHom.range f))
[PROOFSTEP]
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑(x + y) = ↑x + ↑f ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑y) (_ : ↑y ∈ AddMonoidHom.range f))
[PROOFSTEP]
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
rfl
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f
[PROOFSTEP]
ext x
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑(lift F' ≫ F'.m) x = ↑(ι f) x
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = _
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)) = ↑(ι f) x
[PROOFSTEP]
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = ↑(ι f) x
[PROOFSTEP]
rfl


[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b : R
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : ((fun m => a • m) ∘ fun x => s • x) c = ((fun m => a • m) ∘ fun x => s • x) d
⊢ c = d
[PROOFSTEP]
dsimp only [Function.comp] at cd
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b : R
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : a • s • c = a • s • d
⊢ c = d
[PROOFSTEP]
rw [← smul_assoc, ← smul_assoc] at cd
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b : R
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd✝¹ : a • s • c = a • s • d
cd✝ : (a • s) • c = a • s • d
cd : (a • s) • c = (a • s) • d
⊢ c = d
[PROOFSTEP]
exact ab cd
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M b
[PROOFSTEP]
rw [← smul_eq_mul] at ab
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a • b)
⊢ IsSMulRegular M b
[PROOFSTEP]
exact ab.of_smul _
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b
[PROOFSTEP]
rintro ⟨ab, ba⟩
[GOAL]
case refine'_1.intro
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
ba : IsSMulRegular M (b * a)
⊢ IsSMulRegular M a ∧ IsSMulRegular M b
[PROOFSTEP]
refine' ⟨ba.of_mul, ab.of_mul⟩
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case refine'_2.intro
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ha : IsSMulRegular M a
hb : IsSMulRegular M b
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
[PROOFSTEP]
exact ⟨ha.mul hb, hb.mul ha⟩
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : (fun x => 1 • x) a = (fun x => 1 • x) b
⊢ a = b
[PROOFSTEP]
dsimp only [Function.comp] at ab
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : 1 • a = 1 • b
⊢ a = b
[PROOFSTEP]
rw [one_smul, one_smul] at ab
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : a = b
⊢ a = b
[PROOFSTEP]
assumption
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M (?m.10326 h * b)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M 1
[PROOFSTEP]
exact one M
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ n)
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ Nat.zero)
[PROOFSTEP]
rw [pow_zero]
[GOAL]
case zero
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M 1
[PROOFSTEP]
simp only [one]
[GOAL]
case succ
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a ^ Nat.succ n)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a * a ^ n)
[PROOFSTEP]
exact (ra.smul_iff (a ^ n)).mpr hn
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a
[PROOFSTEP]
refine' ⟨_, pow n⟩
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) → IsSMulRegular M a
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ', ← smul_eq_mul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ Nat.pred n • a) → IsSMulRegular M a
[PROOFSTEP]
exact of_smul _
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M (a • s)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M 1
[PROOFSTEP]
exact one M
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
h : IsSMulRegular M 0
a b : M
⊢ (fun x => 0 • x) a = (fun x => 0 • x) b
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b
[PROOFSTEP]
repeat' rw [MulActionWithZero.zero_smul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b
[PROOFSTEP]
rw [MulActionWithZero.zero_smul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
h : IsSMulRegular M 0
a b : M
⊢ 0 = 0 • b
[PROOFSTEP]
rw [MulActionWithZero.zero_smul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ ¬IsSMulRegular M 0 ↔ Nontrivial M
[PROOFSTEP]
rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y
[PROOFSTEP]
push_neg
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
[PROOFSTEP]
rw [← mul_and_mul_iff]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
[PROOFSTEP]
exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M (b * a)
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
⊢ IsSMulRegular R g
[PROOFSTEP]
intro x y h
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x => g • x) x = (fun x => g • x) y
⊢ x = y
[PROOFSTEP]
convert congr_arg (g⁻¹ • ·) h using 1
[GOAL]
case h.e'_2
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x => g • x) x = (fun x => g • x) y
⊢ x = g⁻¹ • (fun x => g • x) x
[PROOFSTEP]
simp [← smul_assoc]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x => g • x) x = (fun x => g • x) y
⊢ y = g⁻¹ • (fun x => g • x) y
[PROOFSTEP]
simp [← smul_assoc]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ua : IsUnit a
⊢ IsSMulRegular M a
[PROOFSTEP]
rcases ua with ⟨a, rfl⟩
[GOAL]
case intro
R : Type u_1
S : Type u_2
M : Type u_3
b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a : Rˣ
⊢ IsSMulRegular M ↑a
[PROOFSTEP]
exact a.isSMulRegular M


[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget GroupCat) x y
⊢ colimitInvAux F x = colimitInvAux F y
[PROOFSTEP]
apply G.mk_eq
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget GroupCat) x y
⊢ ∃ k f g, ↑(F.map f) { fst := x.fst, snd := x.snd⁻¹ }.snd = ↑(F.map g) { fst := y.fst, snd := y.snd⁻¹ }.snd
[PROOFSTEP]
obtain ⟨k, f, g, hfg⟩ := h
[GOAL]
case h.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget GroupCat).map f x.snd = (F ⋙ forget GroupCat).map g y.snd
⊢ ∃ k f g, ↑(F.map f) { fst := x.fst, snd := x.snd⁻¹ }.snd = ↑(F.map g) { fst := y.fst, snd := y.snd⁻¹ }.snd
[PROOFSTEP]
use k, f, g
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget GroupCat).map f x.snd = (F ⋙ forget GroupCat).map g y.snd
⊢ ↑(F.map f) { fst := x.fst, snd := x.snd⁻¹ }.snd = ↑(F.map g) { fst := y.fst, snd := y.snd⁻¹ }.snd
[PROOFSTEP]
rw [MonoidHom.map_inv, MonoidHom.map_inv, inv_inj]
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget GroupCat).map f x.snd = (F ⋙ forget GroupCat).map g y.snd
⊢ ↑(F.map f) x.snd = ↑(F.map g) y.snd
[PROOFSTEP]
exact hfg
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x : ↑(G F)
⊢ ↑(G F)
[PROOFSTEP]
refine' Quot.lift (colimitInvAux.{v, u} F) _ x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x : ↑(G F)
⊢ ∀ (a b : (j : J) × ↑(F.obj j)),
    Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat) a b → colimitInvAux F a = colimitInvAux F b
[PROOFSTEP]
intro x y h
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x✝ : ↑(G F)
x y : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat) x y
⊢ colimitInvAux F x = colimitInvAux F y
[PROOFSTEP]
apply colimitInvAux_eq_of_rel
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x✝ : ↑(G F)
x y : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat) x y
⊢ Types.FilteredColimit.Rel (F ⋙ forget GroupCat) x y
[PROOFSTEP]
apply Types.FilteredColimit.rel_of_quot_rel
[GOAL]
case h.a
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x✝ : ↑(G F)
x y : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat) x y
⊢ Types.Quot.Rel (F ⋙ forget GroupCat) x y
[PROOFSTEP]
exact h
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
x : ↑(G F)
⊢ x⁻¹ * x = 1
[PROOFSTEP]
refine Quot.inductionOn x ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
x : ↑(G F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) a)⁻¹ *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) a =
      1
[PROOFSTEP]
clear x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) a)⁻¹ *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) a =
      1
[PROOFSTEP]
intro x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
x : (j : J) × ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) x)⁻¹ *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) x =
    1
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
j : J
x : ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) { fst := j, snd := x })⁻¹ *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) { fst := j, snd := x } =
    1
[PROOFSTEP]
erw [colimit_inv_mk_eq, colimit_mul_mk_eq (F ⋙ forget₂ GroupCat MonCat.{max v u}) ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j),
  colimit_one_eq (F ⋙ forget₂ GroupCat MonCat.{max v u}) j]
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
j : J
x : ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ GroupCat MonCat)
      { fst := j,
        snd :=
          ↑((F ⋙ forget₂ GroupCat MonCat).map (𝟙 j)) { fst := j, snd := { fst := j, snd := x }.snd⁻¹ }.snd *
            ↑((F ⋙ forget₂ GroupCat MonCat).map (𝟙 j)) { fst := j, snd := x }.snd } =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ GroupCat MonCat) { fst := j, snd := 1 }
[PROOFSTEP]
dsimp
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
j : J
x : ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ GroupCat MonCat)
      { fst := j,
        snd := ↑((forget₂ GroupCat MonCat).map (F.map (𝟙 j))) x⁻¹ * ↑((forget₂ GroupCat MonCat).map (F.map (𝟙 j))) x } =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ GroupCat MonCat) { fst := j, snd := 1 }
[PROOFSTEP]
erw [CategoryTheory.Functor.map_id, mul_left_inv]