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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ ∀ (a : S ⧸ Q), H.restrict a = 0 → a = 0

Tactic:
intro x hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
x : S ⧸ Q
hx : H.restrict x = 0
⊢ x = 0
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
Q : Ideal S
σ : G
inst✝ : Q.IsPrime
h : IsArithFrobAt R σ Q
| σ • Q

Tactic:
← h.comap_eq

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
Q : Ideal S
σ : G
inst✝ : Q.IsPrime
h : IsArithFrobAt R σ Q
| σ • Ideal.comap (MulSemiringAction.toAlgHom R S σ) Q
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x y : SummableFamily Γ R α
⊢ ⋃ a, ((⇑x + ⇑y) a).support ⊆ (⋃ a, (x a).support) ∪ ⋃ a, (y a).support

Tactic:
← Set.iUnion_union_distrib

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x y : SummableFamily Γ R α
⊢ ⋃ a, ((⇑x + ⇑y) a).support ⊆ ⋃ i, (x i).support ∪ (y i).support
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
ι : Type u_7
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
⊢ ∀ (x_1 : ι), x_1 ≠ i → ((single i x) x_1).coeff g = 0

Tactic:
simp +contextual

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
⊢ (coeff (single 0 1)) ((MvPowerSeries.map f) F.toPowerSeries) = 1

Tactic:
by simp [F.lin_coeff_X]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
⊢ (coeff (single 1 1)) ((MvPowerSeries.map f) F.toPowerSeries) = 1

Tactic:
by simp [F.lin_coeff_Y]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
⊢ {a | (f a • s a).coeff g ≠ 0}.Finite

Tactic:
by
    refine Set.Finite.subset (s.finite_co_support g) fun i hi => ?_
    simp_all only [coeff_smul, ne_eq, Set.mem_ofPred_eq, Function.mem_support]
    exact right_ne_zero_of_smul hi

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
⊢ gh ∈ VAddAntidiagonal g ⋯

pp: case refine_2
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Tactic:
· simp_all only [mem_vaddAntidiagonal, Function.mem_support, Set.mem_iUnion, mem_support]
    exact ⟨Exists.intro a.1 hgh.1, Exists.intro a.2 hgh.2.1, trivial⟩

Goal state after:
case refine_2
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![f, 0] F.toPowerSeries = f

Tactic:
by
  calc
    _ = PowerSeries.subst f (F.toPowerSeries.subst ![PowerSeries.X (R := R), 0]) := by
      rw [PowerSeries.subst, subst_comp_subst_apply _ hf.const]
      · congr! 2 with s
        fin_cases s
        · simp [PowerSeries.X, subst]
        · simp [subst, eval₂]
      exact HasSubst.X_zero
    _ = _ := by
      simp [Xzero_eq_X, PowerSeries.subst_X hf]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
g : Γ
⊢ {a | ¬(0 ^ a).coeff g = 0} ⊆ {0}

Tactic:
simp only [Set.subset_singleton_iff, Set.mem_ofPred_eq]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
g : Γ
⊢ ∀ (y : ℕ), ¬(0 ^ y).coeff g = 0 → y = 0
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
⊢ (x ^ n).cardSupp ≤ x.cardSupp ^ n

Tactic:
induction n with
  | zero => simp
  | succ n IH =>
    simpa [pow_succ] using (cardSupp_mul_le ..).trans <| mul_le_mul_left IH _

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ lift.{0, u_1} (SummableFamily.powers x).hsum.cardSupp ≤ max ℵ₀ x.cardSupp

Tactic:
← sum_pow_le_max_aleph0,

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ lift.{0, u_1} (SummableFamily.powers x).hsum.cardSupp ≤ sum fun n ↦ x.cardSupp ^ n
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (↑f).toLinearMap ∘ₗ (toConv (antipode R) * toConv LinearMap.id).ofConv = ofConv 1 ∘ₗ f.toLinearMap

Tactic:
by
          rw [antipode_mul_id, algHom_comp_convOne, ← convOne_comp_coalgHom f.toCoalgHom]

Goal state after:
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingUp R S
P : PrimeSpectrum S
q : PrimeSpectrum R
hq : PrimeSpectrum.comap (algebraMap R S) P ≤ q
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' P ∧ PrimeSpectrum.comap (algebraMap R S) a' = q

Tactic:
obtain ⟨Q, hle, hQ, h⟩ := P.asIdeal.exists_ideal_ge_liesOver_of_le (q := q.asIdeal)
      (p := P.asIdeal.under R) hq

Goal state after:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingUp R S
P : PrimeSpectrum S
q : PrimeSpectrum R
hq : PrimeSpectrum.comap (algebraMap R S) P ≤ q
Q : Ideal S
hle : P.asIdeal ≤ Q
hQ : Q.IsPrime
h : Q.LiesOver q.asIdeal
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' P ∧ PrimeSpectrum.comap (algebraMap R S) a' = q
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case hIN.refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : comap f (map f q ^ n) ⊔ I = comap f (map f q ^ n.succ) ⊔ I
⊢ (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n) ≤
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)) (map f q ^ (n + 1)) ⊔
      I •
        (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
          (map (algebraMap R (Localization.AtPrime q)) q ^ n)

Tactic:
intro x hx

Goal state after:
case hIN.refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : comap f (map f q ^ n) ⊔ I = comap f (map f q ^ n.succ) ⊔ I
x : R
hx :
  x ∈
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n)
⊢ x ∈
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)) (map f q ^ (n + 1)) ⊔
      I •
        (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
          (map (algebraMap R (Localization.AtPrime q)) q ^ n)
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
I : Ideal A
⊢ F.IsTorsionQuot I I

Tactic:
intro x hx

Goal state after:
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
I : Ideal A
x : A
hx : x ∈ I
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon I {x}
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
I J K : Ideal A
hI : F.IsTorsionQuot I K
hJ : F.IsTorsionQuot J K
⊢ F.IsTorsionQuot (I ⊓ J) K

Tactic:
intro x hx

Goal state after:
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
I J K : Ideal A
hI : F.IsTorsionQuot I K
hJ : F.IsTorsionQuot J K
x : A
hx : x ∈ K
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon (I ⊓ J) {x}
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case hIN.refine_2.hy
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : comap f (map f q ^ n) ⊔ I = comap f (map f q ^ n.succ) ⊔ I
y : R
hy : y ∈ comap f (map f q ^ n.succ)
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx : f (Submodule.IsPrincipal.generator I) * f z ∈ map f q ^ n
⊢ ¬span {Submodule.IsPrincipal.generator I} ≤ q

Tactic:
Ideal.span_singleton_generator

Goal state after:
case hIN.refine_2.hy
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : comap f (map f q ^ n) ⊔ I = comap f (map f q ^ n.succ) ⊔ I
y : R
hy : y ∈ comap f (map f q ^ n.succ)
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx : f (Submodule.IsPrincipal.generator I) * f z ∈ map f q ^ n
⊢ ¬I ≤ q
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
⊢ q ∈ (span t).minimalPrimes

Tactic:
let f := Quotient.mk (span t)

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
⊢ q ∈ (span t).minimalPrimes
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
⊢ I ≤ RingHom.ker (algebraMap R (Localization.AtPrime p))

Tactic:
intro x hx

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
⊢ x ∈ RingHom.ker (algebraMap R (Localization.AtPrime p))
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
⊢ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) = I

Tactic:
refine le_antisymm ?_ fun x hx ↦ ?_

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
⊢ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) ≤ I

case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
⊢ x ∈ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal))
Module: Mathlib.RingTheory.KrullDimension.LocalRing

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
⊢ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical

Tactic:
intro x hx

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
⊢ IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
Module: Mathlib.RingTheory.Spectrum.Prime.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
⊢ support A M ⊆ PrimeSpectrum.comap (algebraMap R A) ⁻¹' support R M

Tactic:
intro x hx

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
hx : x ∈ support A M
⊢ x ∈ PrimeSpectrum.comap (algebraMap R A) ⁻¹' support R M
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : ⟨y, hy⟩ ∈ Subring.center ↥R
⊢ x * y = y * x

Tactic:
rw [Subring.mem_center_iff] at this

Goal state after:
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : ∀ (g : ↥R), g * ⟨y, hy⟩ = ⟨y, hy⟩ * g
⊢ x * y = y * x
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
⊢ ∃ g ∉ q, IsStandardOpenImmersion R (Localization.Away g)

Tactic:
obtain ⟨i, hi⟩ : ∃ i, f i ∉ q := by
    rw [← PrimeSpectrum.iSup_basicOpen_eq_top_iff] at h
    have : ⟨q, hq⟩ ∈ ⨆ i, PrimeSpectrum.basicOpen (f i) := by simp [h]
    simpa using this

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
⊢ ∃ g ∉ q, IsStandardOpenImmersion R (Localization.Away g)
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
⊢ ↑(s { asIdeal := P, isMaximal := hP }) ⊆
    ↑(Submodule.span (Rₚ P) (⇑(f P) '' ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))))

Tactic:
intro x hx

Goal state after:
case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
x : Mₚ { asIdeal := P, isMaximal := hP }.asIdeal
hx : x ∈ ↑(s { asIdeal := P, isMaximal := hP })
⊢ x ∈ ↑(Submodule.span (Rₚ P) (⇑(f P) '' ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))))
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mp.refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ s - (aeval β) q ∈ Submodule.restrictScalars R (Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
rw [Algebra.FormallyUnramified.map_maximalIdeal, Submodule.restrictScalars_mem,
        ← Ideal.Quotient.eq]

Goal state after:
case mp.refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ (Ideal.Quotient.mk (maximalIdeal S)) s = (Ideal.Quotient.mk (maximalIdeal S)) ((aeval β) q)
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : ¬IsLocalRing R
⊢ ∃ K₁ K₂ x x_1 f, Function.Surjective ⇑f

Tactic:
obtain ⟨m₁, m₂, _, _, hm₁m₂⟩ := (not_isLocalRing_tfae.out 0 2).mp h

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : ¬IsLocalRing R
m₁ m₂ : Ideal R
left✝¹ : m₁.IsMaximal
left✝ : m₂.IsMaximal
hm₁m₂ : m₁ ≠ m₂
⊢ ∃ K₁ K₂ x x_1 f, Function.Surjective ⇑f
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case neg.convert_10
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
hi : ¬m i = 0
⊢ (weight w) (m - single i 1) + w i = n' + w i

Tactic:
h',

Goal state after:
case neg.convert_10
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
hi : ¬m i = 0
⊢ (weight w) (m - single i 1) + w i = n
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

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
Rₚ : Type u_3
inst✝⁸ : CommRing Rₚ
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : IsLocalization.AtPrime Rₚ p
inst✝⁵ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
⊢ P = comap (algebraMap S Sₚ) (RingHom.ker (algebraMap Sₚ (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)))

Tactic:
Quotient.algebraMap_eq,

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
Rₚ : Type u_3
inst✝⁸ : CommRing Rₚ
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : IsLocalization.AtPrime Rₚ p
inst✝⁵ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
⊢ P = comap (algebraMap S Sₚ) (RingHom.ker (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)))