-- 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:
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} ⊔
      (Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
          Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker ⊔
        Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
          Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}) ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
apply sup_le

Result:
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)

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.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
        Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker ⊔
      Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
        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
⊢ P.ker ^ 2 ≤ Ideal.comap ((localizationAway g).toComp P).toAlgHom (RingHom.ker (compLocalizationAwayAlgHom T g P))

Tactic:
intro x hx

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
x : P.Ring
hx : x ∈ P.ker ^ 2
⊢ x ∈ Ideal.comap ((localizationAway g).toComp P).toAlgHom (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.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
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 hx]

Result:
no goals

Proof state:
case intro
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
a : ((localizationAway g).comp P).Ring
hx : ((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) * a ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
⊢ (compLocalizationAwayAlgHom T g P) (((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) * a) = 0

Tactic:
rw [map_mul, compLocalizationAwayAlgHom_relation_eq_zero, zero_mul]

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
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)

Tactic:
rw [comp_localizationAway_ker _ _ (P.σ g) (by simp), sq, Ideal.sup_mul, Ideal.mul_sup,
  Ideal.mul_sup]

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
⊢ 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} ⊔
      (Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
          Ideal.map ((localizationAway g).toComp P).toAlgHom P.ker ⊔
        Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
          Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}) ≤
    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
x : ((localizationAway g).comp P).Ring
hx : x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
⊢ (compLocalizationAwayAlgHom T g P) x = 0

Tactic:
obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton.mp hx

Result:
case intro
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
a : ((localizationAway g).comp P).Ring
hx : ((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) * a ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
⊢ (compLocalizationAwayAlgHom T g P) (((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) * a) = 0