-- Mathlib/RingTheory/CotangentLocalizationAway.lean
lemma sq_ker_comp_le_ker_compLocalizationAwayAlgHom :
    ((localizationAway g (S := T)).comp P).ker ^ 2 ≤
      RingHom.ker (compLocalizationAwayAlgHom T g P)

Proof state:
case a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
hsple :
  ∀ {x : ((localizationAway g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker * Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker ⊔
      Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker *
        Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
apply sup_le

Result:
case a.a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
hsple :
  ∀ {x : ((localizationAway g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker * Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

case a.a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
hsple :
  ∀ {x : ((localizationAway g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker *
      Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Proof state:
case a.a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
hsple :
  ∀ {x : ((localizationAway g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
x : ((localizationAway g).comp P).Ring
hx : x ∈ Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker
y : ((localizationAway g).comp P).Ring
hy : y ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
⊢ x * y ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
simp [hsple hy]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
⊢ ((localizationAway g).comp P).ker ^ 2 ≤ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
have hsple {x} (hx : x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}) :
      (compLocalizationAwayAlgHom T g P) x = 0 := by
  obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton.mp hx
  rw [map_mul, compLocalizationAwayAlgHom_relation_eq_zero, zero_mul]

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
hsple :
  ∀ {x : ((localizationAway g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ ((localizationAway g).comp P).ker ^ 2 ≤ RingHom.ker (compLocalizationAwayAlgHom T g P)

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
hsple :
  ∀ {x : ((localizationAway g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ (algebraMap P.Ring S) (P.σ g) = g

Tactic:
simp

Result:
no goals

Proof state:
case a.a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
hsple :
  ∀ {x : ((localizationAway g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker * Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
rw [← Ideal.map_mul, Ideal.map_le_iff_le_comap, ← sq]

Result:
case a.a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
hsple :
  ∀ {x : ((localizationAway g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ P.ker ^ 2 ≤ Ideal.comap ((localizationAway g).toComp P).toAlgHom (RingHom.ker (compLocalizationAwayAlgHom T g P))