mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case mul_X
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
Q : Generators S T ι
Q' : Generators S T ι'
f : Q.Hom Q'
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
p : MvPolynomial ι S
n : ι
IH :
  (δAux R Q') (f.toAlgHom p) =
    (δAux R Q) p +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p))
⊢ eval₂ (algebraMap S T) (fun i ↦ Q.val i) p • (δAux R Q') (f.val n) +
      (Q.val n • (δAux R Q) p +
        Q.val n •
          (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
            (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p))) =
    Q.val n • (δAux R Q) p +
      ((aeval Q.val) p • (δAux R Q') (f.val n) +
        Q.val n •
          (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
            (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p)))

Tactic:
rw [add_left_comm]

Goal state after:
case mul_X
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
Q : Generators S T ι
Q' : Generators S T ι'
f : Q.Hom Q'
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
p : MvPolynomial ι S
n : ι
IH :
  (δAux R Q') (f.toAlgHom p) =
    (δAux R Q) p +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p))
⊢ Q.val n • (δAux R Q) p +
      (eval₂ (algebraMap S T) (fun i ↦ Q.val i) p • (δAux R Q') (f.val n) +
        Q.val n •
          (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
            (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p))) =
    Q.val n • (δAux R Q) p +
      ((aeval Q.val) p • (δAux R Q') (f.val n) +
        Q.val n •
          (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
            (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p)))
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
⊢ σ (a * b) - ↑(l (1 ⊗ₜ[P] (D R P) (σ (a * b)))) =
    (σ a - ↑(l (1 ⊗ₜ[P] (D R P) (σ a)))) * (σ b - ↑(l (1 ⊗ₜ[P] (D R P) (σ b))))

Tactic:
have (x y : _) : (l x).1 * (l y).1 = 0 := by
      rw [← Ideal.mem_bot, ← hf', pow_two]; exact Ideal.mul_mem_mul (l x).2 (l y).2

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
this : ∀ (x y : S ⊗[P] Ω[P⁄R]), ↑(l x) * ↑(l y) = 0
⊢ σ (a * b) - ↑(l (1 ⊗ₜ[P] (D R P) (σ (a * b)))) =
    (σ a - ↑(l (1 ⊗ₜ[P] (D R P) (σ a)))) * (σ b - ↑(l (1 ⊗ₜ[P] (D R P) (σ b))))
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
g : { g // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }
⊢ (fun l ↦ ⟨sectionOfRetractionKerToTensor ↑l ⋯ hf' hf, ⋯⟩)
      ((fun g ↦ ⟨retractionOfSectionOfKerSqZero (↑g) hf' ⋯, ⋯⟩) g) =
    g

Tactic:
ext s; obtain ⟨s, rfl⟩ := hf s; simp

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (LinearMap.baseChange T P.toExtension.toKaehler) z = (δAux R Q) ↑x

Tactic:
← ofComp_kerCompPreimage Q P x,

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (LinearMap.baseChange T P.toExtension.toKaehler) z = (δAux R Q) ((Q.ofComp P).toAlgHom ↑(Q.kerCompPreimage P x))
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : Algebra.FormallyEtale S T
⊢ Function.Injective ⇑(mapBaseChange R S T)

Tactic:
rw [injective_iff_map_eq_zero]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : Algebra.FormallyEtale S T
⊢ ∀ (a : T ⊗[S] Ω[S⁄R]), (mapBaseChange R S T) a = 0 → a = 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul.zero
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
⊢ ↑(e (a ⊗ₜ[P.Ring] b)) •
      (LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk)) 0 =
    0

Tactic:
simp only [map_zero, smul_zero]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝⁴ : FiniteType K A
this✝³ : Module.Finite K (Localization.AtPrime Q)
this✝² : IsField (Localization.AtPrime Q)
this✝¹ : Field (Localization.AtPrime Q) := this✝².toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this✝ : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
H : q * q ∣ p
this : q ∣ m
⊢ False

Tactic:
minpoly.dvd_iff,

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝⁴ : FiniteType K A
this✝³ : Module.Finite K (Localization.AtPrime Q)
this✝² : IsField (Localization.AtPrime Q)
this✝¹ : Field (Localization.AtPrime Q) := this✝².toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this✝ : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
H : q * q ∣ p
this : (aeval ((algebraMap A Q.ResidueField) x)) m = 0
⊢ False
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case left
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Injective ⇑(map P.toInfinitesimal)

Tactic:
rw [injective_iff_map_eq_zero]

Goal state after:
case left
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ∀ (a : P.Cotangent), (map P.toInfinitesimal) a = 0 → a = 0
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
⊢ Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)

Tactic:
rw [injective_iff_map_eq_zero]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
⊢ ∀ (a : Localization.AtPrime p), (localRingHom p q (algebraMap R S) ⋯) a = 0 → a = 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
b : ↥P.ker
a : Q.Ring
⊢ (tensorCotangentInvFun f halg H)
      ((LinearMap.liftBaseChange T (Cotangent.map f)) ((algebraMap Q.Ring T) a ⊗ₜ[S] Cotangent.mk b)) =
    (algebraMap Q.Ring T) a ⊗ₜ[S] Cotangent.mk b

Tactic:
simp only [LinearMap.liftBaseChange_tmul, Cotangent.map_mk, Hom.toAlgHom_apply,
          algebraMap_smul]

Goal state after:
case tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
b : ↥P.ker
a : Q.Ring
⊢ (tensorCotangentInvFun f halg H) (a • Cotangent.mk ⟨f.toRingHom ↑b, ⋯⟩) = (algebraMap Q.Ring T) a ⊗ₜ[S] Cotangent.mk b
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))

Tactic:
rw [injective_iff_map_eq_zero]

Goal state after:
case left
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ ∀ (a : T ⊗[S] P.H1Cotangent), (LinearMap.liftBaseChange T (H1Cotangent.map f)) a = 0 → a = 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
⊢ (LinearMap.baseChange T P.cotangentComplex) ((tensorCotangent f halg H₂).symm ↑x) = 0

Tactic:
apply (Extension.tensorCotangentSpaceOfFormallyEtale f H₁).injective

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
⊢ (tensorCotangentSpaceOfFormallyEtale f H₁)
      ((LinearMap.baseChange T P.cotangentComplex) ((tensorCotangent f halg H₂).symm ↑x)) =
    (tensorCotangentSpaceOfFormallyEtale f H₁) 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T

Tactic:
letI Q : Extension R T := .ofSurjective fQ (by
    intro x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x
    obtain ⟨x, rfl⟩ := P.algebraMap_surjective x
    obtain ⟨s, rfl⟩ := P.algebraMap_surjective s
    refine ⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩
    simp only [fQ, IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe]
    rw [IsLocalization.lift_mk'_spec]
    simp)

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
⊢ Function.Injective ⇑(awayMap (algebraMap R S) r')

Tactic:
rw [injective_iff_map_eq_zero]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
⊢ ∀ (a : Away r'), (awayMap (algebraMap R S) r') a = 0 → a = 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
⊢ Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (Algebra.linearMap P.Ring S).ker =
    RingHom.ker fQ

Tactic:
LinearMap.localized'_ker_eq_ker_localizedMap (Localization M') M'
        (Algebra.linearMap P.Ring (Localization M'))
        (f' := (IsScalarTower.toAlgHom P.Ring S T).toLinearMap)

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
⊢ (LinearMap.extendScalarsOfIsLocalization M' (Localization M')
        ((IsLocalizedModule.map M' (Algebra.linearMap P.Ring (Localization M'))
            (IsScalarTower.toAlgHom P.Ring S T).toLinearMap)
          (Algebra.linearMap P.Ring S))).ker =
    RingHom.ker fQ
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
⊢ sInf (s * t⁻¹) = sInf s * (sSup t)⁻¹

Tactic:
sInf_mul,

Goal state after:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
⊢ sInf s * sInf t⁻¹ = sInf s * (sSup t)⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk I).factors)) ≠ 1}.Finite

Tactic:
simp_rw [zpow_neg, Ne, inv_eq_one]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ¬↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) = 1}.Finite
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
a : ℝ
ha : a ≤ 0
hs : ∀ x ∈ ∅, a ≤ x
⊢ a ≤ sInf ∅

pp: case inr
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, a ≤ x
ha : a ≤ 0
hs' : s.Nonempty
⊢ a ≤ sInf s

Tactic:
exacts [ha.trans_eq sInf_empty.symm, le_csInf hs' hs]

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
x : ℝ
hx : 0 ≤ x
⊢ (↑x.toNNReal)⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
rw [← NNReal.coe_inv, Real.toNNReal_coe]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : HeightOneSpectrum R
hx : x ∈ ↑(Finite.toFinset ⋯)
y : HeightOneSpectrum R
hy : y ∈ ↑(Finite.toFinset ⋯)
⊢ x ≠ y → (IsCoprime on fun i ↦ i.maxPowDividing I) x y

Tactic:
hxy

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : HeightOneSpectrum R
hx : x ∈ ↑(Finite.toFinset ⋯)
y : HeightOneSpectrum R
hy : y ∈ ↑(Finite.toFinset ⋯)
hxy : x ≠ y
⊢ (IsCoprime on fun i ↦ i.maxPowDividing I) x y
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q g : GroupSeminorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } = (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
toFun✝¹ : E → ℝ
map_one'✝¹ : toFun✝¹ 1 = 0
mul_le'✝¹ : ∀ (x y : E), toFun✝¹ (x * y) ≤ toFun✝¹ x + toFun✝¹ y
inv'✝¹ : ∀ (x : E), toFun✝¹ x⁻¹ = toFun✝¹ x
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_one' := map_one'✝¹, mul_le' := mul_le'✝¹, inv' := inv'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹, mul_le' := mul_le'✝¹, inv' := inv'✝¹ } =
    { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }