mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case mk
P : Type u_1
inst✝ : LE P
t : Ideal P
toLowerSet✝ : LowerSet P
nonempty'✝ : toLowerSet✝.carrier.Nonempty
directed'✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) toLowerSet✝.carrier
x✝ : { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet = t.toLowerSet
⊢ { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ } = t

Tactic:
cases t

Goal state after:
case mk.mk
P : Type u_1
inst✝ : LE P
toLowerSet✝¹ : LowerSet P
nonempty'✝¹ : toLowerSet✝¹.carrier.Nonempty
directed'✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) toLowerSet✝¹.carrier
toLowerSet✝ : LowerSet P
nonempty'✝ : toLowerSet✝.carrier.Nonempty
directed'✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) toLowerSet✝.carrier
x✝ :
  { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ }.toLowerSet =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet
⊢ { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ } =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: 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
⊢ ?m.62

Tactic:
by
    refine hc.elim_finite_subcover (fun s : Us ↦ f '' s.1) (fun s ↦ h _ s.1.2) (fun x hx ↦ ?_)
    obtain ⟨x, rfl⟩ := hs hx
    obtain ⟨i, hi, hx⟩ := mem_sSup.mp <| by rwa [← heq]
    exact Set.mem_iUnion.mpr ⟨⟨i, hi⟩, x, hx, rfl⟩

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : Preorder P
inst✝ : OrderBot P
⊢ ∀ (a : Ideal P), principal ⊥ ≤ a

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x✝ : P
I✝ J✝ s t I J : Ideal P
x : P
hx : x ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
y : P
hy : y ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
⊢ (fun x1 x2 ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun x1 x2 ↦ x1 ≤ x2) y (x ⊔ y)

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ IsCompact ∅ ∧ IsOpen[inst✝¹] ∅ ∧ ∅ ⊆ ∅ ∧ ∅ ⊆ U

Tactic:
by simp

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : Compacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
h : { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isCompact' := isCompact'✝ } = t

Tactic:
cases t

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
h :
  { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier =
    { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
⊢ { carrier := carrier✝¹, isCompact' := isCompact'✝¹ } = { carrier := carrier✝, isCompact' := isCompact'✝ }
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
s : Set X
⊢ ∀ ⦃t : Set X⦄,
    (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ⊆ W ∧ W ⊆ U) →
      (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U) → ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ∪ t ⊆ W ∧ W ⊆ U

Tactic:
t

Goal state after:
case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
s t : Set X
⊢ (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ⊆ W ∧ W ⊆ U) →
    (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U) → ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ∪ t ⊆ W ∧ W ⊆ U
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₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
⊢ ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂

Tactic:
obtain ⟨x, hx⟩ := hU₁Z

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x : X
hx : x ∈ Z ∩ U₁
⊢ ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
⊢ Function.Injective (Compacts.map f hf) ↔ Function.Injective f

Tactic:
refine ⟨fun h => .of_comp (f := ({·} : β → Compacts β)) ?_, map_injective hf⟩
  simp_rw [Function.comp_def, ← map_singleton hf]
  exact h.comp singleton_injective

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
U : Opens α
h : U ∈ K.openRcNhds
x : ↥K
⊢ ↑x ∈ ↑K

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ i ∈ Finset.cons i s ih

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ i ∈ Finset.cons i s ih

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSober α
inst✝ : IrreducibleSpace α
x : α
⊢ x ∈ closure univ

Tactic:
by simp

Goal state after:
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:
by
    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.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ univ ∈ 𝓝 x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ IsOpen[inst✝] univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ IsRetrocompact (range Subtype.val)

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ s ⊆ range Subtype.val

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ i ∈ Finset.cons i s ih

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
p : PrimeSpectrum R
x✝ : R
⊢ (RingEquiv.ofBijective f hf) (((↑(RingEquiv.ofBijective f hf).symm).comp f) x✝) =
    (RingEquiv.ofBijective f hf) ((id R) x✝)

Tactic:
by simp

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

Goal state before:
pp: R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.Flat

Tactic:
rw [RingHom.Flat]

Goal state after:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ Module.Flat R S
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃*o H
⊢ ∀ {a b : Additive G}, (MulEquiv.toAdditive ↑e).toFun a ≤ (MulEquiv.toAdditive ↑e).toFun b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o Additive H
⊢ ∀ {a b : G}, (MulEquiv.toAdditive.symm ↑e).toFun a ≤ (MulEquiv.toAdditive.symm ↑e).toFun b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃+o H
⊢ ∀ {a b : Multiplicative G}, (AddEquiv.toMultiplicative ↑e).toFun a ≤ (AddEquiv.toMultiplicative ↑e).toFun b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o Multiplicative H
⊢ ∀ {a b : G}, (AddEquiv.toMultiplicative.symm ↑e).toFun a ≤ (AddEquiv.toMultiplicative.symm ↑e).toFun b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o H
⊢ ∀ {a b : G},
    (AddEquiv.toMultiplicativeRight e.toAddEquiv).toFun a ≤ (AddEquiv.toMultiplicativeRight e.toAddEquiv).toFun b ↔
      a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃*o Multiplicative H
⊢ ∀ {a b : Additive G},
    (MulEquiv.toAdditiveLeft e.toMulEquiv).toFun a ≤ (MulEquiv.toAdditiveLeft e.toMulEquiv).toFun b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃+o Additive H
⊢ ∀ {a b : Multiplicative G},
    (AddEquiv.toMultiplicativeLeft e.toAddEquiv).toFun a ≤ (AddEquiv.toMultiplicativeLeft e.toAddEquiv).toFun b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o H
⊢ ∀ {a b : G}, (MulEquiv.toAdditiveRight e.toMulEquiv).toFun a ≤ (MulEquiv.toAdditiveRight e.toMulEquiv).toFun b ↔ a ≤ b

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ zeroLocus Set.univ = ∅

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
⊢ ¬{ asIdeal := ⊥, isPrime := ⋯ }.asIdeal ≠ ⊥

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
← pow_succ',

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ a ^ (n - 1 + 1) = a ^ n
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1✝ D2✝ : Derivation R A M
r : R
a b : A
D1 D2 : Derivation R A M
⊢ (↑D1 + ↑D2) 1 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : R ≃+* S
x✝ : PrimeSpectrum R
⊢ comap ((↑e.symm).comp ↑e) x✝ = x✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : R ≃+* S
x✝ : PrimeSpectrum S
⊢ comap ((↑e).comp ↑e.symm) x✝ = x✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring A
inst✝⁹ : CommSemiring B
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Module A M
inst✝⁴ : Module B M
inst✝³ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M
d : Derivation R B M
⊢ (↑d ∘ₗ (IsScalarTower.toAlgHom R A B).toLinearMap) 1 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring A
inst✝⁹ : CommSemiring B
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Module A M
inst✝⁴ : Module B M
inst✝³ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ : A
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M
d : Derivation R B M
a b : A
⊢ (↑d ∘ₗ (IsScalarTower.toAlgHom R A B).toLinearMap) (a * b) =
    a • (↑d ∘ₗ (IsScalarTower.toAlgHom R A B).toLinearMap) b + b • (↑d ∘ₗ (IsScalarTower.toAlgHom R A B).toLinearMap) a

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ ↑(basicOpen 1) = ↑⊤

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ ↑(basicOpen 0) = ↑⊥

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
hf : Function.Surjective ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ (liftOfSurjective hf hd) (f x) = f (d x)

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
⊢ exponent G = sInf {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
· have : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅ :=
      Set.eq_empty_of_forall_notMem fun n hn ↦ h ⟨n, hn⟩
    rw [Monoid.exponent_eq_zero_iff.mpr h, this, Nat.sInf_empty]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ g' ∈ zpowers g

Tactic:
by
  simp_rw [zpowers_eq_top_of_prime_card h hg, Subgroup.mem_top]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ (-↑n)) ≤ zpowers g
⊢ zpowers (g ^ (-↑n)) = zpowers (g ^ n)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ StableUnderGeneralization {x} ↔ IsMin x

Tactic:
StableUnderGeneralization,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃x_1 y : PrimeSpectrum R⦄, y ⤳ x_1 → x_1 ∈ {x} → y ∈ {x}) ↔ IsMin x
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : orderOf y = 0
⊢ x ∈ {x, y}

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : ¬orderOf y = 0
⊢ x ∈ {x, y}

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ y ∈ {x, y}

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ x ∈ {x, y}

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ y ∈ {x, y}

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
⊢ exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p

Tactic:
refine ⟨fun hG g hg ↦ ?_, fun h ↦ dvd_antisymm ?_ ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : g ≠ 1
⊢ orderOf g = p

case refine_2
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ exponent G ∣ p

case refine_3
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ p ∣ exponent G
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
⊢ ∃ g, orderOf g = exponent G

Tactic:
obtain ⟨t, ht⟩ := hne.csSup_mem hfin

Goal state after:
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ ∃ g, orderOf g = exponent G
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup 0 G
⊢ Nat.card G ∣ 0 ^ 1

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
⊢ Nat.card G = p ^ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ g ^ 0 ^ 1 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ g ^ Nat.card G ^ 1 = 1

Tactic:
by simp

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 α)
⊢ ∑ _a, 1 = card ↑(fixedPoints G α)

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ 1 ∈ Finset.image orderOf Finset.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ : ℕ
⊢ (p₁ ^ n₁).Coprime (Nat.card ↥H₂)

Tactic:
obtain ⟨n₂, heq₂⟩ := iff_card.mp hH₂

Goal state after:
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ n₂ : ℕ
heq₂ : Nat.card ↥H₂ = p₂ ^ n₂
⊢ (p₁ ^ n₁).Coprime (Nat.card ↥H₂)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
hs : s.Finite
⊢ (zeroLocus ↑hs.toFinset)ᶜ = (zeroLocus s)ᶜ

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
⊢ IsIntegral R r

Tactic:
have : (1 : R[X]) ∈ Ideal.span {X} ⊔ (Ideal.span {p}).comap (mapRingHom f) := by
    have H := h _ (isClosed_zeroLocus {p})
    rw [← zeroLocus_span, ← closure_eq_iff_isClosed, closure_image_comap_zeroLocus] at H
    rw [← Ideal.eq_top_iff_one, sup_comm, ← zeroLocus_empty_iff_eq_top, zeroLocus_sup, H]
    suffices ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal by
      simpa [Set.eq_empty_iff_forall_notMem]
    intro q hpq hXq
    have : 1 ∈ q.asIdeal := by simpa [p] using! (sub_mem (q.asIdeal.mul_mem_left (C r) hXq) hpq)
    exact q.2.ne_top (q.asIdeal.eq_top_iff_one.mpr this)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
⊢ IsIntegral R r
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
⊢ (X ^ (1 + c.natDegree)).Monic

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ (X ^ 0).natDegree ≤ 1 + c.natDegree

Tactic:
by simp

Goal state after: