mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
by_cases h' : 1 ≤ p.natDegree

Goal state after:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsIntegralClosure A R B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : R
h : IsIntegral R ((algebraMap R B) x)
⊢ (algebraMap A B) (mk' A ((algebraMap R B) x) h) = (algebraMap A B) ((algebraMap R A) x)

Tactic:
by rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∉ p.support
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
· rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∉ p.support
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
⊢ (Multiset.map (fun i ↦ f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase i)).prod) f.roots).sum =
    (Multiset.map (fun x_1 ↦ f.leadingCoeff * ((Multiset.map (fun x_2 ↦ x - x_2) f.roots).prod * (1 / (x - x_1))))
        f.roots).sum

Tactic:
refine congr_arg Multiset.sum (Multiset.map_congr rfl fun z hz ↦ ?_)

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod =
    f.leadingCoeff * ((Multiset.map (fun x_1 ↦ x - x_1) f.roots).prod * (1 / (x - z)))
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (M + R ∙ x) * (M + R ∙ y) ≤ M

Tactic:
rw [add_mul]

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ M * (M + R ∙ y) + (R ∙ x) * (M + R ∙ y) ≤ M
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
⊢ (∀ (x : S), IsAlgebraic R x) → ∀ (x : K), IsAlgebraic R x

pp: case mpr
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
⊢ (∀ (x : K), IsAlgebraic R x) → ∀ (x : S), IsAlgebraic R x

Tactic:
· intro h x
    let := MulActionWithZero.nontrivial S K
    let := FractionRing.liftAlgebra R K
    have := FractionRing.isScalarTower_liftAlgebra R K
    rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]
    obtain ⟨a : S, b, ha, rfl⟩ := div_surjective S x
    obtain ⟨f, hf₁, hf₂⟩ := h b
    rw [div_eq_mul_inv]
    refine .mul ?_ (.inv ?_) <;> exact isAlgebraic_iff_isIntegral.mp <|
      (h _).algebraMap.extendScalars (FaithfulSMul.algebraMap_injective R _)

Goal state after:
case mpr
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
⊢ (∀ (x : K), IsAlgebraic R x) → ∀ (x : S), IsAlgebraic R x
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h.refine_1
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ (M + A ∙ x) * (M + A ∙ y) ≤ M

Tactic:
rw [add_mul]

Goal state after:
case h.refine_1
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ M * (M + A ∙ y) + (A ∙ x) * (M + A ∙ y) ≤ M
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfullyFlat R S
inst✝ : Flat S (S ⊗[R] M)
⊢ Flat R M

Tactic:
rw [Module.Flat.iff_lTensor_preserves_injective_linearMap]

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfullyFlat R S
inst✝ : Flat S (S ⊗[R] M)
⊢ ∀ ⦃N N' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)

Tactic:
subst_vars; exact c.isGLB_csInf

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mpr.refine_2
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen[inst✝] sU
V : Opens α
hV : V ∈ B
H : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hsU }
⊢ ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU

Tactic:
exact ⟨V, ⟨V, hV, rfl⟩, H⟩

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ∃ Us ⊆ B, U = sSup Us

Tactic:
refine ⟨{ V : Opens α | V ∈ B ∧ V ≤ U }, fun U hU => hU.left, ext ?_⟩

Goal state after:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ↑U = ↑(sSup {V | V ∈ B ∧ V ≤ U})
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
H : ∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))
i : ι
x : ↑(f ⁻¹' (U i).carrier)
⊢ 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))

Tactic:
rw [Function.comp_apply, ← H, ← IsInducing.subtypeVal.nhds_eq_comap]

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
⊢ ∀ {a b : Opens α},
    { toFun := ⇑(comap ↑f.symm), invFun := ⇑(comap ↑f), left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := ⇑(comap ↑f.symm), invFun := ⇑(comap ↑f), left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by
    simp only [← SetLike.coe_subset_coe]; exact f.symm.surjective.preimage_subset_preimage_iff

Goal state after:
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
⊢ Function.Injective (map f ⋯)

Tactic:
intro A B h_images_eq

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : map f ⋯ A = map f ⋯ B
⊢ A = B
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
⊢ ∀ (hx : (∅.sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s), p (∅.sup fun x ↦ ↑x.1 \ ↑x.2) hx

Tactic:
by simpa using sdiff _ bot_mem _ bot_mem

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i ↦ ↑(f i)
⊢ ↑(f a ⊔ s.sup f) = ↑(f a) ⊔ s.sup fun i ↦ ↑(f i)

Tactic:
coe_sup,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i ↦ ↑(f i)
⊢ ↑(f a) ∪ ↑(s.sup f) = ↑(f a) ⊔ s.sup fun i ↦ ↑(f i)
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
⊢ x ∉ I ∨ xᶜ ∉ I

Tactic:
by
  have h : xᶜ ∈ I → x ∉ I := hI.notMem_of_compl_mem
  tauto

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : W₂ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ IsCompact W₁ᶜᶜ

Tactic:
simp [hW₁.1.2]

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s : Set X
hs : IsConstructible s
⊢ P s hs

Tactic:
induction s, hs using BooleanSubalgebra.closure_sdiff_sup_induction with

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

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this✝ : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
hl : Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl
⊢ p = Ideal.under R Pl

Tactic:
← Ideal.under_under (B := (Localization.AtPrime <| Q.under R)) Pl,

Goal state after:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this✝ : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
hl : Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl
⊢ p = Ideal.under R (Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl)
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
⊢ (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A B)

Tactic:
rw [e]; ext; rfl

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Module.Flat R S
⊢ GeneralizingMap (comap (algebraMap R S))

Tactic:
← Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Module.Flat R S
⊢ Algebra.HasGoingDown R S
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ (IsClosedMap fun a ↦ (primeSpectrumProd R S).symm (Sum.inl a)) ∧
    IsClosedMap fun b ↦ (primeSpectrumProd R S).symm (Sum.inr b)

Tactic:
primeSpectrumProd_symm_inl,

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ (IsClosedMap fun a ↦ comap (RingHom.fst R S) a) ∧ IsClosedMap fun b ↦ (primeSpectrumProd R S).symm (Sum.inr b)
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
⊢ D a⁻¹ = -a⁻¹ ^ 2 • D a

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
⊢ D 0⁻¹ = -0⁻¹ ^ 2 • D 0

case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ D a⁻¹ = -a⁻¹ ^ 2 • D a
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ n.natAbs • a ^ (n.natAbs - 1) • D a = n.natAbs • a ^ (↑n.natAbs - 1) • D a

Tactic:
rw [← zpow_natCast]

Goal state after:
case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ n.natAbs • a ^ ↑(n.natAbs - 1) • D a = n.natAbs • a ^ (↑n.natAbs - 1) • D a
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1

Tactic:
simp_rw [exponent, dif_neg h, pow_zero]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ g, map H.subtype (zpowers g) = H) ↔ ∃ g, zpowers g = H

Tactic:
MonoidHom.map_zpowers,

Goal state after:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ g, zpowers (H.subtype g) = H) ↔ ∃ g, zpowers g = H
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ⊥.factorization p ≠ 0
ht : exponent G = ⊥
⊢ ⊥.factorization p = 0

Tactic:
rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_1
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
⊢ a ^ n = a ^ (↑n).val

Tactic:
rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha,
      Int.modEq_comm, Int.modEq_iff_add_fac, Nat.card_eq_fintype_card, ← ZMod.intCast_eq_iff]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ (hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n

Tactic:
by rw [← Nat.card_zpowers]; rfl

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]

Tactic:
calc
      card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
        card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
      _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
      _ = _ := by simp
    rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]
    have key :
      ∀ x,
        card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } =
          card (orbit G x) :=
      fun x => by simp only [Quotient.eq'']; congr
    refine
      Eq.symm
        (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
          (fun a₁ _ _ a₂ _ _ h =>
            Subtype.ext (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
          (fun b => Quotient.inductionOn' b fun b _ hb => ?_) fun a ha _ => by
          rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
    obtain ⟨k, hk⟩ := hG.card_orbit b
    rw [Nat.card_eq_fintype_card] at hk
    have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]
    exact
      ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩,
        Finset.mem_univ _, ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
have : s = basicOpen x := by
    refine subset_antisymm ?_ ?_
    · rw [← hJ', basicOpen_eq_zeroLocus_of_mul_add _ _ mul add]
      exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hy)
    · rw [basicOpen_eq_zeroLocus_compl, Set.compl_subset_comm, ← hI']
      exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hx)

Goal state after:
case inr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this✝ : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
this : s = ↑(basicOpen x)
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
⊢ ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1

Tactic:
peel hj with n hn _

Goal state after:
case h.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
this : ∃ g, g ^ n ≠ 1
⊢ ∃ g, g ^ n ≠ 1