mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
hR : IsIntegrallyClosed R
p : R[X]
⊢ p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))

Tactic:
hp

Goal state after:
case mp
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
hR : IsIntegrallyClosed R
p : R[X]
hp : p.Monic
⊢ Irreducible p ↔ Irreducible (map (algebraMap R K) p)
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq✝ : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this✝ : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : Gal(K/k)
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
y : K
hy : y ∈ ↑L'.toIntermediateField
this : h ↑⟨y, hy⟩ = σ ↑⟨y, hy⟩
⊢ σ⁻¹ (h y) = y

Tactic:
simp only [this, ← AlgEquiv.mul_apply, inv_mul_cancel, one_apply]

Goal state after:
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
sub : (fun g ↦ g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this✝ : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
this : L ≤ L'.toIntermediateField
x✝ : Algebra ↥L ↥L'.toIntermediateField := (↑(inclusion this)).toAlgebra
⊢ FiniteDimensional k ↥L

Tactic:
exact FiniteDimensional.left k L L'.1

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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
heq : (fun f ↦ f.comp (algebraMap F E)) f = (fun f ↦ f.comp (algebraMap F E)) g
x : E
⊢ f x = g x

Tactic:
let q := ringExpChar F

Goal state after:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
heq : (fun f ↦ f.comp (algebraMap F E)) f = (fun f ↦ f.comp (algebraMap F E)) g
x : E
q : ℕ := ringExpChar F
⊢ f x = g x
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this✝¹ : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra
this✝ : SMul ↥(separableClosure F E) ↥L := this✝¹.toSMul
this : IsScalarTower (↥(separableClosure F E)) (↥L) E
⊢ IsPurelyInseparable (↥L) E

Tactic:
exact IsPurelyInseparable.tower_top (separableClosure F E) L E

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

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
⊢ separableClosure F E ≤ L ↔ IsPurelyInseparable (↥L) E

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ separableClosure_le F E L⟩
  let := (inclusion h).toAlgebra
  let : SMul (separableClosure F E) L := Algebra.toSMul
  have : IsScalarTower (separableClosure F E) L E := IsScalarTower.of_algebraMap_eq (congrFun rfl)
  exact IsPurelyInseparable.tower_top (separableClosure F E) L E

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

Goal state before:
pp: k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
x : R ⊗[k] K
⊢ ∃ n > 0, x ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
let q := ringExpChar k

Goal state after:
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
⊢ ∃ n > 0, x ^ n ∈ (algebraMap R (R ⊗[k] K)).range
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K L) x = finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)

Tactic:
← trace_trace (S := K⟮x⟯)

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K ↥K⟮x⟯) ((Algebra.trace (↥K⟮x⟯) L) x) =
    finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : a.val ≤ n / 2
⊢ ↑(↑a.val).natAbs = a

Tactic:
rw [Int.natAbs_natCast, natCast_zmod_val]

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

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β : κ
⊢ ∑ a, ∑ i, ((traceForm A B) (b a * P.map (⇑(algebraMap A B)) a α)) (b i * P.map (⇑(algebraMap A B)) i β) =
    ∑ j, (Pᵀ * traceMatrix A b) α j * P j β

Tactic:
sum_comm

Goal state after:
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β : κ
⊢ ∑ y, ∑ x, ((traceForm A B) (b x * P.map (⇑(algebraMap A B)) x α)) (b y * P.map (⇑(algebraMap A B)) y β) =
    ∑ j, (Pᵀ * traceMatrix A b) α j * P j β
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this✝ : DecidableEq R := Classical.decEq R
this : ∃ a, (∃ a_1 ∈ univ, eval a_1 f = a) ∧ ∃ a_1 ∈ univ, eval a_1 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0

Tactic:
rcases this with ⟨x, ⟨a, _, ha⟩, ⟨b, _, hb⟩⟩

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
x a : R
left✝¹ : a ∈ univ
ha : eval a f = x
b : R
left✝ : b ∈ univ
hb : eval b (-g) = x
⊢ ∃ a b, eval a f + eval b g = 0
Module: Mathlib.LinearAlgebra.FreeModule.Determinant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
this : Nonempty (Module.Free.ChooseBasisIndex R M) := Module.Basis.index_nonempty (Module.Free.chooseBasis R M)
a✝ : Nontrivial R
⊢ LinearMap.det 0 = 0

Tactic:
exact LinearMap.det_zero' (Module.Free.chooseBasis R M)

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]

Tactic:
rcases ZMod.sq_add_sq p x with ⟨a, b, hx⟩

Goal state after:
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ.succ
p a d k : ℕ
hk : k ∈ range p
n✝ : ℕ
hd : (1 + p * a) ^ p ^ (n✝ + 1) = p ^ (n✝ + 1) * d + 1
⊢ p ∣ (p ^ (n✝ + 1) * d) ^ k * ↑(p.choose (k + 1))

Tactic:
cases k <;> simp [mul_assoc, pow_succ']

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

Goal state before:
pp: case intro
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P✝ : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P✝
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P✝) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P✝) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P✝] k
f : B ⧸ Q →ₐ[A ⧸ P✝] k := IsScalarTower.toAlgHom (A ⧸ P✝) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P✝) k).comp (algebraMap A (A ⧸ P✝))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P✝) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this✝² : IsScalarTower A (B ⧸ Q) k
this✝¹ : IsScalarTower A B k
P : Polynomial A
hp : (Polynomial.mapRingHom (algebraMap A B)) P = MulSemiringAction.charpoly G x
this✝ : (Polynomial.aeval x) P = 0
this : (Polynomial.aeval (σ ((algebraMap (B ⧸ Q) k) ((mk Q) x)))) ((Polynomial.mapRingHom (algebraMap A B)) P) = 0
⊢ (σ.comp f).toRingHom ((mk Q) x) ∈ f.range

Tactic:
hp

Goal state after:
case intro
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P✝ : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P✝
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P✝) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P✝) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P✝] k
f : B ⧸ Q →ₐ[A ⧸ P✝] k := IsScalarTower.toAlgHom (A ⧸ P✝) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P✝) k).comp (algebraMap A (A ⧸ P✝))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P✝) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this✝² : IsScalarTower A (B ⧸ Q) k
this✝¹ : IsScalarTower A B k
P : Polynomial A
hp : (Polynomial.mapRingHom (algebraMap A B)) P = MulSemiringAction.charpoly G x
this✝ : (Polynomial.aeval x) P = 0
this : (Polynomial.aeval (σ ((algebraMap (B ⧸ Q) k) ((mk Q) x)))) (MulSemiringAction.charpoly G x) = 0
⊢ (σ.comp f).toRingHom ((mk Q) x) ∈ f.range
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank ℤ ↥N = finrank ℤ M
⊢ Finite (M ⧸ N)

Tactic:
by
  let b := Module.Free.chooseBasis ℤ M
  let a := smithNormalFormCoeffs b h
  let e := N.quotientEquivPiZMod b h
  have : ∀ i, NeZero (a i).natAbs := fun i ↦
    ⟨Int.natAbs_ne_zero.mpr (smithNormalFormCoeffs_ne_zero b h i)⟩
  exact Finite.of_equiv (Π i, ZMod (a i).natAbs) e.symm

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

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k ≃ₐ[A ⧸ P] k
f : B ⧸ Q →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective ⇑f
τ₁ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₁ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₁ x) = σ ((algebraMap (B ⧸ Q) k) x)
τ₂ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₂ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₂ x) = σ.symm ((algebraMap (B ⧸ Q) k) x)
x y : B
e : (mk Q) y = τ₂ ((mk Q) x)
⊢ (algebraMap (B ⧸ Q) k) (τ₁ ((mk Q) y)) = σ ((algebraMap (B ⧸ Q) k) ((mk Q) y))

Tactic:
h₁

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k ≃ₐ[A ⧸ P] k
f : B ⧸ Q →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective ⇑f
τ₁ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₁ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₁ x) = σ ((algebraMap (B ⧸ Q) k) x)
τ₂ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₂ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₂ x) = σ.symm ((algebraMap (B ⧸ Q) k) x)
x y : B
e : (mk Q) y = τ₂ ((mk Q) x)
⊢ σ ((algebraMap (B ⧸ Q) k) ((mk Q) y)) = σ ((algebraMap (B ⧸ Q) k) ((mk Q) y))
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
⊢ (LinearMap.mulLeft R x).range = Submodule.restrictScalars R (span {x})

Tactic:
ext
            simp [mem_span_singleton', mul_comm]

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 α
⊢ P a

Tactic:
have P_of_associated : ∀ {x y}, Associated x y → P x → P y := by
    rintro x y ⟨u, rfl⟩ hx
    exact hcp (fun p _ hpx => isUnit_of_dvd_unit hpx u.isUnit) hx (h1 u.isUnit)

Goal state after:
α : 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 α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
⊢ P a
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hP : P.LiesOver ⊥
⊢ ⊥.inertiaDeg' P = finrank R S

Tactic:
rw [inertiaDeg', dif_pos (over_def P (⊥ : Ideal R)).symm]

Goal state after:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hP : P.LiesOver ⊥
⊢ finrank (R ⧸ ⊥) (S ⧸ P) = finrank R S
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ IsIdempotentElem r

Tactic:
apply PrimeSpectrum.toPiLocalization_bijective.injective

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ (toPiLocalization R) (r * r) = (toPiLocalization R) r
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : ↥(IsUnit.submonoid M)
⊢ a * b = b * a

Tactic:
convert! mul_comm a b

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

Goal state before:
pp: case h₃.inr
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
h : p ∣ ↑(absNorm I)
Q : Ideal S
h₁ : Q.IsMaximal
h₂ : under ℤ Q = span {p}
h₃ : Q ∣ I
⊢ ∃ P_1, P_1.IsMaximal ∧ under ℤ P_1 = span {p} ∧ P_1 ∣ P * I

Tactic:
exact ⟨Q, h₁, h₂, dvd_mul_of_dvd_right h₃ _⟩

Goal state after:
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
z : S
r : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ z = r • ↑((toInvSubmonoid M S) m)

Tactic:
rw [Algebra.smul_def, ← e, mul_assoc]

Goal state after:
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
z : S
r : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ z = z * ((algebraMap R S) ↑(r, m).2 * ↑((toInvSubmonoid M S) m))
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
h : f '' (S ∩ closedPoints X) = ∅
⊢ IsClosed[inst✝¹] (f '' (S ∩ closedPoints X))

pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
x : Y
hx : x ∈ f '' (S ∩ closedPoints X)
⊢ IsClosed[inst✝¹] (f '' (S ∩ closedPoints X))

Tactic:
· simp [h]

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
x : Y
hx : x ∈ f '' (S ∩ closedPoints X)
⊢ IsClosed[inst✝¹] (f '' (S ∩ closedPoints X))
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
p : Ideal R
S₁ : Type u_1
inst✝³ : CommRing S₁
inst✝² : Algebra R S₁
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ p.ramificationIdx' (map e P) = p.ramificationIdx' P

Tactic:
rw [show P.map e = _ from P.map_comap_of_equiv (RingEquivClass.toRingEquiv e : S ≃+* S₁)]

Goal state after:
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝³ : CommRing S₁
inst✝² : Algebra R S₁
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ p.ramificationIdx' (comap (↑e).symm P) = p.ramificationIdx' P
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
inst✝¹ : IsDedekindDomain R
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hvp : v ≠ p
inst✝ : w.LiesOver v
h : w ∣ map f p
⊢ p = v

Tactic:
Ideal.dvd_iff_le,

Goal state after:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : IsDedekindDomain R
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hvp : v ≠ p
inst✝ : w.LiesOver v
h : map f p ≤ w
⊢ p = v
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
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : I ≠ ⊥ → emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v I
h : p * I ≠ ⊥
⊢ emultiplicity w (map f p) + emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v (p * I)

Tactic:
emultiplicity_mul hv.prime,

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
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : I ≠ ⊥ → emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v I
h : p * I ≠ ⊥
⊢ emultiplicity w (map f p) + emultiplicity w (map f I) =
    ↑(v.ramificationIdx' w) * (emultiplicity v p + emultiplicity v I)
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f g : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp g
⊢ (Ideal.Quotient.mkₐ R (Ideal.comap (Shrink.ringEquiv B) I)).comp ((↑(Shrink.algEquiv R B).symm).comp f) =
    (Ideal.Quotient.mkₐ R (Ideal.comap (Shrink.ringEquiv B) I)).comp ((↑(Shrink.algEquiv R B).symm).comp g)

Tactic:
by simpa [DFunLike.ext_iff, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Shrink.ringEquiv] using e

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

Goal state before:
pp: case h₂
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type w
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
⊢ (∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
    (∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
      ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R J).comp

Tactic:
h₁

Goal state after:
case h₂
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type w
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
⊢ (∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
    ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R J).comp