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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔ ∃ c, TrivSqZeroExt.fst x = 0 ∧ TrivSqZeroExt.snd x = 1 * TrivSqZeroExt.fst c

Tactic:
one_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔ ∃ c, TrivSqZeroExt.fst x = 0 ∧ TrivSqZeroExt.snd x = TrivSqZeroExt.fst c
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inr.inr.inr
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x ≠ 0
⊢ ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x

Tactic:
refine ⟨inl ((fst x)⁻¹ * fst y), ?_⟩

Goal state after:
case inr.inr.inr
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x ≠ 0
⊢ fst x * (inl ((fst x)⁻¹ * fst y)).fst = fst y ∨ fst y * (inl ((fst x)⁻¹ * fst y)).fst = fst x
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
p : PrimeSpectrum R
⊢ Ideal.comap (Ideal.Quotient.mkₐ k p.asIdeal) ⊥ = p.asIdeal

Tactic:
← RingHom.ker_eq_comap_bot,

Goal state after:
k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
p : PrimeSpectrum R
⊢ RingHom.ker (Ideal.Quotient.mkₐ k p.asIdeal) = p.asIdeal
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ WeaklyEtale (ULift.{u₁, u_1} R) (ULift.{u₂, u_2} S) ↔ WeaklyEtale R S

Tactic:
by
  rw [weaklyEtale_iff, weaklyEtale_iff, Module.Flat.ulift_left_iff, Module.Flat.ulift_right_iff]
  congr!
  conv_rhs => rw [← RingHom.Flat.ulift_iff.{u₁, u₂}]
  rw [TensorProduct.lmul'_ulift, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom]
  exact RingHom.Flat.comp_iff_of_bijective_right (Equiv.bijective _)

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a x : A
hx : x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
⊢ a * x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}

Tactic:
exact ⟨I.mul_mem_left a hx.1, (fun n ↦ by rw [hI.dpow_mul hx.1, hI'.dpow_mul hx.1, hx.2])⟩

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
⊢ J ⊓ I ≤ I

Tactic:
by simp only [inf_le_right]

Goal state after:
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✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ 1 * ζ ^ (i * j) - ζ ^ ((q + k - i) * j) * ζ ^ (i * j) ∈ Q

Tactic:
one_mul,

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✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ ζ ^ (i * j) - ζ ^ ((q + k - i) * j) * ζ ^ (i * j) ∈ Q
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✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ φ (ζ ^ j) - ζ ^ (q * j) ∈ Q

Tactic:
mul_comm,

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✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ φ (ζ ^ j) - ζ ^ (j * q) ∈ Q
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: case inr
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✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this✝ : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ (q + k - i) * ζ ^ i = 1 * ζ ^ i
⊢ φ ζ = ζ ^ q

Tactic:
one_mul,

Goal state after:
case inr
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✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this✝ : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ (q + k - i) * ζ ^ i = ζ ^ i
⊢ φ ζ = ζ ^ q
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
⊢ mk 1 * (1 - X) = 1

Tactic:
mul_comm,

Goal state after:
S : Type u_1
inst✝ : CommRing S
⊢ (1 - X) * mk 1 = 1
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n ↦ ↑((d + n).choose d)
n : ℕ
⊢ (coeff n) ((mk fun n ↦ ↑((d + n).choose d)) * mk 1) = (coeff n) (mk fun n ↦ ↑((d + 1 + n).choose (d + 1)))

Tactic:
mul_comm,

Goal state after:
case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n ↦ ↑((d + n).choose d)
n : ℕ
⊢ (coeff n) (mk 1 * mk fun n ↦ ↑((d + n).choose d)) = (coeff n) (mk fun n ↦ ↑((d + 1 + n).choose (d + 1)))
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
⊢ ((1 - X) * mk 1) ^ (d + 1) = 1

Tactic:
mul_comm,

Goal state after:
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
⊢ (mk 1 * (1 - X)) ^ (d + 1) = 1
Module: Mathlib.RingTheory.PowerSeries.Binomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r s : R
n : ℕ
ab : ℕ × ℕ
hab : ab ∈ antidiagonal n
⊢ (Ring.choose r ab.1 * Ring.choose s ab.2) • 1 = Ring.choose s ab.2 • Ring.choose r ab.1 • 1

Tactic:
mul_comm,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r s : R
n : ℕ
ab : ℕ × ℕ
hab : ab ∈ antidiagonal n
⊢ (Ring.choose s ab.2 * Ring.choose r ab.1) • 1 = Ring.choose s ab.2 • Ring.choose r ab.1 • 1
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    simp [X, monomial_mul_monomial, coeff_monomial, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)]

Goal state after:
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 : Γ
⊢ ((single i x) i).coeff g = x.coeff g

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:
single_toFun,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
ι : Type u_7
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
⊢ (Pi.single i x i).coeff g = x.coeff g

Γ : 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
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g g' : Γ
hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g'
hg' : ∑ i ∈ (s.coeff g').support, (s i).coeff g' ≠ 0
⊢ g ≤ g'

Tactic:
obtain ⟨i, _, hi⟩ := Finset.exists_ne_zero_of_sum_ne_zero hg'

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g g' : Γ
hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g'
hg' : ∑ i ∈ (s.coeff g').support, (s i).coeff g' ≠ 0
i : α
left✝ : i ∈ (s.coeff g').support
hi : (s i).coeff g' ≠ 0
⊢ g ≤ g'
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : g = 0
⊢ (if 0 = 0 then r • (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g

Tactic:
simp [hg, Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : ¬g = 0
⊢ (if 0 = 0 then r • (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g

Tactic:
simp [hg, Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
⊢ ∀ y ∈ ⋃ n, (x ^ n).support,
    (∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite) →
      {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0}.Finite

Tactic:
intro y ys hy

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
⊢ {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0}.Finite
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
⊢ (if u.order + i.order = 0 then 1 else 0) = 1

Tactic:
if_pos

Goal state after:
case mp
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
⊢ 1 = 1

case mp.hc
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
⊢ u.order + i.order = 0
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsNoetherianRing R
h : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p
⊢ UniqueFactorizationMonoid R

Tactic:
rw [iff_exists_prime_mem_of_isPrime]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsNoetherianRing R
h : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p
⊢ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
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
  obtain ⟨J, hJ⟩ := F.nonempty
  exact ⟨J, hJ, le_of_le_of_eq le_top (by simpa [eq_comm])⟩

Goal state after:
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
y : R
hy : y ∈ comap f (map f q ^ n.succ)
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx : f z * f (Submodule.IsPrincipal.generator I) ∈ map f q ^ n
⊢ z ∈
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n)

Tactic:
mul_comm,

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
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
⊢ z ∈
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n)
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I J : Ideal R
inst✝ : I.Pure
⊢ Function.Injective ⇑(Submodule.subtype J)

Tactic:
exact J.injective_subtype

Goal state after:
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
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝⁴ : p.IsPrime
this✝³ : (map f p).IsPrime
h : (map f p).height ≤ 1
h_lt : map f q < map f p
this✝² : (map f q).IsPrime
this✝¹ : (map f p).FiniteHeight
this✝ : map f q ∈ minimalPrimes (R ⧸ span t)
this : q ⊔ comap f ⊥ ∈ (comap f ⊥).minimalPrimes
⊢ q ∈ (span t).minimalPrimes

Tactic:
← RingHom.ker_eq_comap_bot,

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)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝⁴ : p.IsPrime
this✝³ : (map f p).IsPrime
h : (map f p).height ≤ 1
h_lt : map f q < map f p
this✝² : (map f q).IsPrime
this✝¹ : (map f p).FiniteHeight
this✝ : map f q ∈ minimalPrimes (R ⧸ span t)
this : q ⊔ RingHom.ker f ∈ (RingHom.ker f).minimalPrimes
⊢ q ∈ (span t).minimalPrimes
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
⊢ Function.Injective ⇑(Hom.hom P.toLimit).toMonoidHom

Tactic:
← MonoidHom.ker_eq_bot_iff,

Goal state after:
P : ProfiniteGrp.{u}
⊢ (Hom.hom P.toLimit).ker = ⊥
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝³ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this✝² : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (algebraMap R[X] Rₚ[X]) P
disj : Disjoint ↑(Submonoid.map C p.primeCompl) ↑P
eq : under R[X] (Ideal.map (algebraMap R[X] Rₚ[X]) P) = P
this✝¹ : (under R[X] P').IsMaximal
this✝ : P'.IsMaximal
this : P'.LiesOver p'
⊢ p.height = p'.height

Tactic:
height_map_of_disjoint p.primeCompl

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝³ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this✝² : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (algebraMap R[X] Rₚ[X]) P
disj : Disjoint ↑(Submonoid.map C p.primeCompl) ↑P
eq : under R[X] (Ideal.map (algebraMap R[X] Rₚ[X]) P) = P
this✝¹ : (under R[X] P').IsMaximal
this✝ : P'.IsMaximal
this : P'.LiesOver p'
⊢ p.height = p.height

case h
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝³ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this✝² : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (algebraMap R[X] Rₚ[X]) P
disj : Disjoint ↑(Submonoid.map C p.primeCompl) ↑P
eq : under R[X] (Ideal.map (algebraMap R[X] Rₚ[X]) P) = P
this✝¹ : (under R[X] P').IsMaximal
this✝ : P'.IsMaximal
this : P'.LiesOver p'
⊢ Disjoint ↑p.primeCompl ↑p
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
⊢ under R (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p)) (RelSeries.head lq)).asIdeal ≤
    comap (algebraMap R S) P

Tactic:
refine comap_mono (le_trans (comap_mono (lq.head_le_last)) ?_)

Goal state after:
case refine_2
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
⊢ comap (Quotient.mk (map (algebraMap R S) p)) (RelSeries.last lq).asIdeal ≤ P
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: 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) = ⊤
⊢ Module.Finite R M

Tactic:
choose frac hfrac using fun P : MaximalSpectrum R ↦ IsLocalizedModule.surj P.1.primeCompl (f P.1)

Goal state after:
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
⊢ Module.Finite R M
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case refine_1
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✝ : Etale R S
β : S
hadj : R[β] = ⊤
h : (minpoly R β).Monic
⊢ (aeval ((residue S) β)) (map (residue R) (minpoly R β)) = 0

Tactic:
rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl]
    simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ (Ring.choose (n + ↑k) k * Ring.choose (n + ↑k + ↑l) l) • f.coeff (n + ↑k + ↑l) =
    (k + l).choose k • Ring.choose (n + (↑k + ↑l)) (k + l) • f.coeff (n + (↑k + ↑l))

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ (Ring.choose (n + ↑k + ↑l) l * Ring.choose (n + ↑k) k) • f.coeff (n + ↑k + ↑l) =
    (k + l).choose k • Ring.choose (n + (↑k + ↑l)) (k + l) • f.coeff (n + (↑k + ↑l))
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Nontrivial R₁
inst✝ : Nontrivial R₂
ha : ¬IsUnit (1, 0)
h : IsUnit (0, 1)
⊢ IsUnit 0

Tactic:
simpa using h.map (RingHom.fst R₁ R₂)

Goal state after: