mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
⊢ IsPreirreducible s

Tactic:
rcases s.eq_empty_or_nonempty with he | hne

Goal state after:
case inl
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
he : s = ∅
⊢ IsPreirreducible s

case inr
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
hne : s.Nonempty
⊢ IsPreirreducible s
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_5
inst✝ : Finite ι
U : ι → Opens α
⊢ ↑(⨅ i, U i) = ⋂ i, ↑(U i)

Tactic:
induction ι using Finite.induction_empty_option with
  | of_equiv e ih => rw [← e.iInf_comp, ← e.surjective.iInter_comp, ih]
  | h_empty => simp
  | h_option ih => rw [iInf_option, Set.iInter_option, Opens.coe_inf, ih]

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
⊢ U ⇨ V = Opens.interior (↑U ⇨ ↑V)

Tactic:
ext x

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
x : α
⊢ x ∈ ↑(U ⇨ V) ↔ x ∈ ↑(Opens.interior (↑U ⇨ ↑V))
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s

Tactic:
by
  rw [NoetherianSpace, CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact,
    CompleteLattice.isSupFiniteCompact_iff_all_elements_compact]
  exact forall_congr' Opens.isCompactElement_iff

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case e'_5
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) → X := ⋯
this : IsEmbedding f'
hf' : range f' = f ⁻¹' ↑(U i)
e : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) ≃ₜ ↑(f ⁻¹' ↑(U i)) := ⋯
e_1✝ : ↑(f ⁻¹' (U i).carrier) = ↑(f ⁻¹' ↑(U i))
⊢ Subtype.val ∘ (U i).carrier.restrictPreimage f = ((f ∘ iV i) ∘ Subtype.val) ∘ ⇑e.symm

Tactic:
ext x

Goal state after:
case e'_5
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) → X := Subtype.val ∘ (f ⁻¹' ↑(U i)).restrictPreimage (iV i)
this : IsEmbedding f'
hf' : range f' = f ⁻¹' ↑(U i)
e : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) ≃ₜ ↑(f ⁻¹' ↑(U i)) := this.toHomeomorph.trans (Homeomorph.setCongr hf')
e_1✝ : ↑(f ⁻¹' (U i).carrier) = ↑(f ⁻¹' ↑(U i))
x : ↑(f ⁻¹' (U i).carrier)
⊢ (Subtype.val ∘ (U i).carrier.restrictPreimage f) x = (((f ∘ iV i) ∘ Subtype.val) ∘ ⇑e.symm) x
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), PrespectralSpace (X i)
U : Set ((i : ι) × X i)
hU : ∃ i, U ∈ (fun u ↦ Sigma.mk i '' u) '' {U | IsOpen[inst✝¹ i] U ∧ IsCompact U}
⊢ IsCompact U

Tactic:
obtain ⟨i, V, hV, rfl⟩ := hU

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), PrespectralSpace (X i)
i : ι
V : Set (X i)
hV : V ∈ {U | IsOpen[inst✝¹ i] U ∧ IsCompact U}
⊢ IsCompact ((fun u ↦ Sigma.mk i '' u) V)
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 | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}.Nonempty

Tactic:
by
        obtain ⟨w, h⟩ := inter_nonempty I J
        exact ⟨w, w, h.1, w, h.2, le_sup_left⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
h : Disjoint K L
⊢ Disjoint ↑K ↑L

Tactic:
Set.disjoint_iff

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
h : Disjoint K L
⊢ ↑K ∩ ↑L ⊆ ∅
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
⊢ genericPoints α = {genericPoint α}

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
x : α
⊢ x ∈ genericPoints α ↔ x ∈ {genericPoint α}
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set ↑↑(U i)
hVx : V ∈ 𝓝 ⟨x, hi⟩
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (V ↓∩ ↑(U i) ↓∩ s)
e : ↑V ≃ₜ ↑(Subtype.val '' V) := (Equiv.Set.image Subtype.val V ⋯).toHomeomorphOfIsInducing ⋯
⊢ IsConstructible ((Subtype.val '' V) ↓∩ s)

Tactic:
convert! hV'.preimage_of_isOpenEmbedding e.symm.isOpenEmbedding

Goal state after:
case e'_3
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set ↑↑(U i)
hVx : V ∈ 𝓝 ⟨x, hi⟩
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (V ↓∩ ↑(U i) ↓∩ s)
e : ↑V ≃ₜ ↑(Subtype.val '' V) := ⋯
e_1✝ : ↑(Subtype.val '' V) = ↑(Subtype.val '' V)
⊢ (Subtype.val '' V) ↓∩ s = ⇑e.symm ⁻¹' V ↓∩ ↑(U i) ↓∩ s
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_1
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
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
⊢ (Ideal.Quotient.mkₐ R I).comp (liftOfDerivationToSquareZero I hI d) = IsScalarTower.toAlgHom R A (B ⧸ I)

Tactic:
ext x

Goal state after:
case refine_1
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
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
x : A
⊢ ((Ideal.Quotient.mkₐ R I).comp (liftOfDerivationToSquareZero I hI d)) x = (IsScalarTower.toAlgHom R A (B ⧸ I)) x
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_2
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
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
⊢ (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ((fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) d) = d

Tactic:
ext x

Goal state after:
case refine_2
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
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
x : A
⊢ ↑(((fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ((fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) d)) x) =
    ↑(d x)
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_3
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
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
hf : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ (fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) ((fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ⟨f, hf⟩) =
    ⟨f, hf⟩

Tactic:
ext x

Goal state after:
case refine_3
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
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
hf : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x : A
⊢ ↑((fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) ((fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ⟨f, hf⟩)) x =
    ↑⟨f, hf⟩ x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ IsClosed (zeroLocus s)

Tactic:
by
  rw [isClosed_iff_zeroLocus]
  exact ⟨s, rfl⟩

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ b.factorization x

Tactic:
apply Finset.prod_dvd_prod_of_dvd

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) i ((a.lcm b).factorization i) ∣
      i ^ b.factorization i
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
hle : I ≤ nilradical R
⊢ Bijective (comap (Ideal.Quotient.mk I))

Tactic:
refine ⟨comap_injective_of_surjective _ Ideal.Quotient.mk_surjective, ?_⟩

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
hle : I ≤ nilradical R
⊢ Surjective (comap (Ideal.Quotient.mk I))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
p : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ p✝ ∈ Set.range (comap (RingHom.snd R S))

Tactic:
refine (hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim
    simpa [eq] using h (show (1, 0) ∈ RingHom.ker (RingHom.snd R S) by simp)

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
⊢ D (a / b) = b⁻¹ • D a

Tactic:
by
  simp only [leibniz_div, inv_pow, h, smul_zero, sub_zero, smul_smul]
  rw [← mul_self_mul_inv b⁻¹, inv_inv]
  ring_nf

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ {p | Disjoint ↑(Submonoid.powers r) ↑p.asIdeal} = ↑(basicOpen r)

Tactic:
ext x

Goal state after:
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ x ∈ {p | Disjoint ↑(Submonoid.powers r) ↑p.asIdeal} ↔ x ∈ ↑(basicOpen r)
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
hg : g ≠ 1
⊢ Submonoid.powers g = ⊤

Tactic:
ext x

Goal state after:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
x : G
⊢ x ∈ Submonoid.powers g ↔ x ∈ ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card ↥(zpowers a) = Nat.card G

Tactic:
card_eq_iff_eq_top,

Goal state after:
case e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ zpowers a = ⊤
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
⊢ orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

Tactic:
rw [orderOf_pow_orderOf_div]

Goal state after:
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf 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
⊢ (orderOf x).factorizationLCMLeft (orderOf y) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

pp: case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

pp: case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x

Tactic:
rw [orderOf_pow_orderOf_div]

Goal state after:
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
    (orderOf x).lcm (orderOf y)

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf y ≠ 0

case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf 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
⊢ (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))

Tactic:
rw [orderOf_pow_orderOf_div]

Goal state after:
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ ((orderOf x).factorizationLCMLeft (orderOf y)).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ vanishingIdeal (Set.range (comap f)) = (RingHom.ker f).radical

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x : R
⊢ x ∈ vanishingIdeal (Set.range (comap f)) ↔ x ∈ (RingHom.ker f).radical
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
⊢ ((orderOf x).factorizationLCMLeft (orderOf y)).gcd
      (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y)))) =
    1

pp: case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

pp: case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x

Tactic:
rw [orderOf_pow_orderOf_div]

Goal state after:
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ ((orderOf x).factorizationLCMLeft (orderOf y)).gcd ((orderOf x).factorizationLCMRight (orderOf y)) = 1

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf y ≠ 0

case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case refine_2
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
hG : (Nat.card G).primeFactors ⊆ p.primeFactors
⊢ ∃ n, Nat.card G ∣ p ^ n

Tactic:
refine ⟨Nat.card G, Nat.dvd_prod_primeFactors_pow_self NeZero.out |>.trans ?_⟩

Goal state after:
case refine_2
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
hG : (Nat.card G).primeFactors ⊆ p.primeFactors
⊢ (∏ p ∈ (Nat.card G).primeFactors, p) ^ Nat.card G ∣ p ^ Nat.card G
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)
inst✝ : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = p ^ k
hk0 : k = 0
⊢ False

Tactic:
rw [hk0, pow_zero] at hk

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = 1
hk0 : k = 0
⊢ False
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 α)
x : α
⊢ card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)

Tactic:
simp only [Quotient.eq'']; congr

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)

Tactic:
rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]

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
I : Ideal S
⊢ closure (comap f '' zeroLocus ↑I) = zeroLocus ↑(Ideal.comap f I)

Tactic:
apply subset_antisymm
  · rw [(isClosed_zeroLocus _).closure_subset_iff, Set.image_subset_iff, preimage_comap_zeroLocus]
    exact zeroLocus_anti_mono (Set.image_preimage_subset _ _)
  · rintro x (hx : I.comap f ≤ x.asIdeal)
    obtain ⟨q, hq₁, hq₂⟩ := Ideal.exists_minimalPrimes_le hx
    obtain ⟨p', hp', hp'', rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f _ hq₁
    let p'' : PrimeSpectrum S := ⟨p', hp'⟩
    apply isClosed_closure.stableUnderSpecialization ((le_iff_specializes
      (comap f ⟨p', hp'⟩) x).mp hq₂) (subset_closure (by exact ⟨_, hp'', rfl⟩))

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ 1 = (a * b) ^ 2

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p✝ : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p
⊢ ¬p ∣ H.index

Tactic:
← mul_dvd_mul_iff_left (Nat.card_pos (α := H)).ne',

Goal state after:
p✝ : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p
⊢ ¬Nat.card ↥H * p ∣ Nat.card ↥H * H.index
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
S : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module (ZMod n) M
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
hx : x ∈ K
c : ZMod n
⊢ c • x ∈ K

Tactic:
rw [← ZMod.intCast_zmod_cast c, Int.cast_smul_eq_zsmul]

Goal state after:
n : ℕ
M : Type u_1
S : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module (ZMod n) M
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
hx : x ∈ K
c : ZMod n
⊢ c.cast • x ∈ K
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
⊢ rank G = 0

Tactic:
by
  rw [← le_zero_iff, ← Finset.card_empty]
  exact rank_le (Subsingleton.elim _ _)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ∘ SetLike.coe '' vanishingIdeal '' irreducibleComponents (PrimeSpectrum R) =
    irreducibleComponents (PrimeSpectrum R)

Tactic:
← Set.image_comp,

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal '' irreducibleComponents (PrimeSpectrum R) =
    irreducibleComponents (PrimeSpectrum R)
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsAddTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ n • f = 0

Tactic:
by simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
⊢ Subgroup.comap f (torsion H) = torsion G

Tactic:
ext x

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
x : G
⊢ x ∈ Subgroup.comap f (torsion H) ↔ x ∈ torsion G
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ IsStronglyCoatomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]; infer_instance

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔ (insert a ↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤

Tactic:
Set.pairwise_insert_of_symm

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔
    ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this : Fintype G
⊢ ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥P) ≃* G

Tactic:
set ps := (Nat.card G).primeFactors

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
⊢ ((p : ↥ps) → (P : Sylow (↑p) G) → ↥P) ≃* G