mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
h1 : X.degree < (X ^ p).degree
⊢ (X ^ p).natDegree = p

Tactic:
natDegree_X_pow

Goal state after:
K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
h1 : X.degree < (X ^ p).degree
⊢ p = p
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
hn : (frobenius K p ^ n) x = x ^ p ^ n
⊢ ((frobenius K p).comp (frobenius K p ^ n)) x = (x ^ p ^ n) ^ p

Tactic:
RingHom.comp_apply,

Goal state after:
case succ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
hn : (frobenius K p ^ n) x = x ^ p ^ n
⊢ (frobenius K p) ((frobenius K p ^ n) x) = (x ^ p ^ n) ^ p
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p - 1) = 1

Tactic:
by
  have h := FiniteField.pow_card_sub_one_eq_one a ha
  rwa [ZMod.card p] at h

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
⊢ Nat.card ↥(castHom ⋯ F).fieldRange = p

Tactic:
← Nat.card_eq_of_bijective _ (RingHom.rangeRestrictField_bijective _),

Goal state after:
F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
⊢ Nat.card (ZMod p) = p
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : MulSemiringAction G B
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hAB : Algebra.IsInvariant A B G
inst✝¹ : SMulCommClass G A B
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
this✝ : Nontrivial A
this : Nontrivial B
x y : B
hy : y ∈ nonZeroDivisors B
h : ∀ (g : G), g • ((algebraMap B L) x / (algebraMap B L) y) = (algebraMap B L) x / (algebraMap B L) y
hy' : (algebraMap B L) y ≠ 0
b : B
a : A
hb : x * (algebraMap A B) a = b * y
ha : (algebraMap B L) ((algebraMap A B) a) ≠ 0
hxy : (algebraMap B L) x / (algebraMap B L) y = (algebraMap B L) b / (algebraMap B L) ((algebraMap A B) a)
⊢ ∀ (g : G), g • b = b

Tactic:
by simpa [ha, hxy, smul_div₀', ← algebraMap.coe_smul'] using h

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
x : α
u : αˣ
hx : P x
⊢ P (x * ↑u)

Tactic:
exact hcp (fun p _ hpx => isUnit_of_dvd_unit hpx u.isUnit) hx (h1 u.isUnit)

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := ⋯
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := ⋯
p : α
hpa : p ∈ normalizedFactors a
⊢ p ∈ normalizedFactors ?neg.refine_1.inl.a✝

Tactic:
assumption

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := ⋯
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := ⋯
p : α
hpb : p ∈ normalizedFactors b
⊢ p ∈ normalizedFactors ?neg.refine_1.inr.a✝

Tactic:
assumption

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

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

Tactic:
Submonoid.coe_mul,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
⊢ ↑y * ↑x * ↑(S.fromLeftInv x * S.fromLeftInv y) = 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 * ↑x * ↑(S.fromLeftInv x * S.fromLeftInv y) = 1

Tactic:
Submonoid.coe_mul,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
⊢ ↑y * ↑x * (↑(S.fromLeftInv x) * ↑(S.fromLeftInv y)) = 1
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
⊢ x ∈ invSubmonoid M S ↔ ∃ m, mk' S 1 m = x

Tactic:
simp_rw [← toInvSubmonoid_eq_mk']
  exact ⟨fun h => ⟨_, congr_arg Subtype.val (toInvSubmonoid_surjective M S ⟨x, h⟩).choose_spec⟩,
    fun h => h.choose_spec ▸ (toInvSubmonoid M S h.choose).prop⟩

Goal state after:
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
inst✝ : CharZero S
n : ℕ
⊢ {I | absNorm ↑I ≤ n}.Finite

Tactic:
have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOfPred_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
this : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ {I | absNorm ↑I ≤ n}.Finite
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
n : ℕ
inst✝ : CharZero S
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { I // absNorm ↑I ≤ n } + 1

Tactic:
have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOfPred_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { I // absNorm ↑I ≤ n } + 1
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case refine_1
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ P ^ Multiset.count P (normalizedFactors (map f p)) ∣ map f p

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors (pow_ne_zero _ hP0) hp0,
      normalizedFactors_pow, normalizedFactors_irreducible hPirr, normalize_eq,
      Multiset.nsmul_singleton, ← Multiset.le_count_iff_replicate_le]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ¬P ^ (Multiset.count P (normalizedFactors (map f p)) + 1) ∣ map f p

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors (pow_ne_zero _ hP0) hp0,
      normalizedFactors_pow, normalizedFactors_irreducible hPirr, normalize_eq,
      Multiset.nsmul_singleton, ← Multiset.le_count_iff_replicate_le]

Goal state after:
case refine_2
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ¬Multiset.count P (normalizedFactors (map f p)) + 1 ≤ Multiset.count P (normalizedFactors (map f p))
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
ha : a = fun i ↦ b.repr (b i * x)
⊢ (1 ⊗ₜ[R] x * f.sum fun i y ↦ y ⊗ₜ[R] b i) =
    ∑ k ∈ f.support.biUnion fun i ↦ (a i).support,
      (b.repr (f.sum fun i y ↦ (a i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k

Tactic:
rw [Finsupp.sum, Finset.mul_sum]

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
ha : a = fun i ↦ b.repr (b i * x)
⊢ ∑ i ∈ f.support, 1 ⊗ₜ[R] x * f i ⊗ₜ[R] b i =
    ∑ k ∈ f.support.biUnion fun i ↦ (a i).support,
      (b.repr (f.sum fun i y ↦ (a i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k
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
p : P.ResidueField
s : S
t : ↥M
ht : ¬(algebraMap S P.ResidueField) ↑t = 0
⊢ (s • p) ⊗ₜ[S] 1 = (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t)) (p ⊗ₜ[S] IsLocalization.mk' T s t)

Tactic:
dsimp; simp [Algebra.algebraMap_eq_smul_one, smul_tmul]

Goal state after:
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 R
inst✝⁵ : p.IsPrime
P : Ideal S
inst✝⁴ : P.IsPrime
inst✝³ : P.LiesOver p
inst✝² : QuasiFiniteAt R P
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime P)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p P
m : Ideal (Localization.AtPrime P) := IsLocalRing.maximalIdeal (Localization.AtPrime P)
this✝¹ : m.LiesOver p := Ideal.LiesOver.trans m P p
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime m) := Localization.AtPrime.algebraOfLiesOver p m
this : Algebra (Localization.AtPrime P) (Localization.AtPrime m) := Localization.AtPrime.algebraOfLiesOver P m
⊢ Module.Finite p.ResidueField P.ResidueField

Tactic:
let e := AlgEquiv.ofBijective (IsScalarTower.toAlgHom p.ResidueField P.ResidueField
    m.ResidueField) ((RingHom.surjectiveOnStalks_of_isLocalization
        P.primeCompl _).residueFieldMap_bijective P m (m.over_def P))

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : IsScalarTower R S T
p : Ideal R
inst✝⁵ : p.IsPrime
P : Ideal S
inst✝⁴ : P.IsPrime
inst✝³ : P.LiesOver p
inst✝² : QuasiFiniteAt R P
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime P)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p P
m : Ideal (Localization.AtPrime P) := IsLocalRing.maximalIdeal (Localization.AtPrime P)
this✝¹ : m.LiesOver p := Ideal.LiesOver.trans m P p
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime m) := Localization.AtPrime.algebraOfLiesOver p m
this : Algebra (Localization.AtPrime P) (Localization.AtPrime m) := Localization.AtPrime.algebraOfLiesOver P m
e : P.ResidueField ≃ₐ[p.ResidueField] m.ResidueField :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom p.ResidueField P.ResidueField m.ResidueField) ⋯
⊢ Module.Finite p.ResidueField P.ResidueField
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))
hf : Function.Surjective ⇑f
⊢ QuasiFiniteAt R p.asIdeal

Tactic:
have : Algebra.FiniteType R (Localization.AtPrime p.asIdeal) :=
    .of_surjective (f.restrictScalars R) hf

Goal state after:
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))
hf : Function.Surjective ⇑f
this : FiniteType R (Localization.AtPrime p.asIdeal)
⊢ QuasiFiniteAt R p.asIdeal
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
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
⊢ FormallySmooth R A

Tactic:
rw [iff_split_surjection f P.algebraMap_surjective]

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
⊢ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A
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.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
    ⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))

Tactic:
exact Function.Exact.inr_fst

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))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
⊢ (↑((primesOverOrderIsoFiber R S p).symm.toEquiv q)).ramificationIdx R *
      (↑((primesOverOrderIsoFiber R S p).symm.toEquiv q)).inertiaDeg R =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)

Tactic:
simp_rw [toEquiv_symm, coe_symm_toEquiv, coe_primesOverOrderIsoFiber_symm_apply]

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)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
⊢ (comap Algebra.TensorProduct.includeRight q.asIdeal).ramificationIdx R *
      (comap Algebra.TensorProduct.includeRight q.asIdeal).inertiaDeg R =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)
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
⊢ ↑(m ⟨x, hxs⟩ * ∏ i ∈ {⟨x, hxs⟩}ᶜ, m i) * x = 0

Tactic:
Submonoid.coe_mul,

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
⊢ ↑(m ⟨x, hxs⟩) * ↑(∏ i ∈ {⟨x, hxs⟩}ᶜ, m i) * x = 0
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
⊢ ?m.101 =
    map (algebraMap (Localization.AtPrime q) (Localization.AtPrime r))
      (map (algebraMap R (Localization.AtPrime q)) (under R r))

Tactic:
by rw [map_map, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: case pos
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
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
let e : (Sq ⧸ p.map (algebraMap R Sq)) ≃ₐ[Sq] Sq' ⧸ p.map (algebraMap R Sq') :=
      Ideal.quotientEquivAlg _ _ (AlgEquiv.ofBijective (Algebra.ofId Sq Sq') f.bijective)
        (by rw [IsScalarTower.algebraMap_eq R Sq Sq', Ideal.map_map,
          ← AlgEquiv.toAlgHom_toRingHom, AlgEquiv.toAlgHom_ofBijective, Algebra.toRingHom_ofId])

Goal state after:
case pos
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
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
e : (Sq ⧸ map (algebraMap R Sq) p) ≃ₐ[Sq] Sq' ⧸ map (algebraMap R Sq') p :=
  (map (algebraMap R Sq) p).quotientEquivAlg (map (algebraMap R Sq') p) (AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯) ⋯
⊢ (g • q).ramificationIdx R = q.ramificationIdx R
Module: Mathlib.LinearAlgebra.Countable

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Countable R
inst✝ : Module.Finite R M
⊢ Countable M

Tactic:
obtain ⟨n, s, h⟩ := Module.Finite.exists_fin (R := R) (M := M)
  rw [← Set.countable_univ_iff]
  have : Countable (Submodule.span R (Set.range s)) := inferInstance
  rwa [h] at this

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mpr
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h✝ : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
x : A
h : ∀ i ∈ S, x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
⊢ x ∈ i.maxPowDividing (span {a})

Tactic:
by_cases htop : i.maxPowDividing (span {a}) = ⊤

Goal state after:
case pos
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h✝ : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
x : A
h : ∀ i ∈ S, x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
htop : i.maxPowDividing (span {a}) = ⊤
⊢ x ∈ i.maxPowDividing (span {a})

case neg
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h✝ : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
x : A
h : ∀ i ∈ S, x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
htop : ¬i.maxPowDividing (span {a}) = ⊤
⊢ x ∈ i.maxPowDividing (span {a})
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
⊢ ↑(sInf ∅) = sInf (toReal '' ∅)

pp: case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sInf s) = sInf (toReal '' s)

Tactic:
· simp only [Set.image_empty, Real.sInf_empty, coe_eq_zero]
    exact @subset_sInf_emptyset ℝ (Set.Ici (0 : ℝ)) _ _ (_)

Goal state after:
case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sInf s) = sInf (toReal '' s)
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ ↑(sInf ∅) = 0

Tactic:
coe_sInf,

Goal state after:
⊢ sInf (toReal '' ∅) = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ ↑(sInf (Set.range fun i ↦ s i)) = sInf (Set.range fun i ↦ ↑(s i))

Tactic:
coe_sInf,

Goal state after:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sInf (toReal '' Set.range fun i ↦ s i) = sInf (Set.range fun i ↦ ↑(s i))
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2.refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ BddBelow (range fun q ↦ f ↑↑q)

Tactic:
refine ⟨hf.some, fun z => ?_⟩
      rintro ⟨u, rfl⟩
      suffices hfu : f u ∈ f '' Ioi x from hf.choose_spec hfu
      exact ⟨u, u.prop, rfl⟩

Goal state after: