mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
I : Ideal S
hI : p ∣ ↑(absNorm I)
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I

Tactic:
by
  have : IsAddTorsionFree S := .of_isTorsionFree ℤ _
  have := CharZero.of_isAddTorsionFree S S
  have hpMax : (Ideal.span {p}).IsMaximal :=
    ((Ideal.span_singleton_prime hp.ne_zero).mpr hp).isMaximal (by simpa using hp.ne_zero)
  induction I using UniqueFactorizationMonoid.induction_on_prime with
  | h₁ =>
    obtain ⟨Q, hQ, e⟩ := Ideal.exists_ideal_over_maximal_of_isIntegral (S := S) (Ideal.span {p})
      (fun x ↦ by simp +contextual)
    exact ⟨Q, hQ, e, dvd_zero _⟩
  | h₂ I hI' =>
    obtain rfl : I = ⊤ := by simpa using hI'
    cases hp.not_dvd_one (by simpa using hI)
  | h₃ I P hI' hP IH =>
    simp only [_root_.map_mul, Nat.cast_mul, hp.dvd_mul] at hI
    cases hI with
    | inr h =>
      obtain ⟨Q, h₁, h₂, h₃⟩ := IH h
      exact ⟨Q, h₁, h₂, dvd_mul_of_dvd_right h₃ _⟩
    | inl hI =>
      have := (Ideal.isPrime_of_prime hP).isMaximal hP.ne_zero
      refine ⟨P, this, (hpMax.eq_of_le (by simpa using this.ne_top) ?_).symm, dvd_mul_right _ _⟩
      obtain ⟨q, n, hn, hqP, hq, H⟩ := Ideal.exists_prime_and_absNorm_eq_pow P
      rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI
      obtain ⟨m, hmn, hp⟩ := hI
      rw [Ideal.span_singleton_le_iff_mem]
      have : m ≠ 0 := fun h ↦ hpMax.ne_top (Ideal.span_singleton_eq_top.mpr (by simpa [h] using hp))
      exact Ideal.mem_of_dvd _ hp.symm.dvd (Ideal.pow_mem_of_mem _ (by simpa) _ this.bot_lt)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ zeroLocus ↑I = zeroLocus ↑⊥

Tactic:
zeroLocus_eq_iff,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ I.radical = ⊥.radical
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ (g • q).inertiaDeg R = q.inertiaDeg R

Tactic:
inertiaDeg_of_not_isPrime,

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ 0 = q.inertiaDeg R

case neg.hq
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ ¬(g • q).IsPrime
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
inst✝³ : Module.Free ℤ R
inst✝² : Module.Finite ℤ R
p : ℤ
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver (span {p})
⊢ p.natAbs ^ P.inertiaDeg ℤ = absNorm P

Tactic:
simpa using absNorm_pow_inertiaDeg (span {p}) P

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map f p ≤ P * P
a : Ideal S
ha : map f p = P * a
ha' : ¬a ≤ P
⊢ map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)

Tactic:
rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, ha, Ideal.map_mul,
    Localization.AtPrime.map_eq_maximalIdeal]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map f p ≤ P * P
a : Ideal S
ha : map f p = P * a
ha' : ¬a ≤ P
⊢ maximalIdeal (Localization P.primeCompl) * map (algebraMap S (Localization.AtPrime P)) a =
    maximalIdeal (Localization.AtPrime P)
Module: Mathlib.RingTheory.QuasiFinite.Basic

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
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
⊢ Function.Surjective ⇑(↑S (Algebra.linearMap P.ResidueField (P.Fiber T)))

Tactic:
← LinearMap.range_eq_top,

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
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
⊢ (↑S (Algebra.linearMap P.ResidueField (P.Fiber T))).range = ⊤
Module: Mathlib.RingTheory.QuasiFinite.Basic

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✝ : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : P.ResidueField ⊗[R] T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
⊢ Function.Surjective ⇑(AlgHom.restrictScalars S f).toLinearMap

Tactic:
← LinearMap.range_eq_top,

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✝ : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : P.ResidueField ⊗[R] T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
⊢ (AlgHom.restrictScalars S f).toLinearMap.range = ⊤
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S ⊗[R] S
a✝¹ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) x✝
a✝ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) y✝
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * (x✝ + y✝)) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ + y✝)

Tactic:
simp only [map_add, smul_add, mul_add, *]

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

Goal state before:
pp: R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
M : Submonoid R
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : IsScalarTower R Rₘ Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ

Tactic:
by
  refine .of_comp_surjective fun Q _ _ I e f ↦ ?_
  let := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
  let : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
  let f : Sₘ →ₐ[Rₘ] Q := by
    refine { FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) with commutes' := ?_ }
    intro r
    change
      (RingHom.comp (FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) : Sₘ →+* Q)
            (algebraMap _ _))
          r =
        algebraMap _ _ r
    congr 1
    refine IsLocalization.ringHom_ext M ?_
    rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
      AlgHom.comp_algebraMap]
  use f
  ext
  simp [f]

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

Goal state before:
pp: case refine_2
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)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
x✝ : { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
l : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent
hl : l ∘ₗ ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁ = LinearMap.id
x : ↥(RingHom.ker (algebraMap P' S))
⊢ ({ toAddHom := ↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂), map_smul' := ⋯ } ∘ₗ kerToTensor R P' S) x = LinearMap.id x

Tactic:
obtain ⟨x, rfl⟩ := e₁.surjective x

Goal state after:
case refine_2
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)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
x✝ : { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
l : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent
hl : l ∘ₗ ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁ = LinearMap.id
x : (RingHom.ker (algebraMap P S)).Cotangent
⊢ ({ toAddHom := ↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂), map_smul' := ⋯ } ∘ₗ kerToTensor R P' S) (e₁ x) = LinearMap.id (e₁ x)
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)
⊢ { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
    { g // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S }

Tactic:
by
  let P' := P ⧸ (RingHom.ker (algebraMap P S) ^ 2)
  have h₁ : Surjective (algebraMap P' S) := Function.Surjective.of_comp (g := algebraMap P P') hf
  have h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥ := by
    rw [RingHom.algebraMap_toAlgebra, AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]
  let e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] (RingHom.ker (algebraMap P' S)) :=
    (Ideal.cotangentEquivIdeal _).trans ((LinearEquiv.ofEq _ _
      (IsScalarTower.toAlgHom R P S).ker_kerSquareLift.symm).restrictScalars P)
  let e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] :=
    (tensorKaehlerQuotKerSqEquiv R P S).restrictScalars P
  have H : kerCotangentToTensor R P S =
      e₂.toLinearMap ∘ₗ (kerToTensor R P' S).restrictScalars P ∘ₗ e₁.toLinearMap := by
    ext x
    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
    exact (tensorKaehlerQuotKerSqEquiv_tmul_D 1 x.1).symm
  refine Equiv.trans ?_ (retractionKerToTensorEquivSection (R := R) h₂ h₁)
  refine ⟨fun ⟨l, hl⟩ ↦ ⟨⟨e₁.toLinearMap ∘ₗ l ∘ₗ e₂.toLinearMap, ?_⟩, ?_⟩,
    fun ⟨l, hl⟩ ↦ ⟨e₁.symm.toLinearMap ∘ₗ l.restrictScalars P ∘ₗ e₂.symm.toLinearMap, ?_⟩, ?_, ?_⟩
  · rintro x y
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    simp only [P', ← Ideal.Quotient.algebraMap_eq, IsScalarTower.algebraMap_smul]
    exact (e₁.toLinearMap ∘ₗ l ∘ₗ e₂.toLinearMap).map_smul x y
  · ext1 x
    rw [H] at hl
    obtain ⟨x, rfl⟩ := e₁.surjective x
    exact DFunLike.congr_arg e₁ (LinearMap.congr_fun hl x)
  · ext x
    rw [H]
    apply e₁.injective
    simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, LinearMap.coe_restrictScalars,
      Function.comp_apply, LinearEquiv.symm_apply_apply, LinearMap.id_coe, id_eq,
      LinearEquiv.apply_symm_apply]
    exact LinearMap.congr_fun hl (e₁ x)
  · intro f
    ext x
    simp only [AlgebraTensorModule.curry_apply, Derivation.coe_comp, LinearMap.coe_comp,
      LinearMap.coe_restrictScalars, Derivation.coeFn_coe, Function.comp_apply, curry_apply,
      LinearEquiv.coe_coe, LinearMap.coe_mk, AddHom.coe_coe,
      LinearEquiv.apply_symm_apply, LinearEquiv.symm_apply_apply]
  · intro f
    ext x
    simp only [AlgebraTensorModule.curry_apply, Derivation.coe_comp, LinearMap.coe_comp,
      LinearMap.coe_restrictScalars, Derivation.coeFn_coe, Function.comp_apply, curry_apply,
      LinearMap.coe_mk, AddHom.coe_coe, LinearEquiv.coe_coe,
      LinearEquiv.symm_apply_apply, LinearEquiv.apply_symm_apply]

Goal state after:
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))
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
y : Q.Ring ⊗[P.Ring] ↥P.ker
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)) y =
    0

Tactic:
induction y with
      | zero => simp only [map_zero, smul_zero]
      | add x y hx hy => simp only [LinearMap.map_add, smul_add, hx, hy, zero_add]
      | tmul c d =>
        simp only [LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, SetLike.val_smul,
          LinearMap.coe_restrictScalars, Function.comp_apply, mk_apply, smul_eq_mul, e,
          LinearMap.liftBaseChange_tmul, LinearEquiv.ofBijective_apply]
        have h₂ : b.1 • Cotangent.mk d = 0 := by ext; simp [Cotangent.smul_eq_zero_of_mem _ b.2]
        rw [TensorProduct.smul_tmul', mul_smul, f.mapKer_apply_coe, ← halg,
          algebraMap_smul, ← TensorProduct.tmul_smul, h₂, tmul_zero, smul_zero]

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
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : S
hx : x ∈ RingHom.ker (algebraMap S (ResidueField S))
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0

Tactic:
replace hx : x ∈ Ideal.map (algebraMap R S) (maximalIdeal R) := by simpa [H] using hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : S
hx : x ∈ Ideal.map (algebraMap R S) (maximalIdeal R)
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
⊢ 0 < q.ramificationIdx R

Tactic:
by
  let p := q.under R
  let Sq := Localization.AtPrime q
  rw [ramificationIdx_def]
  apply ENat.toNat_pos
  · rw [← pos_iff_ne_zero, Module.length_pos_iff, Submodule.Quotient.nontrivial_iff,
      IsScalarTower.algebraMap_eq R S, ← map_map, ← lt_top_iff_ne_top]
    grw [map_mono map_comap_le, Localization.AtPrime.map_eq_maximalIdeal]
    exact (IsLocalRing.maximalIdeal.isMaximal _).lt_top
  · let r := PrimeSpectrum.primesOverOrderIsoFiber R S p (primesOver.mk p q)
    have : q = r.1.comap Algebra.TensorProduct.includeRight := by
      rw [← PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply, OrderIso.symm_apply_apply]
    let := Localization.AtPrime.algebraOfLiesOver p (r.1.comap Algebra.TensorProduct.includeRight)
    have : IsArtinianRing (Sq ⧸ map (algebraMap R Sq) p) := by
      convert (Fiber.localizationAlgEquivQuotient p r.1).toRingEquiv.isArtinianRing
    rwa [Module.length_eq_of_surjective (R := Sq ⧸ p.map (algebraMap R Sq)) Quotient.mk_surjective,
      Module.length_ne_top_iff, ← isArtinianRing_iff_isFiniteLength]

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
hq : p.primesOver S = {q}
inst✝⁴ : Module.Finite R S
inst✝³ : q.LiesOver p
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
this : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Function.Surjective ⇑(Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q))

Tactic:
← LinearMap.range_eq_top,

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✝⁴ : Module.Finite R S
inst✝³ : q.LiesOver p
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
this : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
⊢ (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range = ⊤
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✝⁴ : Module.Finite R S
inst✝³ : q.LiesOver p
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
this : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
⊢ ⊤ ≤
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      Submodule.restrictScalars (Localization.AtPrime p)
        (Ideal.map (algebraMap (Localization.AtPrime p) (Localization.AtPrime q))
          (maximalIdeal (Localization.AtPrime p)))

Tactic:
Algebra.FormallyUnramified.map_maximalIdeal

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✝⁴ : Module.Finite R S
inst✝³ : q.LiesOver p
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
this : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
⊢ ⊤ ≤
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q))
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
x : H1Cotangent R S
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 ⋯
⊢ ∀ (x : (Generators.self R T).toExtension.Ring),
    (algebraMap Q.Ring T) ((MvPolynomial.aeval Q.σ).toRingHom x) =
      (algebraMap T T) ((algebraMap (Generators.self R T).toExtension.Ring T) x)

Tactic:
have : (IsScalarTower.toAlgHom R Q.Ring T).comp (MvPolynomial.aeval Q.σ) =
          IsScalarTower.toAlgHom _ (Generators.self R T).toExtension.Ring _ := by
        ext i
        change _ = algebraMap (Generators.self R T).Ring _ (.X i)
        simp
      exact DFunLike.congr_fun this

Goal state after:
Module: Mathlib.Data.DFinsupp.Encodable

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), Countable (α i)
x✝ : Encodable ι := Encodable.ofCountable ι
⊢ Countable (Π₀ (i : ι), α i)

Tactic:
let _ := fun i ↦ Encodable.ofCountable (α i)

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), Countable (α i)
x✝¹ : Encodable ι := Encodable.ofCountable ι
x✝ : (i : ι) → Encodable (α i) := fun i ↦ Encodable.ofCountable (α i)
⊢ Countable (Π₀ (i : ι), α i)
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 : Set M
⊢ sSup ((fun x ↦ x⁻¹) '' s) = (sInf s)⁻¹

Tactic:
sSup_image

Goal state after:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ ⨆ a ∈ s, a⁻¹ = (sInf s)⁻¹
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ 1 < ↑r ↔ 1 < r

Tactic:
rw [← coe_lt_coe, coe_one]

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

Goal state before:
pp: r : ℝ≥0
⊢ ↑r < 1 ↔ r < 1

Tactic:
rw [← coe_lt_coe, coe_one]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : x < a + ε
⊢ sInf s < a + ε

Tactic:
exact csInf_lt_of_lt h x_in hx

Goal state after: