[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x
[PROOFSTEP]
rw [← cast_eq_zero_iff R p x, ← map_natCast (Ideal.Quotient.mk I)]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑(Ideal.Quotient.mk I) ↑x = 0 ↔ ↑x = 0
[PROOFSTEP]
refine' Ideal.Quotient.eq.trans (_ : ↑x - 0 ∈ I ↔ _)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x - 0 ∈ I ↔ ↑x = 0
[PROOFSTEP]
rw [sub_zero]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x ∈ I ↔ ↑x = 0
[PROOFSTEP]
exact ⟨h x, fun h' => h'.symm ▸ I.zero_mem⟩
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ↑(AddSubgroup.index (Submodule.toAddSubgroup I)) = 0
[PROOFSTEP]
rw [AddSubgroup.index, Nat.card_eq]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ↑(if h : Finite (R ⧸ Submodule.toAddSubgroup I) then Fintype.card (R ⧸ Submodule.toAddSubgroup I) else 0) = 0
[PROOFSTEP]
split_ifs with hq
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
case neg R : Type u_1 inst✝ : CommRing R I : Ideal R hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I) ⊢ ↑0 = 0
[PROOFSTEP]
swap
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
[PROOFSTEP]
by_contra h
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
h : ¬↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
⊢ False
[PROOFSTEP]
letI : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
h : ¬↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)
⊢ False
[PROOFSTEP]
have h : (Fintype.card (R ⧸ I) : R ⧸ I) ≠ 0 := h
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
h✝ : ¬↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)
h : ↑(Fintype.card (R ⧸ I)) ≠ 0
⊢ False
[PROOFSTEP]
simp at h


[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e f g : A₁ ≃ₐ[R] A₂
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨f, _⟩, _⟩ := f
[GOAL]
case mk.mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e g : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ f
right_inv✝ : Function.RightInverse invFun✝ f
map_mul'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
commutes'✝ :
  ∀ (r : R),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
h₁ :
  (fun f => f.toFun)
      { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ } =
    (fun f => f.toFun) g
h₂ :
  (fun f => f.invFun)
      { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ } =
    (fun f => f.invFun) g
⊢ { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }, map_mul' := map_mul'✝,
      map_add' := map_add'✝, commutes' := commutes'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨g, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝¹ : A₂ → A₁
left_inv✝¹ : Function.LeftInverse invFun✝¹ f
right_inv✝¹ : Function.RightInverse invFun✝¹ f
map_mul'✝¹ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x * y) =
      Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x *
        Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_add'✝¹ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x + y) =
      Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x +
        Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
commutes'✝¹ :
  ∀ (r : R),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
g : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ g
right_inv✝ : Function.RightInverse invFun✝ g
map_mul'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
commutes'✝ :
  ∀ (r : R),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
h₁ :
  (fun f => f.toFun)
      { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    (fun f => f.toFun)
      { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
h₂ :
  (fun f => f.invFun)
      { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    (fun f => f.invFun)
      { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
⊢ { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
      map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
      map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e f g : A₁ ≃ₐ[R] A₂
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨f, _⟩, _⟩ := f
[GOAL]
case mk.mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e g : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ f
right_inv✝ : Function.RightInverse invFun✝ f
map_mul'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
commutes'✝ :
  ∀ (r : R),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
h₁ :
  (fun f => f.toFun)
      { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ } =
    (fun f => f.toFun) g
h₂ :
  (fun f => f.invFun)
      { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ } =
    (fun f => f.invFun) g
⊢ { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }, map_mul' := map_mul'✝,
      map_add' := map_add'✝, commutes' := commutes'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨g, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝¹ : A₂ → A₁
left_inv✝¹ : Function.LeftInverse invFun✝¹ f
right_inv✝¹ : Function.RightInverse invFun✝¹ f
map_mul'✝¹ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x * y) =
      Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x *
        Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_add'✝¹ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x + y) =
      Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x +
        Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
commutes'✝¹ :
  ∀ (r : R),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
g : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ g
right_inv✝ : Function.RightInverse invFun✝ g
map_mul'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
commutes'✝ :
  ∀ (r : R),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
h₁ :
  (fun f => f.toFun)
      { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    (fun f => f.toFun)
      { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
h₂ :
  (fun f => f.invFun)
      { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    (fun f => f.invFun)
      { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
⊢ { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
      map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
      map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
[PROOFSTEP]
congr
  -- Porting note: the default simps projection was `e.toEquiv.toFun`, it should be `FunLike.coe`
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
r : R
x : A₁
⊢ ↑e (r • x) = r • ↑e x
[PROOFSTEP]
simp only [Algebra.smul_def, map_mul, commutes]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
src✝ : A₂ ≃+* A₁ := RingEquiv.symm (toRingEquiv e)
r : R
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R A₂) r) = ↑(algebraMap R A₁) r
[PROOFSTEP]
rw [← e.toRingEquiv.symm_apply_apply (algebraMap R A₁ r)]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
src✝ : A₂ ≃+* A₁ := RingEquiv.symm (toRingEquiv e)
r : R
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R A₂) r) =
    ↑(RingEquiv.symm (toRingEquiv e)) (↑(toRingEquiv e) (↑(algebraMap R A₁) r))
[PROOFSTEP]
congr
[GOAL]
case e_a
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
src✝ : A₂ ≃+* A₁ := RingEquiv.symm (toRingEquiv e)
r : R
⊢ ↑(algebraMap R A₂) r = ↑(toRingEquiv e) (↑(algebraMap R A₁) r)
[PROOFSTEP]
change _ = e _
[GOAL]
case e_a
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
src✝ : A₂ ≃+* A₁ := RingEquiv.symm (toRingEquiv e)
r : R
⊢ ↑(algebraMap R A₂) r = ↑e (↑(algebraMap R A₁) r)
[PROOFSTEP]
rw [e.commutes]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
⊢ symm (symm e) = e
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
a✝ : A₁
⊢ ↑(symm (symm e)) a✝ = ↑e a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
src✝ : A₁ ≃+* A₃ := RingEquiv.trans (toRingEquiv e₁) (toRingEquiv e₂)
r : R
⊢ Equiv.toFun e₂.toEquiv (Equiv.toFun e₁.toEquiv (↑(algebraMap R A₁) r)) = ↑(algebraMap R A₃) r
[PROOFSTEP]
rw [e₁.commutes', e₂.commutes']
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
⊢ AlgHom.comp ↑e ↑(symm e) = AlgHom.id R A₂
[PROOFSTEP]
ext
[GOAL]
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
x✝ : A₂
⊢ ↑(AlgHom.comp ↑e ↑(symm e)) x✝ = ↑(AlgHom.id R A₂) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
⊢ AlgHom.comp ↑(symm e) ↑e = AlgHom.id R A₁
[PROOFSTEP]
ext
[GOAL]
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
x✝ : A₁
⊢ ↑(AlgHom.comp ↑(symm e) ↑e) x✝ = ↑(AlgHom.id R A₁) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁ →ₐ[R] A₂
⊢ (fun f => AlgHom.comp (AlgHom.comp (↑(symm e₂)) f) ↑e₁) ((fun f => AlgHom.comp (AlgHom.comp (↑e₂) f) ↑(symm e₁)) f) =
    f
[PROOFSTEP]
simp only [AlgHom.comp_assoc, toAlgHom_eq_coe, symm_comp]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁ →ₐ[R] A₂
⊢ AlgHom.comp (↑(symm e₂)) (AlgHom.comp (↑e₂) (AlgHom.comp f (AlgHom.id R A₁))) = f
[PROOFSTEP]
simp only [← AlgHom.comp_assoc, symm_comp, AlgHom.id_comp, AlgHom.comp_id]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁' →ₐ[R] A₂'
⊢ (fun f => AlgHom.comp (AlgHom.comp (↑e₂) f) ↑(symm e₁)) ((fun f => AlgHom.comp (AlgHom.comp (↑(symm e₂)) f) ↑e₁) f) =
    f
[PROOFSTEP]
simp only [AlgHom.comp_assoc, toAlgHom_eq_coe, comp_symm]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁' →ₐ[R] A₂'
⊢ AlgHom.comp (↑e₂) (AlgHom.comp (↑(symm e₂)) (AlgHom.comp f (AlgHom.id R A₁'))) = f
[PROOFSTEP]
simp only [← AlgHom.comp_assoc, comp_symm, AlgHom.id_comp, AlgHom.comp_id]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
⊢ ↑(arrowCongr e₁ e₃) (AlgHom.comp g f) = AlgHom.comp (↑(arrowCongr e₂ e₃) g) (↑(arrowCongr e₁ e₂) f)
[PROOFSTEP]
ext
[GOAL]
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑(↑(arrowCongr e₁ e₃) (AlgHom.comp g f)) x✝ = ↑(AlgHom.comp (↑(arrowCongr e₂ e₃) g) (↑(arrowCongr e₁ e₂) f)) x✝
[PROOFSTEP]
simp only [arrowCongr, Equiv.coe_fn_mk, AlgHom.comp_apply]
[GOAL]
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑↑e₃ (↑g (↑f (↑↑(symm e₁) x✝))) = ↑↑e₃ (↑g (↑↑(symm e₂) (↑↑e₂ (↑f (↑↑(symm e₁) x✝)))))
[PROOFSTEP]
congr
[GOAL]
case H.h.e_6.h.h.e_6.h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑f (↑↑(symm e₁) x✝) = ↑↑(symm e₂) (↑↑e₂ (↑f (↑↑(symm e₁) x✝)))
[PROOFSTEP]
exact (e₂.symm_apply_apply _).symm
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
⊢ arrowCongr refl refl = Equiv.refl (A₁ →ₐ[R] A₂)
[PROOFSTEP]
ext
[GOAL]
case H.H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x✝¹ : A₁ →ₐ[R] A₂
x✝ : A₁
⊢ ↑(↑(arrowCongr refl refl) x✝¹) x✝ = ↑(↑(Equiv.refl (A₁ →ₐ[R] A₂)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e e₁ : A₁ ≃ₐ[R] A₂
e₁' : A₁' ≃ₐ[R] A₂'
e₂ : A₂ ≃ₐ[R] A₃
e₂' : A₂' ≃ₐ[R] A₃'
⊢ arrowCongr (trans e₁ e₂) (trans e₁' e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂')
[PROOFSTEP]
ext
[GOAL]
case H.H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e e₁ : A₁ ≃ₐ[R] A₂
e₁' : A₁' ≃ₐ[R] A₂'
e₂ : A₂ ≃ₐ[R] A₃
e₂' : A₂' ≃ₐ[R] A₃'
x✝¹ : A₁ →ₐ[R] A₁'
x✝ : A₃
⊢ ↑(↑(arrowCongr (trans e₁ e₂) (trans e₁' e₂')) x✝¹) x✝ = ↑(↑((arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂')) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
⊢ (arrowCongr e₁ e₂).symm = arrowCongr (symm e₁) (symm e₂)
[PROOFSTEP]
ext
[GOAL]
case H.H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
x✝¹ : A₁' →ₐ[R] A₂'
x✝ : A₁
⊢ ↑(↑(arrowCongr e₁ e₂).symm x✝¹) x✝ = ↑(↑(arrowCongr (symm e₁) (symm e₂)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
⊢ (fun ψ => trans e (trans ψ (symm e'))) ((fun ψ => trans (symm e) (trans ψ e')) ψ) = ψ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
a✝ : A₁
⊢ ↑((fun ψ => trans e (trans ψ (symm e'))) ((fun ψ => trans (symm e) (trans ψ e')) ψ)) a✝ = ↑ψ a✝
[PROOFSTEP]
simp_rw [trans_apply, symm_apply_apply]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
⊢ (fun ψ => trans (symm e) (trans ψ e')) ((fun ψ => trans e (trans ψ (symm e'))) ψ) = ψ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
a✝ : A₂
⊢ ↑((fun ψ => trans (symm e) (trans ψ e')) ((fun ψ => trans e (trans ψ (symm e'))) ψ)) a✝ = ↑ψ a✝
[PROOFSTEP]
simp_rw [trans_apply, apply_symm_apply]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
⊢ equivCongr refl refl = Equiv.refl (A₁ ≃ₐ[R] A₁')
[PROOFSTEP]
ext
[GOAL]
case H.h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x✝ : A₁ ≃ₐ[R] A₁'
a✝ : A₁
⊢ ↑(↑(equivCongr refl refl) x✝) a✝ = ↑(↑(Equiv.refl (A₁ ≃ₐ[R] A₁')) x✝) a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul✝ : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes✝ : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
map_mul : ∀ (x y : A₁), ↑(toLinearEquiv e) (x * y) = ↑(toLinearEquiv e) x * ↑(toLinearEquiv e) y
commutes : ∀ (r : R), ↑(toLinearEquiv e) (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
⊢ ofLinearEquiv (toLinearEquiv e) map_mul commutes = e
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul✝ : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes✝ : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
map_mul : ∀ (x y : A₁), ↑(toLinearEquiv e) (x * y) = ↑(toLinearEquiv e) x * ↑(toLinearEquiv e) y
commutes : ∀ (r : R), ↑(toLinearEquiv e) (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
a✝ : A₁
⊢ ↑(ofLinearEquiv (toLinearEquiv e) map_mul commutes) a✝ = ↑e a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
⊢ toLinearEquiv (ofLinearEquiv l map_mul commutes) = l
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
x✝ : A₁
⊢ ↑(toLinearEquiv (ofLinearEquiv l map_mul commutes)) x✝ = ↑l x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e ϕ : A₁ ≃ₐ[R] A₂
src✝ : (A₁ ≃ₐ[R] A₁) ≃ A₂ ≃ₐ[R] A₂ := equivCongr ϕ ϕ
ψ χ : A₁ ≃ₐ[R] A₁
⊢ Equiv.toFun
      { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
        left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (ψ * χ) =
    Equiv.toFun
        { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
          left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        ψ *
      Equiv.toFun
        { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
          left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        χ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e ϕ : A₁ ≃ₐ[R] A₂
src✝ : (A₁ ≃ₐ[R] A₁) ≃ A₂ ≃ₐ[R] A₂ := equivCongr ϕ ϕ
ψ χ : A₁ ≃ₐ[R] A₁
a✝ : A₂
⊢ ↑(Equiv.toFun
          { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
            left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          (ψ * χ))
      a✝ =
    ↑(Equiv.toFun
            { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
              left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            ψ *
          Equiv.toFun
            { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
              left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            χ)
      a✝
[PROOFSTEP]
simp only [mul_apply, trans_apply, symm_apply_apply]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
⊢ autCongr refl = MulEquiv.refl (A₁ ≃ₐ[R] A₁)
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x✝ : A₁ ≃ₐ[R] A₁
a✝ : A₁
⊢ ↑(↑(autCongr refl) x✝) a✝ = ↑(↑(MulEquiv.refl (A₁ ≃ₐ[R] A₁)) x✝) a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
y : R
x : A₁
h : ↑(algebraMap R A₂) y = ↑e x
⊢ ↑(algebraMap R A₁) y = x
[PROOFSTEP]
simpa using e.symm.toAlgHom.algebraMap_eq_apply h


[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R
[PROOFSTEP]
have hch := CharP.cast_eq_zero R (ringChar R)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R
[PROOFSTEP]
have hp : p.Prime := Fact.out
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ IsUnit ↑p → ¬p ∣ ringChar R
[PROOFSTEP]
rintro h₁ ⟨q, hq⟩
[GOAL]
case mp.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
⊢ False
[PROOFSTEP]
rcases IsUnit.exists_left_inv h₁ with ⟨a, ha⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
⊢ False
[PROOFSTEP]
have h₃ : ¬ringChar R ∣ q := by
  rintro ⟨r, hr⟩
  rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
  nth_rw 1 [← mul_one (ringChar R)] at hq
  exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
⊢ ¬ringChar R ∣ q
[PROOFSTEP]
rintro ⟨r, hr⟩
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
r : ℕ
hr : q = ringChar R * r
⊢ False
[PROOFSTEP]
rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False
[PROOFSTEP]
nth_rw 1 [← mul_one (ringChar R)] at hq
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R * 1 = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False
[PROOFSTEP]
exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
⊢ False
[PROOFSTEP]
have h₄ := mt (CharP.int_cast_eq_zero_iff R (ringChar R) q).mp
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
⊢ False
[PROOFSTEP]
apply_fun ((↑) : ℕ → R) at hq
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
hq : ↑(ringChar R) = ↑(p * q)
⊢ False
[PROOFSTEP]
apply_fun (· * ·) a at hq
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
hq : a * ↑(ringChar R) = a * ↑(p * q)
⊢ False
[PROOFSTEP]
rw [Nat.cast_mul, hch, mul_zero, ← mul_assoc, ha, one_mul] at hq
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
hq : 0 = ↑q
⊢ False
[PROOFSTEP]
norm_cast at h₄
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
hq : 0 = ↑q
h₄ : ¬ringChar R ∣ q → ¬↑q = 0
⊢ False
[PROOFSTEP]
exact h₄ h₃ hq.symm
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ ¬p ∣ ringChar R → IsUnit ↑p
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
⊢ IsUnit ↑p
[PROOFSTEP]
rcases(hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : a * ↑p + b * ↑(ringChar R) = 1
⊢ IsUnit ↑p
[PROOFSTEP]
apply_fun ((↑) : ℤ → R) at hab
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑(a * ↑p + b * ↑(ringChar R)) = ↑1
⊢ IsUnit ↑p
[PROOFSTEP]
push_cast at hab
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑a * ↑p + ↑b * ↑(ringChar R) = 1
⊢ IsUnit ↑p
[PROOFSTEP]
rw [hch, mul_zero, add_zero, mul_comm] at hab
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑p * ↑a = 1
⊢ IsUnit ↑p
[PROOFSTEP]
exact isUnit_of_mul_eq_one (p : R) a hab
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ p ∣ ringChar R ↔ p ∣ Fintype.card R
[PROOFSTEP]
refine'
  ⟨fun h =>
    h.trans <|
      Int.coe_nat_dvd.mp <|
        (CharP.int_cast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <| by exact_mod_cast CharP.cast_card_eq_zero R,
    fun h => _⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ ringChar R
⊢ ↑↑(Fintype.card R) = 0
[PROOFSTEP]
exact_mod_cast CharP.cast_card_eq_zero R
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
⊢ p ∣ ringChar R
[PROOFSTEP]
by_contra h₀
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
⊢ False
[PROOFSTEP]
rcases exists_prime_addOrderOf_dvd_card p h with ⟨r, hr⟩
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
⊢ False
[PROOFSTEP]
have hr₁ := addOrderOf_nsmul_eq_zero r
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : addOrderOf r • r = 0
⊢ False
[PROOFSTEP]
rw [hr, nsmul_eq_mul] at hr₁
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : ↑p * r = 0
⊢ False
[PROOFSTEP]
rcases IsUnit.exists_left_inv ((isUnit_iff_not_dvd_char R p).mpr h₀) with ⟨u, hu⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : ↑p * r = 0
u : R
hu : u * ↑p = 1
⊢ False
[PROOFSTEP]
apply_fun (· * ·) u at hr₁
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * ↑p = 1
hr₁ : u * (↑p * r) = u * 0
⊢ False
[PROOFSTEP]
rw [mul_zero, ← mul_assoc, hu, one_mul] at hr₁
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * ↑p = 1
hr₁ : r = 0
⊢ False
[PROOFSTEP]
exact mt AddMonoid.addOrderOf_eq_one_iff.mpr (ne_of_eq_of_ne hr (Nat.Prime.ne_one Fact.out)) hr₁


[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
src✝ : AddSubmonoid M := ⊥
⊢ ∀ (c : R) {x : M},
    x ∈
        {
              toAddSubsemigroup :=
                { carrier := {0},
                  add_mem' := (_ : ∀ {a b : M}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier) },
              zero_mem' := (_ : 0 ∈ src✝.carrier) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := {0},
                  add_mem' := (_ : ∀ {a b : M}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier) },
              zero_mem' := (_ : 0 ∈ src✝.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q p : Submodule R M
⊢ restrictScalars S p = ⊥ ↔ p = ⊥
[PROOFSTEP]
simp [SetLike.ext_iff]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q p : Submodule R M
x : M
⊢ x ∈ ⊥ → x ∈ p
[PROOFSTEP]
simp (config := { contextual := true }) [zero_mem]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
x y : { x // x ∈ ⊥ }
⊢ x = y
[PROOFSTEP]
rcases x with ⟨x, xm⟩
[GOAL]
case mk
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
y : { x // x ∈ ⊥ }
x : M
xm : x ∈ ⊥
⊢ { val := x, property := xm } = y
[PROOFSTEP]
rcases y with ⟨y, ym⟩
[GOAL]
case mk.mk
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ { val := x, property := xm } = { val := y, property := ym }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_val
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ x = y
[PROOFSTEP]
rw [(Submodule.eq_bot_iff _).mp rfl x xm]
[GOAL]
case mk.mk.e_val
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ 0 = y
[PROOFSTEP]
rw [(Submodule.eq_bot_iff _).mp rfl y ym]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q p : Submodule R M
⊢ p ≠ ⊥ ↔ ∃ x, x ∈ p ∧ x ≠ 0
[PROOFSTEP]
simp only [ne_eq, p.eq_bot_iff, not_forall, exists_prop]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p✝ q p : Submodule R M
inst✝ : Subsingleton { x // x ∈ p }
⊢ p = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p✝ q p : Submodule R M
inst✝ : Subsingleton { x // x ∈ p }
⊢ p ≤ ⊥
[PROOFSTEP]
intro v hv
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p✝ q p : Submodule R M
inst✝ : Subsingleton { x // x ∈ p }
v : M
hv : v ∈ p
⊢ v ∈ ⊥
[PROOFSTEP]
exact congr_arg Subtype.val (Subsingleton.elim (⟨v, hv⟩ : p) 0)
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q p : Submodule R M
⊢ restrictScalars S p = ⊤ ↔ p = ⊤
[PROOFSTEP]
simp [SetLike.ext_iff]
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ ∀ {a b : M},
    a ∈ ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s →
      b ∈ ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s → a + b ∈ ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp (config := { contextual := true }) [add_mem]
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ 0 ∈
    { carrier := ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s,
        add_mem' :=
          (_ :
            ∀ (a a_1 : M),
              a ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i →
                a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i → a + a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i) }.carrier
[PROOFSTEP]
simp [zero_mem]
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ ∀ (c : R) {x : M},
    x ∈
        {
              toAddSubsemigroup :=
                { carrier := ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s,
                  add_mem' :=
                    (_ :
                      ∀ (a a_1 : M),
                        a ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i →
                          a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i →
                            a + a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i) },
              zero_mem' := (_ : 0 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s,
                  add_mem' :=
                    (_ :
                      ∀ (a a_1 : M),
                        a ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i →
                          a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i →
                            a + a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i) },
              zero_mem' := (_ : 0 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simp (config := { contextual := true }) [smul_mem]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q✝ p q : Submodule R M
⊢ ∀ {a b : M}, a ∈ ↑p ∩ ↑q → b ∈ ↑p ∩ ↑q → a + b ∈ ↑p ∩ ↑q
[PROOFSTEP]
simp (config := { contextual := true }) [add_mem]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q✝ p q : Submodule R M
⊢ 0 ∈ { carrier := ↑p ∩ ↑q, add_mem' := (_ : ∀ (a a_1 : M), a ∈ ↑p ∩ ↑q → a_1 ∈ ↑p ∩ ↑q → a + a_1 ∈ ↑p ∩ ↑q) }.carrier
[PROOFSTEP]
simp [zero_mem]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q✝ p q : Submodule R M
⊢ ∀ (c : R) {x : M},
    x ∈
        {
              toAddSubsemigroup :=
                { carrier := ↑p ∩ ↑q,
                  add_mem' := (_ : ∀ (a a_1 : M), a ∈ ↑p ∩ ↑q → a_1 ∈ ↑p ∩ ↑q → a + a_1 ∈ ↑p ∩ ↑q) },
              zero_mem' := (_ : 0 ∈ ↑p ∩ ↑q) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := ↑p ∩ ↑q,
                  add_mem' := (_ : ∀ (a a_1 : M), a ∈ ↑p ∩ ↑q → a_1 ∈ ↑p ∩ ↑q → a + a_1 ∈ ↑p ∩ ↑q) },
              zero_mem' := (_ : 0 ∈ ↑p ∩ ↑q) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simp (config := { contextual := true }) [smul_mem]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
src✝¹ : OrderTop (Submodule R M) := inferInstance
src✝ : OrderBot (Submodule R M) := inferInstance
x✝² : Set (Submodule R M)
x✝¹ : Submodule R M
hs : x✝¹ ∈ x✝²
x✝ : Submodule R M
hq : x✝ ∈ fun x => ∀ (b : Submodule R M), b ∈ x✝² → b ≤ x
⊢ x✝¹ ≤ x✝
[PROOFSTEP]
exact hq _ hs
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
⊢ ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
[PROOFSTEP]
letI := Classical.decEq ι
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
[PROOFSTEP]
refine' s.induction_on _ fun i s _ ih ↦ _
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Finset.inf ∅ p) = ⋂ (i : ι) (_ : i ∈ ∅), ↑(p i)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
ih : ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
⊢ ↑(Finset.inf (insert i s) p) = ⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), ↑(p i_1)
[PROOFSTEP]
rw [Finset.inf_insert, inf_coe, ih]
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
ih : ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
⊢ ↑(p i) ∩ ⋂ (i : ι) (_ : i ∈ s), ↑(p i) = ⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), ↑(p i_1)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ↑(⨅ (i : ι), p i) = ⋂ (i : ι), ↑(p i)
[PROOFSTEP]
rw [iInf, sInf_coe]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ⋂ (p_1 : Submodule R M) (_ : p_1 ∈ Set.range fun i => p i), ↑p_1 = ⋂ (i : ι), ↑(p i)
[PROOFSTEP]
simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ x ∈ ⨅ (i : ι), p i ↔ ∀ (i : ι), x ∈ p i
[PROOFSTEP]
rw [← SetLike.mem_coe, iInf_coe, Set.mem_iInter]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ (∀ (i : ι), x ∈ ↑(p i)) ↔ ∀ (i : ι), x ∈ p i
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
x : M
⊢ x ∈ Finset.inf s p ↔ ∀ (i : ι), i ∈ s → x ∈ p i
[PROOFSTEP]
simp only [← SetLike.mem_coe, finset_inf_coe, Set.mem_iInter]
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q S T : Submodule R M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
have : S ≤ S ⊔ T := le_sup_left
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q S T : Submodule R M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
rw [LE.le] at this
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q S T : Submodule R M
this : Preorder.toLE.1 S (S ⊔ T)
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
exact this
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q S T : Submodule R M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
have : T ≤ S ⊔ T := le_sup_right
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q S T : Submodule R M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
rw [LE.le] at this
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q S T : Submodule R M
this : Preorder.toLE.1 T (S ⊔ T)
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
exact this
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : Semiring S✝
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S✝ M
inst✝⁴ : SMul S✝ R
inst✝³ : IsScalarTower S✝ R M
p q : Submodule R M
R' : Type u_4
M' : Type u_5
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s - t ∈ S ⊔ T
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : Semiring S✝
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S✝ M
inst✝⁴ : SMul S✝ R
inst✝³ : IsScalarTower S✝ R M
p q : Submodule R M
R' : Type u_4
M' : Type u_5
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s + -t ∈ S ⊔ T
[PROOFSTEP]
exact add_mem_sup hs (neg_mem ht)
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
have := le_sSup hs
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
rw [LE.le] at this
[GOAL]
R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : Preorder.toLE.1 s (sSup S)
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
exact this
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q p p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ∧ x ∈ p' → x ∈ {0}) ↔ ∀ (x : M), x ∈ p → x ∈ p' → x = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
hpq : Disjoint p q
a : { x // x ∈ p }
ha : ↑a ∈ q
⊢ a = 0
[PROOFSTEP]
exact_mod_cast disjoint_def.mp hpq a (coe_mem a) ha


[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
a : A
ha : a ∈ ↑s
⊢ ↑↑(AlgHom.comp (Subalgebra.val (Algebra.adjoin R ↑s)) (unitization s)) ↑{ val := a, property := ha } = a
[PROOFSTEP]
simp
[GOAL]
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
⊢ Function.Injective ↑(unitization s)
[PROOFSTEP]
refine' (injective_iff_map_eq_zero _).mpr fun x hx => _
[GOAL]
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx : ↑(unitization s) x = 0
⊢ x = 0
[PROOFSTEP]
induction' x using Unitization.ind with r a
[GOAL]
case h
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r + ↑a) = 0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
rw [map_add] at hx
[GOAL]
case h
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
have hx' := congr_arg (Subtype.val : _ → A) hx
[GOAL]
case h
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a) = ↑0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
simp only [NonUnitalSubalgebra.unitization_apply_coe, Unitization.fst_inl, Subalgebra.coe_algebraMap,
  Unitization.snd_inl, ZeroMemClass.coe_zero, add_zero, map_neg, AddSubgroupClass.coe_neg, Unitization.fst_inr,
  map_zero, Unitization.snd_inr, Subalgebra.coe_add, zero_add] at hx'
[GOAL]
case h
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(algebraMap R A) r + ↑a = 0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
by_cases hr : r = 0
[GOAL]
case pos
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(algebraMap R A) r + ↑a = 0
hr : r = 0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
simp only [hr, map_zero, Unitization.inl_zero, zero_add] at hx' ⊢
[GOAL]
case pos
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hr : r = 0
hx' : ↑a = 0
⊢ ↑a = 0
[PROOFSTEP]
rw [← ZeroMemClass.coe_zero s] at hx'
[GOAL]
case pos
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hr : r = 0
hx' : ↑a = ↑0
⊢ ↑a = 0
[PROOFSTEP]
exact congr_arg _ (Subtype.coe_injective hx')
[GOAL]
case neg
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(algebraMap R A) r + ↑a = 0
hr : ¬r = 0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
refine' False.elim (h1 _)
[GOAL]
case neg
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(algebraMap R A) r + ↑a = 0
hr : ¬r = 0
⊢ 1 ∈ s
[PROOFSTEP]
rw [← eq_sub_iff_add_eq, zero_sub] at hx'
[GOAL]
case neg
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(algebraMap R A) r = -↑a
hr : ¬r = 0
⊢ 1 ∈ s
[PROOFSTEP]
replace hx' := congr_arg (fun y => r⁻¹ • y) hx'
[GOAL]
case neg
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hr : ¬r = 0
hx' : (fun y => r⁻¹ • y) (↑(algebraMap R A) r) = (fun y => r⁻¹ • y) (-↑a)
⊢ 1 ∈ s
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, ← smul_assoc, smul_eq_mul, inv_mul_cancel hr, one_smul] at hx'
[GOAL]
case neg
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hr : ¬r = 0
hx' : 1 = r⁻¹ • -↑a
⊢ 1 ∈ s
[PROOFSTEP]
exact hx'.symm ▸ SMulMemClass.smul_mem r⁻¹ (neg_mem a.prop)
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
S : Subsemiring R
⊢ NonUnitalSubsemiring.toSubsemiring (toNonUnitalSubsemiring S) (_ : 1 ∈ S) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
inst✝ : NonAssocSemiring R
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
⊢ NonUnitalSubsemiring.toSubsemiring
      (toNonUnitalSubsemiring { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ })
      (_ : 1 ∈ { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }) =
    { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
S : NonUnitalSubsemiring R
h1 : 1 ∈ S
⊢ Subsemiring.toNonUnitalSubsemiring (toSubsemiring S h1) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
inst✝ : NonAssocSemiring R
toAddSubmonoid✝ : AddSubmonoid R
mul_mem'✝ : ∀ {a b : R}, a ∈ toAddSubmonoid✝.carrier → b ∈ toAddSubmonoid✝.carrier → a * b ∈ toAddSubmonoid✝.carrier
h1 : 1 ∈ { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ }
⊢ Subsemiring.toNonUnitalSubsemiring (toSubsemiring { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ } h1) =
    { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R✝ : Type u_1
inst✝¹ : NonAssocSemiring R✝
R : Type u_2
inst✝ : Semiring R
S : NonUnitalSubsemiring R
⊢ Function.Surjective ↑(unitization S)
[PROOFSTEP]
simpa [unitization, AlgEquiv.arrowCongr] using
  NonUnitalSubalgebra.unitization_surjective (hSRA := AddSubmonoidClass.nsmulMemClass) S
[GOAL]
R : Type u_1
inst✝ : Ring R
S : Subring R
⊢ NonUnitalSubring.toSubring (toNonUnitalSubring S) (_ : 1 ∈ S) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
inst✝ : Ring R
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
⊢ NonUnitalSubring.toSubring (toNonUnitalSubring { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ })
      (_ : 1 ∈ { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }) =
    { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : Ring R
S : NonUnitalSubring R
h1 : 1 ∈ S
⊢ Subring.toNonUnitalSubring (toSubring S h1) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
inst✝ : Ring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ Subring.toNonUnitalSubring
      (toSubring { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } h1) =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : Ring R
S : NonUnitalSubring R
⊢ Function.Surjective ↑(unitization S)
[PROOFSTEP]
simpa [unitization, AlgEquiv.arrowCongr] using
  NonUnitalSubalgebra.unitization_surjective (hSRA := AddSubgroupClass.zsmulMemClass) S
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ NonUnitalSubalgebra.toSubalgebra (toNonUnitalSubalgebra S) (_ : 1 ∈ S) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), ↑(algebraMap R A) r ∈ toSubsemiring✝.carrier
⊢ NonUnitalSubalgebra.toSubalgebra
      (toNonUnitalSubalgebra { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ })
      (_ : 1 ∈ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }) =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : NonUnitalSubalgebra R A
h1 : 1 ∈ S
⊢ Subalgebra.toNonUnitalSubalgebra (toSubalgebra S h1) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
⊢ Subalgebra.toNonUnitalSubalgebra
      (toSubalgebra { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ } h1) =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : StarSubalgebra R A
⊢ NonUnitalStarSubalgebra.toStarSubalgebra (toNonUnitalStarSubalgebra S) (_ : 1 ∈ S.carrier) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
toSubalgebra✝ : Subalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toSubalgebra✝.carrier → star a ∈ toSubalgebra✝.carrier
⊢ NonUnitalStarSubalgebra.toStarSubalgebra
      (toNonUnitalStarSubalgebra { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ })
      (_ :
        1 ∈
          { toSubalgebra := toSubalgebra✝,
                      star_mem' := star_mem'✝ }.toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) =
    { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h1 : 1 ∈ S
⊢ StarSubalgebra.toNonUnitalStarSubalgebra (toStarSubalgebra S h1) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h1 : 1 ∈ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
⊢ StarSubalgebra.toNonUnitalStarSubalgebra
      (toStarSubalgebra { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ } h1) =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
a : A
ha : a ∈ ↑S
⊢ ↑↑(StarAlgHom.comp (StarSubalgebra.subtype (StarSubalgebra.adjoin R ↑S)) (unitization S)).toAlgHom
      ↑{ val := a, property := ha } =
    a
[PROOFSTEP]
simp


[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
n : ℕ
x✝ : 0 < n + 1
⊢ 0 ^ (n + 1) = 0
[PROOFSTEP]
rw [pow_succ, zero_mul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
k : ℕ
x✝ : k + 1 ≠ 0
⊢ 0 ^ (k + 1) = 0
[PROOFSTEP]
rw [pow_succ]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
k : ℕ
x✝ : k + 1 ≠ 0
⊢ 0 * 0 ^ k = 0
[PROOFSTEP]
exact zero_mul _
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
n : ℕ
⊢ 0 ^ n = if n = 0 then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
n : ℕ
h : n = 0
⊢ 0 ^ n = 1
[PROOFSTEP]
rw [h, pow_zero]
[GOAL]
case neg
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
n : ℕ
h : ¬n = 0
⊢ 0 ^ n = 0
[PROOFSTEP]
rw [zero_pow (Nat.pos_of_ne_zero h)]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
x : M
n m : ℕ
hn : n ≤ m
hx : x ^ n = 0
⊢ x ^ m = 0
[PROOFSTEP]
rw [← tsub_add_cancel_of_le hn, pow_add, hx, mul_zero]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H : x ^ n = 0
⊢ x = 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H✝ : x ^ n = 0
H : x ^ Nat.zero = 0
⊢ x = 0
[PROOFSTEP]
rw [pow_zero] at H
[GOAL]
case zero
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H✝ : x ^ n = 0
H : 1 = 0
⊢ x = 0
[PROOFSTEP]
rw [← mul_one x, H, mul_zero]
[GOAL]
case succ
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n✝ : ℕ
H✝ : x ^ n✝ = 0
n : ℕ
ih : x ^ n = 0 → x = 0
H : x ^ Nat.succ n = 0
⊢ x = 0
[PROOFSTEP]
rw [pow_succ] at H
[GOAL]
case succ
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n✝ : ℕ
H✝ : x ^ n✝ = 0
n : ℕ
ih : x ^ n = 0 → x = 0
H : x * x ^ n = 0
⊢ x = 0
[PROOFSTEP]
exact Or.casesOn (mul_eq_zero.1 H) id ih
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ a ^ n = 0 ↔ a = 0
[PROOFSTEP]
refine' ⟨pow_eq_zero, _⟩
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ a = 0 → a ^ n = 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
n : ℕ
hn : 0 < n
⊢ 0 ^ n = 0
[PROOFSTEP]
exact zero_pow hn
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : MonoidWithZero M
inst✝¹ : NoZeroDivisors M
inst✝ : Nontrivial M
a : M
n : ℕ
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
[PROOFSTEP]
cases (zero_le n).eq_or_gt
[GOAL]
case inl
R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : MonoidWithZero M
inst✝¹ : NoZeroDivisors M
inst✝ : Nontrivial M
a : M
n : ℕ
h✝ : n = 0
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
[PROOFSTEP]
simp [*, ne_of_gt]
[GOAL]
case inr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : MonoidWithZero M
inst✝¹ : NoZeroDivisors M
inst✝ : Nontrivial M
a : M
n : ℕ
h✝ : 0 < n
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
[PROOFSTEP]
simp [*, ne_of_gt]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
a : M
n : ℕ
hn : n ≠ 0
⊢ a ^ n ≠ 0 → a ≠ 0
[PROOFSTEP]
contrapose!
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
a : M
n : ℕ
hn : n ≠ 0
⊢ a = 0 → a ^ n = 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
n : ℕ
hn : n ≠ 0
⊢ 0 ^ n = 0
[PROOFSTEP]
exact zero_pow' n hn
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
⊢ 0 ^ n = 0 ↔ 0 < n
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
⊢ 0 ^ n = 0 → 0 < n
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
⊢ 0 < n → 0 ^ n = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 ^ n = 0
⊢ 0 < n
[PROOFSTEP]
rw [pos_iff_ne_zero]
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 ^ n = 0
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
h : 0 ^ 0 = 0
⊢ False
[PROOFSTEP]
simp at h
[GOAL]
case mpr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 < n
⊢ 0 ^ n = 0
[PROOFSTEP]
exact zero_pow' n h.ne.symm
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
r : M
⊢ inverse r ^ 0 = inverse (r ^ 0)
[PROOFSTEP]
rw [pow_zero, pow_zero, Ring.inverse_one]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
r : M
n : ℕ
⊢ inverse r ^ (n + 1) = inverse (r ^ (n + 1))
[PROOFSTEP]
rw [pow_succ, pow_succ', Ring.mul_inverse_rev' ((Commute.refl r).pow_left n), Ring.inverse_pow r n]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ x ^ n ∣ x ^ m ↔ n ≤ m
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ x ^ n ∣ x ^ m → n ≤ m
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
⊢ n ≤ m
[PROOFSTEP]
rw [← not_lt]
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
⊢ ¬m < n
[PROOFSTEP]
intro hmn
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ False
[PROOFSTEP]
apply h1
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ IsUnit x
[PROOFSTEP]
have : x ^ m * x ∣ x ^ m * 1 := by
  rw [← pow_succ', mul_one]
  exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ x ^ m * x ∣ x ^ m * 1
[PROOFSTEP]
rw [← pow_succ', mul_one]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ x ^ (m + 1) ∣ x ^ m
[PROOFSTEP]
exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
this : x ^ m * x ∣ x ^ m * 1
⊢ IsUnit x
[PROOFSTEP]
rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
this : x ^ m * x ∣ x ^ m * 1
⊢ x ^ m ≠ 0
[PROOFSTEP]
apply pow_ne_zero m h0
[GOAL]
case mpr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ n ≤ m → x ^ n ∣ x ^ m
[PROOFSTEP]
apply pow_dvd_pow
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
ha : c ^ n ∣ a
hb : c ^ m ∣ b
⊢ c ^ min n m ∣ a + b
[PROOFSTEP]
replace ha := (pow_dvd_pow c (min_le_left n m)).trans ha
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
hb : c ^ m ∣ b
ha : c ^ min n m ∣ a
⊢ c ^ min n m ∣ a + b
[PROOFSTEP]
replace hb := (pow_dvd_pow c (min_le_right n m)).trans hb
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
ha : c ^ min n m ∣ a
hb : c ^ min n m ∣ b
⊢ c ^ min n m ∣ a + b
[PROOFSTEP]
exact dvd_add ha hb
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CommSemiring R
a b : R
⊢ (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
[PROOFSTEP]
simp only [sq, add_mul_self_eq]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CommSemiring R
a b : R
⊢ (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b
[PROOFSTEP]
rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ (-1) ^ (n + 1) = 1
[PROOFSTEP]
rw [pow_succ, h, neg_one_mul, neg_neg]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = 1
⊢ (-1) ^ (n + 1) = -1
[PROOFSTEP]
rw [pow_succ, h, mul_one]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
a : R
n : ℕ
⊢ (-a) ^ bit0 n = a ^ bit0 n
[PROOFSTEP]
rw [pow_bit0', neg_mul_neg, pow_bit0']
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
a : R
n : ℕ
⊢ (-a) ^ bit1 n = -a ^ bit1 n
[PROOFSTEP]
simp only [bit1, pow_succ, neg_pow_bit0, neg_mul_eq_neg_mul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
a : R
⊢ (-a) ^ 2 = a ^ 2
[PROOFSTEP]
simp [sq]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
⊢ (-1) ^ 2 = 1
[PROOFSTEP]
simp [neg_sq, one_pow]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
h : Commute a b
⊢ a ^ 2 - b ^ 2 = (a + b) * (a - b)
[PROOFSTEP]
rw [sq, sq, h.mul_self_sub_mul_self_eq]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
⊢ (-1) ^ n * r = 0 ↔ r = 0
[PROOFSTEP]
rcases neg_one_pow_eq_or R n with h | h
[GOAL]
case inl
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
h : (-1) ^ n = 1
⊢ (-1) ^ n * r = 0 ↔ r = 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
h : (-1) ^ n = -1
⊢ (-1) ^ n * r = 0 ↔ r = 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
⊢ r * (-1) ^ n = 0 ↔ r = 0
[PROOFSTEP]
rcases neg_one_pow_eq_or R n with h | h
[GOAL]
case inl
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
h : (-1) ^ n = 1
⊢ r * (-1) ^ n = 0 ↔ r = 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
h : (-1) ^ n = -1
⊢ r * (-1) ^ n = 0 ↔ r = 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
h : Commute a b
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
[PROOFSTEP]
rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
⊢ a ^ 2 = 1 ↔ a = 1 ∨ a = -1
[PROOFSTEP]
rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
[PROOFSTEP]
rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b
[PROOFSTEP]
rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a✝ b✝ : R
a b : Rˣ
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
[PROOFSTEP]
simp_rw [ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]