[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ AddCommGroup (Cotangent I)
[PROOFSTEP]
delta Cotangent
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ AddCommGroup ({ x // x ∈ I } ⧸ I • ⊤)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Module (R ⧸ I) (Cotangent I)
[PROOFSTEP]
delta Cotangent
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Module (R ⧸ I) ({ x // x ∈ I } ⧸ I • ⊤)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Submodule.map (Submodule.subtype I) (LinearMap.ker (toCotangent I)) = I ^ 2
[PROOFSTEP]
rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
  Algebra.id.smul_eq_mul, Submodule.map_subtype_top]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : { x // x ∈ I }
⊢ x ∈ LinearMap.ker (toCotangent I) ↔ ↑x ∈ I ^ 2
[PROOFSTEP]
rw [← I.map_toCotangent_ker]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : { x // x ∈ I }
⊢ x ∈ LinearMap.ker (toCotangent I) ↔ ↑x ∈ Submodule.map (Submodule.subtype I) (LinearMap.ker (toCotangent I))
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : { x // x ∈ I }
⊢ ↑(toCotangent I) x = ↑(toCotangent I) y ↔ ↑x - ↑y ∈ I ^ 2
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : { x // x ∈ I }
⊢ ↑(toCotangent I) x - ↑(toCotangent I) y = 0 ↔ ↑x - ↑y ∈ I ^ 2
[PROOFSTEP]
exact I.mem_toCotangent_ker
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Subsingleton (Cotangent I) ↔ IsIdempotentElem I
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Subsingleton (Cotangent I) → IsIdempotentElem I
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
H : Subsingleton (Cotangent I)
⊢ IsIdempotentElem I
[PROOFSTEP]
refine' (pow_two I).symm.trans (le_antisymm (Ideal.pow_le_self two_ne_zero) _)
[GOAL]
case mp
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
H : Subsingleton (Cotangent I)
⊢ I ≤ I ^ 2
[PROOFSTEP]
exact fun x hx => (I.toCotangent_eq_zero ⟨x, hx⟩).mp (Subsingleton.elim _ _)
[GOAL]
case mpr
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ IsIdempotentElem I → Subsingleton (Cotangent I)
[PROOFSTEP]
exact fun e =>
  ⟨fun x y =>
    Quotient.inductionOn₂' x y fun x y => I.toCotangent_eq.mpr <| ((pow_two I).trans e).symm ▸ I.sub_mem x.prop y.prop⟩
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ I • ⊤ ≤ Submodule.comap (Submodule.subtype I) (I ^ 2)
[PROOFSTEP]
rw [← Submodule.map_le_iff_le_comap, Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype, smul_eq_mul,
  pow_two]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
⊢ cotangentIdeal I ^ 2 = ⊥
[PROOFSTEP]
rw [eq_bot_iff, pow_two I.cotangentIdeal, ← smul_eq_mul]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
⊢ cotangentIdeal I • cotangentIdeal I ≤ ⊥
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x : R ⧸ I ^ 2
hx : x ∈ cotangentIdeal I • cotangentIdeal I
⊢ x ∈ ⊥
[PROOFSTEP]
refine Submodule.smul_induction_on hx ?_ ?_
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x : R ⧸ I ^ 2
hx : x ∈ cotangentIdeal I • cotangentIdeal I
⊢ ∀ (r : R ⧸ I ^ 2), r ∈ cotangentIdeal I → ∀ (n : R ⧸ I ^ 2), n ∈ cotangentIdeal I → r • n ∈ ⊥
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
[GOAL]
case refine_1.intro.intro.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ cotangentIdeal I • cotangentIdeal I
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ ↑(RingHom.toSemilinearMap (Quotient.mk (I ^ 2))) x • ↑(RingHom.toSemilinearMap (Quotient.mk (I ^ 2))) y ∈ ⊥
[PROOFSTEP]
apply (Submodule.Quotient.eq _).mpr _
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ cotangentIdeal I • cotangentIdeal I
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x x_1 => x * x_1) x y - 0 ∈ I ^ 2
[PROOFSTEP]
rw [sub_zero, pow_two]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ cotangentIdeal I • cotangentIdeal I
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x x_1 => x * x_1) x y ∈ I * I
[PROOFSTEP]
exact Ideal.mul_mem_mul hx hy
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x : R ⧸ I ^ 2
hx : x ∈ cotangentIdeal I • cotangentIdeal I
⊢ ∀ (x y : R ⧸ I ^ 2), x ∈ ⊥ → y ∈ ⊥ → x + y ∈ ⊥
[PROOFSTEP]
intro x y hx hy
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ cotangentIdeal I • cotangentIdeal I
x y : R ⧸ I ^ 2
hx : x ∈ ⊥
hy : y ∈ ⊥
⊢ x + y ∈ ⊥
[PROOFSTEP]
exact add_mem hx hy
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ LinearMap.range (cotangentToQuotientSquare I) = Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
trans LinearMap.range (I.cotangentToQuotientSquare.comp I.toCotangent)
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ LinearMap.range (cotangentToQuotientSquare I) =
    LinearMap.range (LinearMap.comp (cotangentToQuotientSquare I) (toCotangent I))
[PROOFSTEP]
rw [LinearMap.range_comp, I.toCotangent_range, Submodule.map_top]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ LinearMap.range (LinearMap.comp (cotangentToQuotientSquare I) (toCotangent I)) =
    Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
rw [to_quotient_square_comp_toCotangent, LinearMap.range_comp, I.range_subtype]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Submodule.map (Submodule.mkQ (I ^ 2)) I = Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x✝ : R ⧸ I ^ 2
⊢ x✝ ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I ↔ x✝ ∈ Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Cotangent I ≃ₗ[R] { x // x ∈ cotangentIdeal I }
[PROOFSTEP]
refine
  {
    LinearMap.codRestrict (I.cotangentIdeal.restrictScalars R) I.cotangentToQuotientSquare fun x => by
      {rw [← to_quotient_square_range]; exact LinearMap.mem_range_self _ _
    },
    Equiv.ofBijective _ ⟨?_, ?_⟩ with }
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : Cotangent I
⊢ ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
{rw [← to_quotient_square_range]; exact LinearMap.mem_range_self _ _
}
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : Cotangent I
⊢ ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
rw [← to_quotient_square_range]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : Cotangent I
⊢ ↑(cotangentToQuotientSquare I) x ∈ LinearMap.range (cotangentToQuotientSquare I)
[PROOFSTEP]
exact LinearMap.mem_range_self _ _
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
⊢ Function.Injective fun c =>
    { val := ↑(cotangentToQuotientSquare I) c,
      property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) }
[PROOFSTEP]
rintro x y e
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x y : Cotangent I
e :
  (fun c =>
        { val := ↑(cotangentToQuotientSquare I) c,
          property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
      x =
    (fun c =>
        { val := ↑(cotangentToQuotientSquare I) c,
          property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
      y
⊢ x = y
[PROOFSTEP]
replace e := congr_arg Subtype.val e
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x y : Cotangent I
e :
  ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        x) =
    ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        y)
⊢ x = y
[PROOFSTEP]
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
[GOAL]
case refine_1.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
y : Cotangent I
x : { x // x ∈ I }
e :
  ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        (↑(toCotangent I) x)) =
    ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        y)
⊢ ↑(toCotangent I) x = y
[PROOFSTEP]
obtain ⟨y, rfl⟩ := I.toCotangent_surjective y
[GOAL]
case refine_1.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x y : { x // x ∈ I }
e :
  ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        (↑(toCotangent I) x)) =
    ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        (↑(toCotangent I) y))
⊢ ↑(toCotangent I) x = ↑(toCotangent I) y
[PROOFSTEP]
rw [I.toCotangent_eq]
[GOAL]
case refine_1.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x y : { x // x ∈ I }
e :
  ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        (↑(toCotangent I) x)) =
    ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        (↑(toCotangent I) y))
⊢ ↑x - ↑y ∈ I ^ 2
[PROOFSTEP]
dsimp only [toCotangent_to_quotient_square, Submodule.mkQ_apply] at e
[GOAL]
case refine_1.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x y : { x // x ∈ I }
e : Submodule.Quotient.mk ↑x = Submodule.Quotient.mk ↑y
⊢ ↑x - ↑y ∈ I ^ 2
[PROOFSTEP]
rwa [Submodule.Quotient.eq] at e
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
⊢ Function.Surjective fun c =>
    { val := ↑(cotangentToQuotientSquare I) c,
      property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) }
[PROOFSTEP]
rintro ⟨_, x, hx, rfl⟩
[GOAL]
case refine_2.mk.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x : R
hx : x ∈ ↑I
⊢ ∃ a,
    (fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        a =
      { val := ↑(RingHom.toSemilinearMap (Quotient.mk (I ^ 2))) x,
        property :=
          (_ :
            ∃ a,
              a ∈ ↑I ∧
                ↑(RingHom.toSemilinearMap (Quotient.mk (I ^ 2))) a =
                  ↑(RingHom.toSemilinearMap (Quotient.mk (I ^ 2))) x) }
[PROOFSTEP]
exact ⟨I.toCotangent ⟨x, hx⟩, Subtype.ext rfl⟩
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑(LinearEquiv.symm (cotangentEquivIdeal I))
      { val := ↑(Submodule.mkQ (I ^ 2)) x,
        property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(toCotangent I) { val := x, property := hx }
[PROOFSTEP]
apply I.cotangentEquivIdeal.injective
[GOAL]
case a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑(cotangentEquivIdeal I)
      (↑(LinearEquiv.symm (cotangentEquivIdeal I))
        { val := ↑(Submodule.mkQ (I ^ 2)) x,
          property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) }) =
    ↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx })
[PROOFSTEP]
rw [I.cotangentEquivIdeal.apply_symm_apply]
[GOAL]
case a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ { val := ↑(Submodule.mkQ (I ^ 2)) x,
      property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx })
[PROOFSTEP]
ext
[GOAL]
case a.a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑{ val := ↑(Submodule.mkQ (I ^ 2)) x,
        property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx }))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ A ⧸ RingHom.ker ↑f ^ 2 →ₐ[R] B
[PROOFSTEP]
refine { Ideal.Quotient.lift (RingHom.ker f.toRingHom ^ 2) f.toRingHom ?_ with commutes' := ?_ }
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ ∀ (a : A), a ∈ RingHom.ker ↑f ^ 2 → ↑↑f a = 0
[PROOFSTEP]
intro a ha
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
ha : a ∈ RingHom.ker ↑f ^ 2
⊢ ↑↑f a = 0
[PROOFSTEP]
exact Ideal.pow_le_self two_ne_zero ha
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
src✝ : A ⧸ RingHom.ker ↑f ^ 2 →+* B :=
  Quotient.lift (RingHom.ker ↑f ^ 2) ↑f (_ : ∀ (a : A), a ∈ RingHom.ker ↑f ^ 2 → a ∈ RingHom.ker ↑f)
⊢ ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ :
                  ∀ (x y : A ⧸ RingHom.ker ↑f ^ 2),
                    OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
        (↑(algebraMap R (A ⧸ RingHom.ker ↑f ^ 2)) r) =
      ↑(algebraMap R B) r
[PROOFSTEP]
intro r
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
src✝ : A ⧸ RingHom.ker ↑f ^ 2 →+* B :=
  Quotient.lift (RingHom.ker ↑f ^ 2) ↑f (_ : ∀ (a : A), a ∈ RingHom.ker ↑f ^ 2 → a ∈ RingHom.ker ↑f)
r : R
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : A ⧸ RingHom.ker ↑f ^ 2),
                  OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R (A ⧸ RingHom.ker ↑f ^ 2)) r) =
    ↑(algebraMap R B) r
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply R A, RingHom.toFun_eq_coe, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.lift_mk]
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
src✝ : A ⧸ RingHom.ker ↑f ^ 2 →+* B :=
  Quotient.lift (RingHom.ker ↑f ^ 2) ↑f (_ : ∀ (a : A), a ∈ RingHom.ker ↑f ^ 2 → a ∈ RingHom.ker ↑f)
r : R
⊢ ↑↑f (↑(algebraMap R A) r) = ↑(algebraMap R B) r
[PROOFSTEP]
exact f.map_algebraMap r
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ RingHom.ker ↑(AlgHom.kerSquareLift f) = cotangentIdeal (RingHom.ker ↑f)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ RingHom.ker ↑(AlgHom.kerSquareLift f) ≤ cotangentIdeal (RingHom.ker ↑f)
[PROOFSTEP]
intro x hx
[GOAL]
case a
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A ⧸ RingHom.ker ↑f ^ 2
hx : x ∈ RingHom.ker ↑(AlgHom.kerSquareLift f)
⊢ x ∈ cotangentIdeal (RingHom.ker ↑f)
[PROOFSTEP]
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
[GOAL]
case a.intro
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A
hx : ↑(Quotient.mk (RingHom.ker ↑f ^ 2)) x ∈ RingHom.ker ↑(AlgHom.kerSquareLift f)
⊢ ↑(Quotient.mk (RingHom.ker ↑f ^ 2)) x ∈ cotangentIdeal (RingHom.ker ↑f)
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
case a
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ cotangentIdeal (RingHom.ker ↑f) ≤ RingHom.ker ↑(AlgHom.kerSquareLift f)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case a.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A
hx : x ∈ ↑(RingHom.ker ↑f)
⊢ ↑(RingHom.toSemilinearMap (Quotient.mk (RingHom.ker ↑f ^ 2))) x ∈ RingHom.ker ↑(AlgHom.kerSquareLift f)
[PROOFSTEP]
exact hx
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ (R ⧸ I ^ 2) ⧸ cotangentIdeal I ≃+* R ⧸ I
[PROOFSTEP]
refine (Ideal.quotEquivOfEq (Ideal.map_eq_submodule_map _ _).symm).trans ?_
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ (R ⧸ I ^ 2) ⧸ map (Quotient.mk (I ^ 2)) I ≃+* R ⧸ I
[PROOFSTEP]
refine (DoubleQuot.quotQuotEquivQuotSup _ _).trans ?_
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ R ⧸ I ^ 2 ⊔ I ≃+* R ⧸ I
[PROOFSTEP]
exact Ideal.quotEquivOfEq (sup_eq_right.mpr <| Ideal.pow_le_self two_ne_zero)


[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
p q : NonUnitalSubring R
h : (fun s => s.carrier) p = (fun s => s.carrier) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
q : NonUnitalSubring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } =
    (fun s => s.carrier) q
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toNonUnitalSubsemiring
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ toNonUnitalSubsemiring✝¹ = toNonUnitalSubsemiring✝
[PROOFSTEP]
exact SetLike.coe_injective h
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
s : NonUnitalSubring R
x : { x // x ∈ s }
⊢ ↑x = 0 ↔ x = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type u_1
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
g : S →ₙ+* T
f✝ f : R →ₙ+* S
⊢ range f = NonUnitalSubring.map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
T : Type u_1
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
g : S →ₙ+* T
f✝ f : R →ₙ+* S
x✝ : S
⊢ x✝ ∈ range f ↔ x✝ ∈ NonUnitalSubring.map f ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type u_1
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ NonUnitalSubring.map g (range f) = range (comp g f)
[PROOFSTEP]
simpa only [range_eq_map] using (⊤ : NonUnitalSubring R).map_map g f
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
x : R
⊢ x ∈ ↑⊥ ↔ x = 0
[PROOFSTEP]
rw [coe_bot, Set.mem_singleton_iff]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set (NonUnitalSubring R)
⊢ ↑(⨅ (t : NonUnitalSubring R) (_ : t ∈ s), toSubsemigroup t) = ⋂ (t : NonUnitalSubring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set (NonUnitalSubring R)
⊢ ↑(⨅ (t : NonUnitalSubring R) (_ : t ∈ s), toAddSubgroup t) = ⋂ (t : NonUnitalSubring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
S : ι → NonUnitalSubring R
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
[PROOFSTEP]
simp only [iInf, coe_sInf, Set.biInter_range]
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
S : ι → NonUnitalSubring R
x : R
⊢ x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i
[PROOFSTEP]
simp only [iInf, mem_sInf, Set.forall_range_iff]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ p { val := b, property := hb }
[PROOFSTEP]
refine' Exists.elim _ fun (hb : b ∈ closure s) (hc : p ⟨b, hb⟩) => hc
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ ∃ x, p { val := b, property := x }
[PROOFSTEP]
refine' closure_induction hb (fun x hx => ⟨subset_closure hx, Hs x hx⟩) ⟨zero_mem (closure s), H0⟩ _ _ _
[GOAL]
case refine'_1
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ ∀ (x y : R),
    (∃ x_1, p { val := x, property := x_1 }) →
      (∃ x, p { val := y, property := x }) → ∃ x_1, p { val := x + y, property := x_1 }
[PROOFSTEP]
rintro x y ⟨hx, hpx⟩ ⟨hy, hpy⟩
[GOAL]
case refine'_1.intro.intro
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
x y : R
hx : x ∈ closure s
hpx : p { val := x, property := hx }
hy : y ∈ closure s
hpy : p { val := y, property := hy }
⊢ ∃ x_1, p { val := x + y, property := x_1 }
[PROOFSTEP]
exact ⟨add_mem hx hy, Hadd _ _ hpx hpy⟩
[GOAL]
case refine'_2
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ ∀ (x : R), (∃ x_1, p { val := x, property := x_1 }) → ∃ x_1, p { val := -x, property := x_1 }
[PROOFSTEP]
rintro x ⟨hx, hpx⟩
[GOAL]
case refine'_2.intro
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
x : R
hx : x ∈ closure s
hpx : p { val := x, property := hx }
⊢ ∃ x_1, p { val := -x, property := x_1 }
[PROOFSTEP]
exact ⟨neg_mem hx, Hneg _ hpx⟩
[GOAL]
case refine'_3
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ ∀ (x y : R),
    (∃ x_1, p { val := x, property := x_1 }) →
      (∃ x, p { val := y, property := x }) → ∃ x_1, p { val := x * y, property := x_1 }
[PROOFSTEP]
rintro x y ⟨hx, hpx⟩ ⟨hy, hpy⟩
[GOAL]
case refine'_3.intro.intro
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
x y : R
hx : x ∈ closure s
hpx : p { val := x, property := hx }
hy : y ∈ closure s
hpy : p { val := y, property := hy }
⊢ ∃ x_1, p { val := x * y, property := x_1 }
[PROOFSTEP]
exact ⟨mul_mem hx hy, Hmul _ _ hpx hpy⟩
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ p a b
[PROOFSTEP]
refine' closure_induction hb _ (H0_right _) (Hadd_right a) (Hneg_right a) (Hmul_right a)
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : R), x ∈ s → p a x
[PROOFSTEP]
refine' closure_induction ha Hs (fun x _ => H0_left x) _ _ _
[GOAL]
case refine'_1
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x y : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → (∀ (x : R), x ∈ s → p y x) → ∀ (x_1 : R), x_1 ∈ s → p (x + y) x_1
[PROOFSTEP]
exact fun x y H₁ H₂ z zs => Hadd_left x y z (H₁ z zs) (H₂ z zs)
[GOAL]
case refine'_2
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → ∀ (x_1 : R), x_1 ∈ s → p (-x) x_1
[PROOFSTEP]
exact fun x hx z zs => Hneg_left x z (hx z zs)
[GOAL]
case refine'_3
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x y : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → (∀ (x : R), x ∈ s → p y x) → ∀ (x_1 : R), x_1 ∈ s → p (x * y) x_1
[PROOFSTEP]
exact fun x y H₁ H₂ z zs => Hmul_left x y z (H₁ z zs) (H₂ z zs)
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
⊢ 0 * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [zero_mul q]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
⊢ 0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.zero_mem _
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
p₁ p₂ : R
ihp₁ : p₁ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
ihp₂ : p₂ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ (p₁ + p₂) * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [add_mul p₁ p₂ q]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
p₁ p₂ : R
ihp₁ : p₁ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
ihp₂ : p₂ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ p₁ * q + p₂ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.add_mem _ ihp₁ ihp₂
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ -x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
have f : -x * q = -(x * q) := by simp
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ -x * q = -(x * q)
[PROOFSTEP]
simp
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f✝ : R →ₙ+* S
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
f : -x * q = -(x * q)
⊢ -x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [f]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f✝ : R →ₙ+* S
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
f : -x * q = -(x * q)
⊢ -(x * q) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.neg_mem _ hx
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x * 0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [mul_zero x]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ 0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.zero_mem _
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q₁ q₂ : R
ihq₁ : x * q₁ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
ihq₂ : x * q₂ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x * (q₁ + q₂) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [mul_add x q₁ q₂]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q₁ q₂ : R
ihq₁ : x * q₁ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
ihq₂ : x * q₂ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x * q₁ + x * q₂ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.add_mem _ ihq₁ ihq₂
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x * -z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
have f : x * -z = -(x * z) := by simp
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x * -z = -(x * z)
[PROOFSTEP]
simp
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f✝ : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
f : x * -z = -(x * z)
⊢ x * -z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [f]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f✝ : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
f : x * -z = -(x * z)
⊢ -(x * z) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.neg_mem _ hz
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x y : { x // x ∈ closure s }
⊢ x * y = y * x
[PROOFSTEP]
ext
[GOAL]
case a
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x y : { x // x ∈ closure s }
⊢ ↑(x * y) = ↑(y * x)
[PROOFSTEP]
simp only [NonUnitalSubring.val_mul]
[GOAL]
case a
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x y : { x // x ∈ closure s }
⊢ ↑x * ↑y = ↑y * ↑x
[PROOFSTEP]
refine'
  closure_induction₂ x.prop y.prop hcomm (fun x => by simp only [mul_zero, zero_mul])
    (fun x => by simp only [mul_zero, zero_mul]) (fun x y hxy => by simp only [mul_neg, neg_mul, hxy])
    (fun x y hxy => by simp only [mul_neg, neg_mul, hxy]) (fun x₁ x₂ y h₁ h₂ => by simp only [add_mul, mul_add, h₁, h₂])
    (fun x₁ x₂ y h₁ h₂ => by simp only [add_mul, mul_add, h₁, h₂])
    (fun x₁ x₂ y h₁ h₂ => by rw [← mul_assoc, ← h₁, mul_assoc x₁ y x₂, ← h₂, mul_assoc]) fun x₁ x₂ y h₁ h₂ => by
    rw [← mul_assoc, h₁, mul_assoc, h₂, ← mul_assoc]
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ 0 * x = x * 0
[PROOFSTEP]
simp only [mul_zero, zero_mul]
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ x * 0 = 0 * x
[PROOFSTEP]
simp only [mul_zero, zero_mul]
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x✝ y✝ : { x // x ∈ closure s }
x y : R
hxy : x * y = y * x
⊢ -x * y = y * -x
[PROOFSTEP]
simp only [mul_neg, neg_mul, hxy]
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x✝ y✝ : { x // x ∈ closure s }
x y : R
hxy : x * y = y * x
⊢ x * -y = -y * x
[PROOFSTEP]
simp only [mul_neg, neg_mul, hxy]
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * y = y * x₁
h₂ : x₂ * y = y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)
[PROOFSTEP]
simp only [add_mul, mul_add, h₁, h₂]
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * x₂ = x₂ * x₁
h₂ : x₁ * y = y * x₁
⊢ x₁ * (x₂ + y) = (x₂ + y) * x₁
[PROOFSTEP]
simp only [add_mul, mul_add, h₁, h₂]
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * y = y * x₁
h₂ : x₂ * y = y * x₂
⊢ x₁ * x₂ * y = y * (x₁ * x₂)
[PROOFSTEP]
rw [← mul_assoc, ← h₁, mul_assoc x₁ y x₂, ← h₂, mul_assoc]
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * x₂ = x₂ * x₁
h₂ : x₁ * y = y * x₁
⊢ x₁ * (x₂ * y) = x₂ * y * x₁
[PROOFSTEP]
rw [← mul_assoc, h₁, mul_assoc, h₂, ← mul_assoc]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : NonUnitalSubring R
x : R × S
⊢ x ∈ prod s ⊤ ↔ x ∈ comap (NonUnitalRingHom.fst R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_fst]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : NonUnitalSubring S
x : R × S
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (NonUnitalRingHom.snd R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_snd]
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i ↔ ∃ i, x ∈ S i
[PROOFSTEP]
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
let U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup)
    (Subsemigroup.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
    (AddSubgroup.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i)) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i)))
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
suffices (⨆ i, S i) ≤ U by simpa using @this x
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i)) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i)))
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
this : ⨆ (i : ι), S i ≤ U
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
simpa using @this x
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i)) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i)))
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ ⨆ (i : ι), S i ≤ U
[PROOFSTEP]
exact iSup_le fun i x hx => Set.mem_iUnion.2 ⟨i, hx⟩
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
[PROOFSTEP]
simp [mem_iSup_of_directed hS]
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
S : Set (NonUnitalSubring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
haveI : Nonempty S := Sne.to_subtype
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
S : Set (NonUnitalSubring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk, exists_prop]
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
S : Set (NonUnitalSubring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : NonUnitalSubring R) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp [mem_sSup_of_directedOn Sne hS]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f✝ : R →ₙ+* S
s : NonUnitalSubring R
f : R →ₙ+* S
⊢ ↑(range f) = ↑⊤ ↔ Set.range ↑f = Set.univ
[PROOFSTEP]
rw [coe_range, coe_top]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalRing R
inst✝² : NonUnitalRing S
inst✝¹ : NonUnitalRing T
inst✝ : NonUnitalRingHomClass F R S
g✝ : S →ₙ+* T
f✝ : R →ₙ+* S
s t : NonUnitalSubring R
g : S → R
f : R →ₙ+* S
h : Function.LeftInverse g ↑f
src✝ : R →ₙ+* { x // x ∈ NonUnitalRingHom.range f } := NonUnitalRingHom.rangeRestrict f
x : { x // x ∈ NonUnitalRingHom.range f }
x' : R
hx' : ↑f x' = ↑x
⊢ ↑f (g ↑x) = ↑x
[PROOFSTEP]
rw [← hx', h x']


[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ ↑(opRingEquiv R) (op (↑(monomial n) r)) = ↑(monomial n) (op r)
[PROOFSTEP]
simp only [opRingEquiv, RingEquiv.coe_trans, Function.comp_apply, AddMonoidAlgebra.opRingEquiv_apply,
  RingEquiv.op_apply_apply, toFinsuppIso_apply, unop_op, toFinsupp_monomial, Finsupp.mapRange_single,
  toFinsuppIso_symm_apply, ofFinsupp_single]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ ↑(opRingEquiv R) (op (↑C r * X ^ n)) = ↑C (op r) * X ^ n
[PROOFSTEP]
simp only [X_pow_mul, op_mul, op_pow, map_mul, map_pow, opRingEquiv_op_X, opRingEquiv_op_C]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : Rᵐᵒᵖ
⊢ ↑(opRingEquiv R) (↑(RingEquiv.symm (opRingEquiv R)) (↑(monomial n) r)) =
    ↑(opRingEquiv R) (op (↑(monomial n) (unop r)))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : Rᵐᵒᵖ
n : ℕ
⊢ ↑(RingEquiv.symm (opRingEquiv R)) (↑C r * X ^ n) = op (↑C (unop r) * X ^ n)
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, opRingEquiv_symm_monomial, C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
n : ℕ
⊢ coeff (↑(opRingEquiv R) p) n = op (coeff (unop p) n)
[PROOFSTEP]
induction' p using MulOpposite.rec' with p
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
n : ℕ
p : R[X]
⊢ coeff (↑(opRingEquiv R) (op p)) n = op (coeff (unop (op p)) n)
[PROOFSTEP]
cases p
[GOAL]
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (↑(opRingEquiv R) (op { toFinsupp := toFinsupp✝ })) n = op (coeff (unop (op { toFinsupp := toFinsupp✝ })) n)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ support (↑(opRingEquiv R) p) = support (unop p)
[PROOFSTEP]
induction' p using MulOpposite.rec' with p
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ support (↑(opRingEquiv R) (op p)) = support (unop (op p))
[PROOFSTEP]
cases p
[GOAL]
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (↑(opRingEquiv R) (op { toFinsupp := toFinsupp✝ })) = support (unop (op { toFinsupp := toFinsupp✝ }))
[PROOFSTEP]
exact Finsupp.support_mapRange_of_injective (map_zero _) _ op_injective
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)
[PROOFSTEP]
by_cases p0 : p = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : p = 0
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)
[PROOFSTEP]
simp only [p0, _root_.map_zero, natDegree_zero, unop_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : ¬p = 0
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)
[PROOFSTEP]
simp only [p0, natDegree_eq_support_max', Ne.def, AddEquivClass.map_eq_zero_iff, not_false_iff, support_opRingEquiv,
  unop_eq_zero_iff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ leadingCoeff (↑(opRingEquiv R) p) = op (leadingCoeff (unop p))
[PROOFSTEP]
rw [leadingCoeff, coeff_opRingEquiv, natDegree_opRingEquiv, leadingCoeff]