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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
b : Basis ι R S
x : S
hx : x ≠ 0
i : ι
⊢ ↑((basisSpanSingleton b hx) i) = x * b i

Tactic:
simp only [basisSpanSingleton, Basis.map_apply, LinearEquiv.trans_apply,
    Submodule.restrictScalarsEquiv_apply, LinearEquiv.ofInjective_apply, LinearEquiv.coe_ofEq_apply,
    LinearEquiv.restrictScalars_apply, LinearMap.mulLeft_apply]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ P ^ i
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ d, ∃ e ∈ P ^ (i + 1), a * d + e = c

Tactic:
rw [eq_b] at c_mem
    simp only [mul_comm a]
    exact Ideal.mem_span_singleton_sup.mp c_mem

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : ↥S.leftInv
⊢ ↑x * ↑(S.fromLeftInv x) = 1

Tactic:
mul_fromLeftInv

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : ↥S.leftInv
⊢ 1 = 1
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
⊢ ↑y * ↑(S.fromLeftInv y) = 1

Tactic:
mul_fromLeftInv

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
⊢ 1 = 1
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Group M
S : Submonoid M
x : ↥S.leftInv
⊢ ↑x * ↑(S.fromLeftInv x) = 1

Tactic:
mul_fromLeftInv

Goal state after:
M : Type u_1
inst✝ : Group M
S : Submonoid M
x : ↥S.leftInv
⊢ 1 = 1
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case succ.succ.refine_1
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ^ (n + 1) ≤ Module.annihilator R M → P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
⊢ Jac ^ (n + 1) ≤ Module.annihilator R ↥(Jac • ⊤)

Tactic:
rwa [← Submodule.annihilator_top, Submodule.le_annihilator_iff, Jac.pow_succ,
      Submodule.mul_smul, ← Submodule.le_annihilator_iff] at hn

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

Goal state before:
pp: case h₂
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hI : IsUnit ⊤
h : ⊤ ≠ ⊥
⊢ emultiplicity w (map f ⊤) = ↑(v.ramificationIdx' w) * emultiplicity v ⊤

Tactic:
simp_rw [Ideal.map_top, emultiplicity_eq_count_normalizedFactors hw top_ne_bot,
      emultiplicity_eq_count_normalizedFactors hv h, ← Ideal.one_eq_top, normalizedFactors_one]

Goal state after:
case h₂
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hI : IsUnit ⊤
h : ⊤ ≠ ⊥
⊢ ↑(Multiset.count (normalize w) 0) = ↑(v.ramificationIdx' w) * ↑(Multiset.count (normalize v) 0)
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ FormallyUnramified R S ↔ ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (TensorProduct.lmul' R) t = 1

Tactic:
formallyUnramified_iff,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ Subsingleton Ω[S⁄R] ↔ ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (TensorProduct.lmul' R) t = 1
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
⊢ QuasiFinite S T

Tactic:
refine ⟨fun P hP ↦ .of_surjective (Algebra.linearMap P.ResidueField (P.Fiber T)) ?_⟩

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
⊢ Function.Surjective ⇑(Algebra.linearMap P.ResidueField (P.Fiber T))
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
j : I
hj : ∀ (x : I), ¬f x = 0 → (a x) j = 0
⊢ b.repr (f.sum fun i y ↦ (a i) j • y) = 0

Tactic:
simp only [Finsupp.sum]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
j : I
hj : ∀ (x : I), ¬f x = 0 → (a x) j = 0
⊢ b.repr (∑ x ∈ f.support, (a x) j • f x) = 0
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
i : I
⊢ ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i

Tactic:
simp_rw [Finsupp.sum, TensorProduct.smul_tmul', ← TensorProduct.sum_tmul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
i : I
⊢ (∑ a ∈ (b.repr (x * f i)).support, (b.repr (x * f i)) a • b a) ⊗ₜ[R] b i = (x * f i) ⊗ₜ[R] b i
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
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : QuasiFiniteAt R p
f : T ≃ₐ[R] S
⊢ p = Ideal.comap (↑f.symm).toRingHom (Ideal.comap f.toRingEquiv.toRingHom p)

Tactic:
by ext; simp

Goal state after:
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✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H✝ : IsClopen {p}
this✝² : IsNoetherianRing S
this✝¹ : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = ↑(PrimeSpectrum.basicOpen e)
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal := IsLocalization.Away.liftAlgHom e ⋯
h₁ : Set.range (PrimeSpectrum.comap (algebraMap S (Localization.Away e))) = {p}
this✝ : Subsingleton (PrimeSpectrum (Localization.Away e))
x : S
s : ↥p.asIdeal.primeCompl
this : IsUnit ((algebraMap S (Localization.Away e)) ↑s)
⊢ ∃ a, f a = IsLocalization.mk' (Localization.AtPrime p.asIdeal) x s

Tactic:
by
      refine ⟨algebraMap _ _ x * this.unit⁻¹, (this.map f).mul_right_cancel ?_⟩
      simp only [← map_mul, mul_assoc, IsUnit.val_inv_mul]
      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 σ
i : σ
⊢ (Q.comp P).cotangentSpaceBasis.repr
      ((↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
        ((Basis.baseChange T P.cotangentSpaceBasis) i)) =
    (Q.comp P).cotangentSpaceBasis.repr
      ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        ((Basis.baseChange T P.cotangentSpaceBasis) i))

Tactic:
ext j

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 σ
i : σ
j : ι ⊕ σ
⊢ ((Q.comp P).cotangentSpaceBasis.repr
        ((↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
          ((Basis.baseChange T P.cotangentSpaceBasis) i)))
      j =
    ((Q.comp P).cotangentSpaceBasis.repr
        ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
          ((Basis.baseChange T P.cotangentSpaceBasis) i)))
      j
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 σ
i : ι ⊕ σ
⊢ Q.cotangentSpaceBasis.repr
      ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
        ((Q.comp P).cotangentSpaceBasis i)) =
    Q.cotangentSpaceBasis.repr
      ((Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i))

Tactic:
ext j

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 σ
i : ι ⊕ σ
j : ι
⊢ (Q.cotangentSpaceBasis.repr
        ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
          ((Q.comp P).cotangentSpaceBasis i)))
      j =
    (Q.cotangentSpaceBasis.repr
        ((Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i)))
      j
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₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
x : Q'.toExtension.H1Cotangent
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) x) = (δ Q' P') x

Tactic:
by
  let : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
  obtain ⟨x, hx⟩ := x
  obtain ⟨⟨y, hy⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
  change δ _ _ ⟨_, _⟩ = δ _ _ _
  replace hx : (1 : T) ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0 := by
    simpa only [LinearMap.mem_ker, Extension.cotangentComplex_mk, ker, RingHom.mem_ker] using! hx
  simp only [LinearMap.domRestrict_apply, Extension.Cotangent.map_mk, δ_eq_δAux]
  refine (δAux_toAlgHom f _).trans ?_
  rw [hx, map_zero, map_zero, add_zero]

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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact
    ⇑(↑T (Extension.H1Cotangent.map f.toExtensionHom) ∘ₗ
        Extension.H1Cotangent.map ((Q.comp P).defaultHom W).toExtensionHom)
    ⇑(δ Q P)

Tactic:
← Extension.H1Cotangent.map_comp,

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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact ⇑(Extension.H1Cotangent.map (f.toExtensionHom.comp ((Q.comp P).defaultHom W).toExtensionHom)) ⇑(δ Q P)
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Tactic:
let : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ _))

Goal state after:
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : Algebra P.Ring P.infinitesimal.Ring :=
  { smul := map_toInfinitesimal_bijective._aux_1_1 P, algebraMap := map_toInfinitesimal_bijective._aux_1_3 P,
    commutes' := ⋯, smul_def' := ⋯ }
⊢ CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
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 ⊔
      maximalIdeal (Localization.AtPrime p) • ⊤

Tactic:
rw [Ideal.smul_top_eq_map, 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.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)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha : (algebraMap (Localization.AtPrime p) q.ResidueField) a = (algebraMap (Localization.AtPrime q) q.ResidueField) x
⊢ x ∈
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q))

Tactic:
IsScalarTower.algebraMap_apply _ (Localization.AtPrime q),

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)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  (algebraMap (Localization.AtPrime q) q.ResidueField)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) a) =
    (algebraMap (Localization.AtPrime q) q.ResidueField) x
⊢ x ∈
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q))
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case e'_4
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ LinearMap.liftBaseChange T
      (↑S (Extension.H1Cotangent.map (W.defaultHom (Q.comp P)).toExtensionHom) ∘ₗ
        Extension.H1Cotangent.map g.toExtensionHom) =
    LinearMap.liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)

Tactic:
← Extension.H1Cotangent.map_comp,

Goal state after:
case e'_4
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ LinearMap.liftBaseChange T
      (Extension.H1Cotangent.map ((W.defaultHom (Q.comp P)).toExtensionHom.comp g.toExtensionHom)) =
    LinearMap.liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case e'_5
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ ↑T (Extension.H1Cotangent.map f.toExtensionHom) ∘ₗ
      Extension.H1Cotangent.map ((Q.comp P).defaultHom W).toExtensionHom =
    Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom

Tactic:
← Extension.H1Cotangent.map_comp,

Goal state after:
case e'_5
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ Extension.H1Cotangent.map (f.toExtensionHom.comp ((Q.comp P).defaultHom W).toExtensionHom) =
    Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom
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 ⋯
f : (Generators.self R T).toExtension.Hom Q :=
  { toRingHom := (MvPolynomial.aeval Q.σ).toRingHom, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
⊢ (Extension.H1Cotangent.equivOfFormallySmooth (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯)
        (Generators.self R T).toExtension)
      ((Extension.H1Cotangent.map
          {
            toRingHom :=
              algebraMap (Generators.self R S).toExtension.Ring
                (Localization (Submonoid.comap (algebraMap (Generators.self R S).toExtension.Ring S) M)),
            toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
        x) =
    (H1Cotangent.map R R S T) x

Tactic:
← Extension.H1Cotangent.equivOfFormallySmooth_symm,

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
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 ⋯
f : (Generators.self R T).toExtension.Hom Q :=
  { toRingHom := (MvPolynomial.aeval Q.σ).toRingHom, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
⊢ (Extension.H1Cotangent.equivOfFormallySmooth (Generators.self R T).toExtension
          (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯)).symm
      ((Extension.H1Cotangent.map
          {
            toRingHom :=
              algebraMap (Generators.self R S).toExtension.Ring
                (Localization (Submonoid.comap (algebraMap (Generators.self R S).toExtension.Ring S) M)),
            toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
        x) =
    (H1Cotangent.map R R S T) x