mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
⊢ FormallyUnramified R A

Tactic:
replace H : ∀ ⦃B : Type u⦄ [CommRing B] [Small.{w} B],
        ∀ [Algebra R B] (I : Ideal B) (_ : I ^ 2 = ⊥),
          Function.Injective ((Ideal.Quotient.mkₐ R I).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ I) := by
      intro B _ _ _ I hI f g e
      simpa [DFunLike.ext_iff] using H (B := Shrink B) (I.comap (Shrink.ringEquiv _))
        (by rw [← Ideal.map_symm, ← Ideal.map_pow, hI]; simp)
        (a₁ := (Shrink.algEquiv _ _).symm.toAlgHom.comp f)
        (a₂ := (Shrink.algEquiv _ _).symm.toAlgHom.comp g)
        (by simpa [DFunLike.ext_iff, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Shrink.ringEquiv] using e)

Goal state after:
case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
⊢ FormallyUnramified R A
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
this : ∀ (i : ℕ), (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂
x : A
i : ℕ
⊢ (Ideal.Quotient.mk (I ^ i)) (g₁ x - g₂ x) = 0

Tactic:
map_sub,

Goal state after:
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
this : ∀ (i : ℕ), (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂
x : A
i : ℕ
⊢ (Ideal.Quotient.mk (I ^ i)) (g₁ x) - (Ideal.Quotient.mk (I ^ i)) (g₂ x) = 0
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁.comp ((↑e).comp ↑e.symm) = f₂.comp ((↑e).comp ↑e.symm)

Tactic:
← AlgHom.comp_assoc,

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ (f₁.comp ↑e).comp ↑e.symm = f₂.comp ((↑e).comp ↑e.symm)
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case e_φ₁
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ (Ideal.Quotient.mkₐ R I).comp (f₁.comp ↑e) = (Ideal.Quotient.mkₐ R I).comp (f₂.comp ↑e)

Tactic:
← AlgHom.comp_assoc,

Goal state after:
case e_φ₁
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ ((Ideal.Quotient.mkₐ R I).comp f₁).comp ↑e = (Ideal.Quotient.mkₐ R I).comp (f₂.comp ↑e)
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
A : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
B : Type u_3
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ (Ideal.Quotient.mkₐ R I).comp (f₁.comp (IsScalarTower.toAlgHom R A B)) =
    (Ideal.Quotient.mkₐ R I).comp (f₂.comp (IsScalarTower.toAlgHom R A B))

Tactic:
← AlgHom.comp_assoc,

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
A : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
B : Type u_3
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ ((Ideal.Quotient.mkₐ R I).comp f₁).comp (IsScalarTower.toAlgHom R A B) =
    (Ideal.Quotient.mkₐ R I).comp (f₂.comp (IsScalarTower.toAlgHom R A B))
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
H : ∀ (x : PrimeSpectrum R), (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {x}).Finite
P : Ideal R
x✝ : P.IsPrime
this✝ : IsJacobsonRing (P.Fiber S)
this : Finite (PrimeSpectrum (P.Fiber S))
⊢ IsNoetherianRing (P.Fiber S) ∧ Ring.KrullDimLE 0 (P.Fiber S)

Tactic:
exact ⟨Algebra.FiniteType.isNoetherianRing P.ResidueField _,
    (PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero.mp inferInstance).right⟩

Goal state after:
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l✝ : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l✝ ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
H : ∀ (x : P.Ring), (Ideal.Quotient.mk I) ((aeval (σ ∘ ⇑f)) x) = f ((algebraMap P.Ring A) x)
l : P.Ring ⧸ RingHom.ker (algebraMap P.Ring A) ^ 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ (RingHom.ker (algebraMap P.Ring A) ^ 2) (aeval (σ ∘ ⇑f)) ⋯
this : f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift = (Ideal.Quotient.mkₐ R I).comp l
⊢ (Ideal.Quotient.mkₐ R I).comp (l.comp g) = f

Tactic:
← AlgHom.comp_assoc,

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l✝ : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l✝ ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
H : ∀ (x : P.Ring), (Ideal.Quotient.mk I) ((aeval (σ ∘ ⇑f)) x) = f ((algebraMap P.Ring A) x)
l : P.Ring ⧸ RingHom.ker (algebraMap P.Ring A) ^ 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ (RingHom.ker (algebraMap P.Ring A) ^ 2) (aeval (σ ∘ ⇑f)) ⋯
this : f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift = (Ideal.Quotient.mkₐ R I).comp l
⊢ ((Ideal.Quotient.mkₐ R I).comp l).comp g = f
Module: Mathlib.RingTheory.QuasiFinite.Basic

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
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) := e ⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'

Tactic:
have : Algebra.QuasiFiniteAt p.ResidueField qF.asIdeal := .baseChange q _
    congr($(e.symm_apply_apply ⟨⟨q, ‹_›⟩, PrimeSpectrum.ext (q.over_def p).symm⟩).1.1).symm

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
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) := e ⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩
this : QuasiFiniteAt p.ResidueField qF.asIdeal
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type u_1
inst✝³ : CommRing B✝
inst✝² : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u_1
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let __src := (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this).comp ((Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g')) =
    (↑this).comp ((↑this.symm).comp g)
| (↑this).comp ((↑this.symm).comp g)

Tactic:
← AlgHom.comp_assoc,

Goal state after:
R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type u_1
inst✝³ : CommRing B✝
inst✝² : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u_1
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let __src := (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this).comp ((Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g')) =
    (↑this).comp ((↑this.symm).comp g)
| ((↑this).comp ↑this.symm).comp g
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u_4
inst✝⁸ : CommRing R
A : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R A
inst✝ : FormallySmooth R B
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra A C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[A] C ⧸ I
algInst✝ : Algebra R C := ⋯
scalarTowerInst✝ : IsScalarTower R A C := ⋯
g : B →ₐ[R] C
hg : (Ideal.Quotient.mkₐ R I).comp g = AlgHom.restrictScalars R f
⊢ (Ideal.Quotient.mkₐ R I).comp (g.comp (IsScalarTower.toAlgHom R A B)) =
    (Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A C)

Tactic:
← AlgHom.comp_assoc,

Goal state after:
R : Type u_4
inst✝⁸ : CommRing R
A : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R A
inst✝ : FormallySmooth R B
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra A C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[A] C ⧸ I
algInst✝ : Algebra R C := ((algebraMap A C).comp (algebraMap R A)).toAlgebra
scalarTowerInst✝ : IsScalarTower R A C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R C))
g : B →ₐ[R] C
hg : (Ideal.Quotient.mkₐ R I).comp g = AlgHom.restrictScalars R f
⊢ ((Ideal.Quotient.mkₐ R I).comp g).comp (IsScalarTower.toAlgHom R A B) =
    (Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A C)
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 σ
⊢ Function.Exact ⇑(LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
    ⇑(Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom)

Tactic:
← fst_compEquiv,

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 σ
⊢ Function.Exact ⇑(LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
    ⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
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
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
⊢ (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) (1 - f 1) = 0

Tactic:
map_sub,

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
⊢ (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) 1 - (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) (f 1) = 0
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case tmul
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 : T
y : P.toExtension.H1Cotangent
⊢ (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((LinearMap.lTensor T Extension.h1Cotangentι) (x ⊗ₜ[S] y)) ∈
    (Q.comp P).toExtension.cotangentComplex.ker

Tactic:
simp [← Extension.CotangentSpace.map_cotangentComplex]

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hp0 : map (algebraMap R S) p ≠ ⊥
⊢ q.ramificationIdx R = Multiset.count q (normalizedFactors (map (algebraMap R S) p))

Tactic:
by
  rw [← factors_eq_normalizedFactors, ← ramificationIdx_eq_factors_count p q hp0]

Goal state after:
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
x : R
hxs : x ∈ ↑s
⊢ ↑(∏ i ∈ {⟨x, hxs⟩}ᶜ, m i) * 0 = 0

Tactic:
mul_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
x : R
hxs : x ∈ ↑s
⊢ 0 = 0
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
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
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : ¬r.IsPrime
⊢ 0 = q.ramificationIdx R * 0

Tactic:
mul_zero

Goal state after:
case neg
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
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : ¬r.IsPrime
⊢ 0 = 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
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
x : R
w✝ : ↥(Submonoid.powers r')
n : ℕ
hn : (algebraMap R S) (r' ^ n * x) = 0
k : ℕ
hk : ↑(∏ i, m i) ^ k * (r' ^ n * x) = 0
⊢ s ^ k * 0 = 0

Tactic:
mul_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
x : R
w✝ : ↥(Submonoid.powers r')
n : ℕ
hn : (algebraMap R S) (r' ^ n * x) = 0
k : ℕ
hk : ↑(∏ i, m i) ^ k * (r' ^ n * x) = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: case e_6
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✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
x : S
hxs : x ∈ ↑s
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ (algebraMap R S) r'' * (algebraMap R S) r * (algebraMap R S) (∏ i ∈ s.erase x, b i) * (x * (algebraMap R S) (b x)) =
    x * ((algebraMap R S) r * (algebraMap R S) ((∏ x ∈ s.erase x, b x) * b x) * (algebraMap R S) r'')

Tactic:
map_mul

Goal state after:
case e_6
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✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
x : S
hxs : x ∈ ↑s
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ (algebraMap R S) r'' * (algebraMap R S) r * (algebraMap R S) (∏ i ∈ s.erase x, b i) * (x * (algebraMap R S) (b x)) =
    x * ((algebraMap R S) r * ((algebraMap R S) (∏ x ∈ s.erase x, b x) * (algebraMap R S) (b x)) * (algebraMap R S) r'')
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ ⨆ i, f i = 0

Tactic:
dsimp [iSup]

Goal state after:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ sSup (Set.range fun i ↦ f i) = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
⊢ ∃ x, f ≈ const abs x

Tactic:
have ub : ∃ x, ∀ y ∈ s, y ≤ x := (exists_gt f).imp ub'

Goal state after:
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
⊢ ∃ x, f ≈ const abs x
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ¬{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x ↦ ↑x) → a ≤ x}.Nonempty

Tactic:
rw [Set.not_nonempty_iff_eq_empty]

Goal state after:
⊢ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x ↦ ↑x) → a ≤ x} = ∅
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ¬{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x ↦ ↑x) → x ≤ a}.Nonempty

Tactic:
rw [Set.not_nonempty_iff_eq_empty]

Goal state after:
⊢ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x ↦ ↑x) → x ≤ a} = ∅
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ∞
x : ι
⊢ ((fun x ↦ ↑x) ∘ ENNReal.toNNReal ∘ f) x = f x

Tactic:
simp [coe_toNNReal (hf x)]

Goal state after: