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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
⊢ (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
          (mapAlgHom M includeRight) ⋯).comp
      rTensorEquivAlgEquiv.invFun =
    AlgHom.id A (A ⊗[R] B)[M]

Tactic:
apply AlgHom.toLinearMap_injective

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
⊢ ((Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
            (mapAlgHom M includeRight) ⋯).comp
        rTensorEquivAlgEquiv.invFun).toLinearMap =
    (AlgHom.id A (A ⊗[R] B)[M]).toLinearMap
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
⊢ (AlgHom.restrictScalars R
          (rTensorEquivAlgEquiv.invFun.comp
            (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
              (mapAlgHom M includeRight) ⋯))).comp
      includeRight =
    (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))).comp includeRight

Tactic:
apply AlgHom.toLinearMap_injective

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
⊢ ((AlgHom.restrictScalars R
            (rTensorEquivAlgEquiv.invFun.comp
              (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
                (mapAlgHom M includeRight) ⋯))).comp
        includeRight).toLinearMap =
    ((AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))).comp includeRight).toLinearMap
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (-f).Splits

Tactic:
← neg_one_mul,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (-1 * f).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
p : R[X]
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
f : R[X]
hf₀ : (X - C a) * f ≠ 0
hp : (X - C a) * (f * g) = p
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
⊢ ((X - C a) * f).Splits ∧ g.Splits

Tactic:
subst hp

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : ((X - C a) * (f * g)).natDegree = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ ((X - C a) * f).Splits ∧ g.Splits
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✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this✝ : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral (↥S) x
Sx : Submodule (↥S) B := Subalgebra.toSubmodule (↥S)[x]
MSx : Module ↥S ↥Sx := SMulMemClass.toModule Sx
this : Module.Finite ↥S ↥Sx
⊢ Module.Finite R ↥(Subalgebra.toSubmodule (Subalgebra.restrictScalars R (↥S)[x]))

Tactic:
let : SMul S Sx := { MSx with }

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this✝¹ : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral (↥S) x
Sx : Submodule (↥S) B := Subalgebra.toSubmodule (↥S)[x]
MSx : Module ↥S ↥Sx := SMulMemClass.toModule Sx
this✝ : Module.Finite ↥S ↥Sx
this : SMul ↥S ↥Sx := MSx.toSMul
⊢ Module.Finite R ↥(Subalgebra.toSubmodule (Subalgebra.restrictScalars R (↥S)[x]))
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case inr.refine_1
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ p.leadingCoeff ∈ (algebraMap R Rₘ).range

Tactic:
hp₁.leadingCoeff

Goal state after:
case inr.refine_1
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ 1 ∈ (algebraMap R Rₘ).range
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ s ⊆ ↑(vanishingIdeal Set.univ) ↔ s ⊆ ↑(nilradical R)

Tactic:
vanishingIdeal_univ

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ s ⊆ ↑(nilradical R) ↔ s ⊆ ↑(nilradical R)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : IsLocalRing R
inst✝¹² : CommRing S
inst✝¹¹ : IsLocalRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : IsLocalRing T
inst✝⁸ : Algebra R S
inst✝⁷ : IsLocalHom (algebraMap R S)
R₀ : Type u_4
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : IsLocalRing R₀
inst✝¹ : IsLocalHom (algebraMap R₀ R)
inst✝ : IsLocalHom (algebraMap R₀ S)
x : ResidueField R₀
⊢ (algebraMap (ResidueField R₀) (ResidueField S)) x =
    (algebraMap (ResidueField R) (ResidueField S)) ((algebraMap (ResidueField R₀) (ResidueField R)) x)

Tactic:
obtain ⟨x, rfl⟩ := residue_surjective x

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : IsLocalRing R
inst✝¹² : CommRing S
inst✝¹¹ : IsLocalRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : IsLocalRing T
inst✝⁸ : Algebra R S
inst✝⁷ : IsLocalHom (algebraMap R S)
R₀ : Type u_4
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : IsLocalRing R₀
inst✝¹ : IsLocalHom (algebraMap R₀ R)
inst✝ : IsLocalHom (algebraMap R₀ S)
x : R₀
⊢ (algebraMap (ResidueField R₀) (ResidueField S)) ((residue R₀) x) =
    (algebraMap (ResidueField R) (ResidueField S)) ((algebraMap (ResidueField R₀) (ResidueField R)) ((residue R₀) x))
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : (algebraMap S (S ⊗[R] T)) ((algebraMap R S) r) ∈ J
⊢ False

Tactic:
simp only [Algebra.algebraMap_eq_smul_one (A := S), Algebra.TensorProduct.algebraMap_apply,
      Algebra.algebraMap_self, id_apply, smul_tmul, ← Algebra.algebraMap_eq_smul_one (A := T)] at H

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : 1 ⊗ₜ[R] (algebraMap R T) r ∈ J
⊢ False
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
I : Ideal R
inst✝² : I.IsPrime
k : Type u_5
inst✝¹ : Field k
p : Ideal k
inst✝ : p.IsPrime
⊢ p.IsMaximal

Tactic:
by simpa [p.eq_bot_of_prime] using Ideal.bot_isMaximal

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I : Ideal R
inst✝ : I.IsPrime
f : R →+* S
hf₁ : I ≤ RingHom.ker f
hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)
r : R
⊢ (lift I f hf₁ hf₂) ((algebraMap R I.ResidueField) r) = f r

Tactic:
lift,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I : Ideal R
inst✝ : I.IsPrime
f : R →+* S
hf₁ : I ≤ RingHom.ker f
hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)
r : R
⊢ (IsLocalization.lift ⋯) ((algebraMap R I.ResidueField) r) = f r
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal R
hI : ker f = I
⊢ LeftInverse
    (fun x ↦
      match x with
      | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ })
    fun p ↦ ⟨PrimeSpectrum.comap f p, ⋯⟩

Tactic:
intro ⟨p, _⟩
    simp only [PrimeSpectrum.mk.injEq]
    exact p.map_comap_of_surjective f hf

Goal state after:
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case mpr
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ (∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i) → IsCompact U ∧ IsOpen U

Tactic:
· rintro ⟨s, hs, rfl⟩
    constructor
    · exact hs.isCompact_biUnion fun i _ => hb' i
    · exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)

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:
simp only [← SetLike.coe_subset_coe]

Goal state after:
ι : 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
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)

Tactic:
refine ⟨fun hf ↦ fun i ↦ hf.restrictPreimage _, fun hf ↦ fun x y h ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h : (fun x1 x2 ↦ x1 ⤳ x2) y (f x)
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ ↑S, IsClosed[inst✝¹] t
hSi : ∀ t ∈ ↑S, IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
t : Set α
htS : t ∈ S
ht : s ⊆ t
⊢ s ∈ ↑S

Tactic:
ht.antisymm (hs.2 (hSi _ htS) ht)

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ ↑S, IsClosed[inst✝¹] t
hSi : ∀ t ∈ ↑S, IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
t : Set α
htS : t ∈ S
ht : s ⊆ t
⊢ t ∈ ↑S
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
x : Y
⊢ (∃ i, ∃ (_ : i ∈ t), x ∈ f '' ↑↑i) → x ∈ U

Tactic:
rintro ⟨i, hi, x, hx, rfl⟩

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
i : ↑Us
hi : i ∈ t
x : X
hx : x ∈ ↑↑i
⊢ f x ∈ U
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : CompleteLattice P
I : Ideal P
α : Sort u_2
inst✝ : Finite α
f : α → P
⊢ ⨆ i, f i ∈ I ↔ ∀ (i : α), f i ∈ I

Tactic:
simpa [← Equiv.plift.symm.iSup_comp, Equiv.plift.forall_congr_left]
    using biSup_mem_iff (f := f ∘ PLift.down) Set.finite_univ

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case refine_1
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∀ I ∈ SetLike.coe '' S, IsIdeal I

pp: case refine_2
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∀ (x y : Ideal P), x ≤ y → ↑x ⊆ ↑y

pp: case refine_3
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ⋯.toIdeal ≠ ⊤

pp: case refine_4
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ⋯.toIdeal ∈ upperBounds S

Tactic:
· simp [Ideal.isIdeal]

Goal state after:
case refine_2
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∀ (x y : Ideal P), x ≤ y → ↑x ⊆ ↑y

case refine_3
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ⋯.toIdeal ≠ ⊤

case refine_4
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ⋯.toIdeal ∈ upperBounds S
Module: Mathlib.Topology.Sober

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst✝¹] (T ∩ range f))
hxT : f y ∈ T
⊢ closure[inst✝²] {y} = f ⁻¹' T

Tactic:
hf.isEmbedding.closure_eq_preimage_closure_image,

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst✝¹] (T ∩ range f))
hxT : f y ∈ T
⊢ f ⁻¹' closure[inst✝¹] (f '' {y}) = f ⁻¹' T
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (f '' sᶜ)

Tactic:
← range_sdiff_image hfopen.injective

Goal state after:
case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (range f \ f '' s)
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : R1Space α
S✝ : Set α
h : IsIrreducible S✝
hs : IsClosed S✝
⊢ ∃ x, IsGenericPoint x S✝

Tactic:
obtain ⟨x, hx⟩ := h.nonempty
    use x
    apply subset_antisymm
    · rw [← hs.closure_eq]
      exact closure_mono (singleton_subset_iff.mpr hx)
    · exact isPreirreducible_iff_forall_mem_subset_closure_singleton.mp h.isPreirreducible x hx

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.Flat
⊢ PreservesFiniteLimits (extendScalars f)

Tactic:
have : PreservesFiniteLimits (extendScalars.{_, _, u} f ⋙ restrictScalars.{_, _, u} f) :=
    ModuleCat.preservesFiniteLimits_tensorLeft_of_ringHomFlat hf
  exact preservesFiniteLimits_of_reflects_of_preserves (extendScalars f) (restrictScalars f)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hpq : p < q
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p

Tactic:
obtain ⟨P, hPQ, _, _⟩ := Q.exists_ideal_le_liesOver_of_le (p := p) (q := q) hpq.le
  refine ⟨P, ?_, inferInstance, inferInstance⟩
  by_contra hc
  have : P = Q := eq_of_le_of_not_lt hPQ hc
  subst this
  simp [P.over_def p, P.over_def q] at hpq

Goal state after:
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
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
⊢ (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) ∈ I * I

Tactic:
convert! Ideal.mul_mem_mul (F x).2 (F y).2 using 1

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
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
D : Type u_7
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : B →ₐ[R] D
hf : f.Flat
⊢ (Algebra.TensorProduct.lTensor A f).Flat

Tactic:
algebraize [f.toRingHom, (Algebra.TensorProduct.lTensor (S := A) A f).toRingHom]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
D : Type u_7
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : B →ₐ[R] D
hf : f.Flat
algInst✝¹ : Algebra B D := f.toAlgebra
algInst✝ : Algebra (A ⊗[R] B) (A ⊗[R] D) := (Algebra.TensorProduct.lTensor A f).toAlgebra
algebraizeInst✝ : Module.Flat B D
⊢ (Algebra.TensorProduct.lTensor A f).Flat
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A) = CommRingCat.ofHom (algebraMap R A)

Tactic:
by simp [IsScalarTower.algebraMap_eq R S A]

Goal state after:
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 b : K
⊢ (b * b⁻¹ * b⁻¹) • D a + -((a * (b ^ 2)⁻¹) • D b) = ((b ^ 2)⁻¹ * b) • D a + -(((b ^ 2)⁻¹ * a) • D b)

Tactic:
ring_nf

Goal state after:
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 b : K
h : D b = 0
⊢ ((b ^ 2)⁻¹ * b) • D a = (b⁻¹ * b⁻¹ * b) • D a

Tactic:
ring_nf

Goal state after:
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
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-(a ^ ↑(n.natAbs * 2))⁻¹ * ↑n.natAbs * a ^ ↑(n.natAbs - 1)) • D a =
    (-↑n.natAbs * (a ^ ↑(n.natAbs - 1) / a ^ ↑(n.natAbs * 2))) • D a

Tactic:
ring_nf

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
this : zpowers g = ⊥ ∨ zpowers g = ⊤
⊢ zpowers g = ⊤

Tactic:
zpowers_eq_bot,

Goal state after:
G : Type u_2
inst✝ : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
this : g = 1 ∨ zpowers g = ⊤
⊢ zpowers g = ⊤
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
inst✝ : Group α
a : α
⊢ (↑(zpowers a)).Finite ↔ IsOfFinOrder a

Tactic:
simp only [← orderOf_pos_iff, ← Nat.card_zpowers, Nat.card_pos_iff, ← SetLike.coe_sort_coe,
    nonempty_coe_sort, Nat.card_pos_iff, Set.finite_coe_iff, OneMemClass.coe_nonempty, true_and]

Goal state after:
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: G : Type u_3
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
⊢ g ^ k • Quotient.out q = g ^ (↑k).cast • Quotient.out q

Tactic:
ZMod.coe_intCast,

Goal state after:
G : Type u_3
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
⊢ g ^ k • Quotient.out q = g ^ (k % ↑(minimalPeriod (fun x ↦ g • x) (Quotient.out q))) • Quotient.out q