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
I : Ideal S
hI : Nat.Prime (absNorm I)
⊢ (span {↑(absNorm I)}).IsPrime

Tactic:
Ideal.span_singleton_prime (Int.ofNat_ne_zero.mpr hI.ne_zero),

Goal state after:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
⊢ Prime ↑(absNorm I)
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
I : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S ↥I
inst✝ : AddEquivClass E S ↥I
e : E
⊢ (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I

Tactic:
by
  -- `S ⧸ I` might be infinite if `I = ⊥`, but then `e` can't be an equiv.
  by_cases hI : I = ⊥
  · subst hI
    have : (1 : S) ≠ 0 := one_ne_zero
    have : (1 : S) = 0 := EquivLike.injective e (Subsingleton.elim _ _)
    contradiction
  exact Submodule.natAbs_det_equiv (I.restrictScalars ℤ) e

Goal state after:
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) = ↑x * (↑x)⁻¹

Tactic:
mul_inv_cancel,

Goal state after:
M : Type u_1
inst✝ : Group M
S : Submonoid M
x : ↥S.leftInv
⊢ ↑x * ↑(S.fromLeftInv x) = 1
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommGroup M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ ↑x * ↑((S.leftInvEquiv hS).symm x) = ↑x * (↑x)⁻¹

Tactic:
mul_inv_cancel,

Goal state after:
M : Type u_1
inst✝ : CommGroup M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ ↑x * ↑((S.leftInvEquiv hS).symm x) = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
I : Ideal R
hU : ∃ I_1, (zeroLocus ↑I_1)ᶜ = (zeroLocus ↑I)ᶜ
J : Ideal R
hZ : ∃ I, zeroLocus ↑J = zeroLocus ↑I
hS : ((zeroLocus ↑I)ᶜ ∩ zeroLocus ↑J).Nonempty
⊢ ((zeroLocus ↑I)ᶜ ∩ zeroLocus ↑J ∩ closedPoints (PrimeSpectrum R)).Nonempty

Tactic:
simp only [Set.nonempty_iff_ne_empty, ne_eq, Set.inter_assoc,
    ← Set.disjoint_iff_inter_eq_empty, Set.disjoint_compl_left_iff_subset,
    zeroLocus_subset_zeroLocus_iff, Ideal.radical_eq_jacobson, Ideal.jacobson, le_sInf_iff] at hS ⊢

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
I : Ideal R
hU : ∃ I_1, (zeroLocus ↑I_1)ᶜ = (zeroLocus ↑I)ᶜ
J : Ideal R
hZ : ∃ I, zeroLocus ↑J = zeroLocus ↑I
hS : ¬∀ b ∈ {J_1 | J ≤ J_1 ∧ J_1.IsMaximal}, I ≤ b
⊢ ¬zeroLocus ↑J ∩ closedPoints (PrimeSpectrum R) ⊆ zeroLocus ↑I
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_2
M✝ : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M✝
inst✝¹ : Module R M✝
inst✝ : IsSemiprimaryRing R
M : Type u
x✝³ : AddCommGroup M
x✝² x✝¹ : Module R M
x✝ : IsScalarTower R R M
h : IsNoetherian R ↥(Ring.jacobson R • ⊤) ↔ IsArtinian R ↥(Ring.jacobson R • ⊤)
h' : IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)
N : Submodule R M := Ring.jacobson R • ⊤
⊢ IsNoetherian R ↥N ∧ IsNoetherian R (M ⧸ N) ↔ IsArtinian R ↥N ∧ IsArtinian R (M ⧸ N)

Tactic:
N,

Goal state after:
R : Type u_2
M✝ : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M✝
inst✝¹ : Module R M✝
inst✝ : IsSemiprimaryRing R
M : Type u
x✝³ : AddCommGroup M
x✝² x✝¹ : Module R M
x✝ : IsScalarTower R R M
h : IsNoetherian R ↥(Ring.jacobson R • ⊤) ↔ IsArtinian R ↥(Ring.jacobson R • ⊤)
h' : IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)
N : Submodule R M := Ring.jacobson R • ⊤
⊢ IsNoetherian R ↥(Ring.jacobson R • ⊤) ∧ IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔
    IsArtinian R ↥(Ring.jacobson R • ⊤) ∧ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)
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
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ Nat.Prime (absNorm (span {x}))

Tactic:
rwa [Ideal.absNorm_span_singleton, ← Int.prime_iff_natAbs_prime]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
p q : Submodule A M
h : p ⋖ q
f : ↥p →ₗ[A] ↥q := inclusion ⋯
key : IsSimpleModule A (↥q ⧸ f.range)
hm : (maximalIdeal A).IsMaximal
e : (↥q ⧸ f.range) ≃ₗ[A] A ⧸ maximalIdeal A
g : ↥q →ₗ[A] A ⧸ maximalIdeal A := ↑e ∘ₗ f.range.mkQ
this✝² : Function.Injective ⇑f
this✝¹ : Function.Surjective ⇑g
this✝ : Function.Exact ⇑f ⇑g
this : FaithfullyFlat A B
⊢ length B (B ⊗[A] ↥q) = length B (B ⊗[A] ↥p) + length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
rw [length_eq_add_of_exact (lTensor B B f) (lTensor B B g) (by simpa) (by simpa) (by simpa),
    (Algebra.TensorProduct.quotIdealMapEquivTensorQuot B (maximalIdeal A)).toLinearEquiv.length_eq]

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
inst✝ : QuasiFinite R S
⊢ Module.Finite R S

Tactic:
by
  classical
  let e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
    .ofBijective (IsScalarTower.toAlgHom _ _ _)
      (PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective.mp inferInstance)
  have : Fintype (PrimeSpectrum R) := .ofFinite _
  let e' : S ≃ₐ[R] Π p : PrimeSpectrum R, Localization p.asIdeal.primeCompl ⊗[R] S :=
    (Algebra.TensorProduct.rid R R S).symm.trans <| (Algebra.TensorProduct.congr .refl e).trans <|
      (Algebra.TensorProduct.piRight _ _ _ _).trans <| AlgEquiv.piCongrRight
      fun _ ↦ Algebra.TensorProduct.comm _ _ _
  have (p : PrimeSpectrum R) : Module.Finite R (Localization p.asIdeal.primeCompl ⊗[R] S) :=
    have : Module.Finite R (Localization.AtPrime p.asIdeal) :=
      .of_surjective (Algebra.linearMap _ _)
        (IsArtinianRing.localization_surjective p.asIdeal.primeCompl _)
    have : Module.Finite (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] S) := finite_of_isArtinianRing_of_isLocalRing
    .trans (Localization.AtPrime p.asIdeal) _
  exact .of_surjective e'.symm.toLinearMap e'.symm.surjective

Goal state after:
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
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ x_1 ∈ f.support,
      ∑ x_2 ∈ f.support.biUnion fun i ↦ (b.repr (b i * x)).support, ((b.repr (b x_1 * x)) x_2 • f x_1) ⊗ₜ[R] b x_2

Tactic:
apply Finset.sum_congr rfl

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := ⋯
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
⊢ ∀ x_1 ∈ f.support,
    ∑ x ∈ (a x_1).support, ((a x_1) x • f x_1) ⊗ₜ[R] b x =
      ∑ x_2 ∈ f.support.biUnion fun i ↦ (b.repr (b i * x)).support, ((b.repr (b x_1 * x)) x_2 • f x_1) ⊗ₜ[R] b x_2
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
⊢ Ideal.under R (Ideal.under S (IsLocalRing.maximalIdeal (Localization.AtPrime Q))) = Ideal.under R Q

Tactic:
rw [Localization.AtPrime.under_maximalIdeal]

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

Goal state before:
pp: case h2.refine_2
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.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Extension.Cotangent.map (Q.toComp P).toExtensionHom) (Extension.Cotangent.mk ⟨w, hw⟩) =
    Extension.Cotangent.mk ⟨(Q.toComp P).toAlgHom w, ⋯⟩

Tactic:
· rw [map_mk]
      rfl

Goal state after:
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✝¹ : FormallySmooth R A
inst✝ : FormallySmooth A B
C : Type (max u_4 u_6)
x✝¹ : CommRing C
x✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
obtain ⟨f', e⟩ := FormallySmooth.comp_surjective _ _ I hI (f.comp (IsScalarTower.toAlgHom R A B))

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✝¹ : FormallySmooth R A
inst✝ : FormallySmooth A B
C : Type (max u_4 u_6)
x✝¹ : CommRing C
x✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f' = f.comp (IsScalarTower.toAlgHom R A B)
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case hz.fst
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
⊢ 0 = Q.toExtension.cotangentComplex ((Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y)

Tactic:
hy,

Goal state after:
case hz.fst
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
⊢ 0 = Q.toExtension.cotangentComplex (Extension.Cotangent.mk x)
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)
⊢ ¬minpoly K ((algebraMap A Q.ResidueField) x) ^ 2 ∣ p

Tactic:
have : IsField (Localization.AtPrime Q) :=
    have := IsArtinianRing.of_finite K (Localization.AtPrime Q)
    have := Algebra.FormallyUnramified.isReduced_of_field K (Localization.AtPrime Q)
    IsArtinianRing.isField_of_isReduced_of_isLocalRing _

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)
⊢ ¬minpoly K ((algebraMap A Q.ResidueField) x) ^ 2 ∣ 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
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' := ⋯ }
this : IsScalarTower P.Ring P.infinitesimal.Ring S
⊢ CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Tactic:
apply LinearMap.restrictScalars_injective 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 := ⋯
this : IsScalarTower P.Ring P.infinitesimal.Ring S
⊢ ↑P.Ring (CotangentSpace.map P.toInfinitesimal) = ↑P.Ring ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
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)
this :
  LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex =
    Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f)
⊢ (tensorCotangentSpaceOfFormallyEtale f H₁)
      ((LinearMap.baseChange T P.cotangentComplex) ((tensorCotangent f halg H₂).symm ↑x)) =
    Q.cotangentComplex ↑x

Tactic:
exact (DFunLike.congr_fun this _).trans (DFunLike.congr_arg Q.cotangentComplex
        ((tensorCotangent f halg H₂).apply_symm_apply x.1))

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
⊢ ∑ i,
      (↑((primesOverOrderIsoFiber R S p).symm.toEquiv i)).ramificationIdx R *
        (↑((primesOverOrderIsoFiber R S p).symm.toEquiv i)).inertiaDeg R =
    ∑ p_1, finrank p.ResidueField (Localization.AtPrime p_1.asIdeal)

Tactic:
apply Finset.sum_congr rfl

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this : Fintype (PrimeSpectrum (p.Fiber S)) := ⋯
⊢ ∀ x ∈ Finset.univ,
    (↑((primesOverOrderIsoFiber R S p).symm.toEquiv x)).ramificationIdx R *
        (↑((primesOverOrderIsoFiber R S p).symm.toEquiv x)).inertiaDeg R =
      finrank p.ResidueField (Localization.AtPrime x.asIdeal)
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.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 =
    (Extension.H1Cotangent.map f) ((H1Cotangent.map R R S T) x)

Tactic:
Algebra.H1Cotangent.map,

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.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 =
    (Extension.H1Cotangent.map f)
      ((Extension.H1Cotangent.map ((Generators.self R S).defaultHom (Generators.self R T)).toExtensionHom) 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
M : Submonoid S
inst✝ : IsLocalization M T
⊢ Function.Bijective ⇑(LinearMap.liftBaseChange T (map R R S T))

Tactic:
← tensorH1CotangentOfIsLocalization_toLinearMap R T M

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
⊢ Function.Bijective ⇑↑(tensorH1CotangentOfIsLocalization R T M)
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha✝ : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
ha : a ∉ S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

Tactic:
exact prod_eq_zero hi <| by simp [*, -coe_biUnion]

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

Goal state before:
pp: s : Set ℝ
⊢ sInf (-s) = -sSup s

Tactic:
← neg_eq_iff_eq_neg,

Goal state after:
s : Set ℝ
⊢ -sInf (-s) = sSup s
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a ≤ y

Tactic:
have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]

Goal state after:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this : a * x⁻¹ < 1
⊢ a ≤ y
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: α : Type u_1
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
⊢ ↑a ≤ ↑a + ↑(-a)

Tactic:
exact le_self_add

Goal state after:
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑a + ↑(c - a) < b

Tactic:
← coe_add,

Goal state after:
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑(a + (c - a)) < b
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p + q).toNNReal = ↑p.toNNReal + ↑q.toNNReal

Tactic:
← coe_add,

Goal state after:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p + q).toNNReal = ↑(p.toNNReal + q.toNNReal)
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ≥0∞
⊢ (∞ * a).toReal = 0

Tactic:
rw [mul_comm]

Goal state after:
a : ℝ≥0∞
⊢ (a * ∞).toReal = 0
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case inr.inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x
⊢ y ∈ [[a, b]]

Tactic:
uIcc_of_le hab,

Goal state after:
case inr.inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x
⊢ y ∈ Icc a b
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ a - x✝ - (a - b) = b - x✝

Tactic:
tsub_tsub_tsub_cancel_left

Goal state after:
case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ b - x✝ = b - x✝

case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ b ≤ a
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : 0 < x
h'x : x ≠ ⊤
⊢ 0 < x.toReal

Tactic:
lift x to ℝ using by aesop

Goal state after:
x : ℝ
hx : 0 < ↑x
h'x : ↑x ≠ ⊤
⊢ 0 < (↑x).toReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : x < 0
h'x : x ≠ ⊥
⊢ x.toReal < 0

Tactic:
lift x to ℝ using by aesop

Goal state after:
x : ℝ
hx : ↑x < 0
h'x : ↑x ≠ ⊥
⊢ (↑x).toReal < 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ WithBot.some '' WithTop.some '' Iio x = Ioo ⊥ ↑x

Tactic:
rw [WithTop.image_coe_Iio, WithBot.image_coe_Iio]

Goal state after:
x : ℝ
⊢ Ioo ⊥ ↑↑x = Ioo ⊥ ↑x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ (if ↑x = ⊤ then ∞ else ENNReal.ofReal (↑x).toReal) = x

Tactic:
if_neg _,

Goal state after:
case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ ENNReal.ofReal (↑x).toReal = x

x : ℝ≥0∞
h_top : ¬x = ∞
⊢ ¬↑x = ⊤
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.ofNat n) = ↑r ^ Int.ofNat n

pp: case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n

Tactic:
· simp only [Int.ofNat_eq_natCast, coe_pow, zpow_natCast]

Goal state after:
case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n