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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : ↑(f ⁻¹' s)
y : ↑s
h : y ⤳ s.restrictPreimage f x
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y

Tactic:
obtain ⟨a, ha, hy⟩ := H (h.map <| continuous_subtype_val (p := (· ∈ s)))

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : ↑(f ⁻¹' s)
y : ↑s
h : y ⤳ s.restrictPreimage f x
a : α
ha : a ⤳ ↑x
hy : f a = ↑y
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case mpr
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ (∀ (i : ι), IsOpen[inst✝] (s ∩ ↑(U i))) → IsOpen[inst✝] s

Tactic:
intro H

Goal state after:
case mpr
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpen[inst✝] (s ∩ ↑(U i))
⊢ IsOpen[inst✝] s
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ [IsLocallyClosed s, IsOpen[inst✝] (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)].TFAE

Tactic:
tfae_have 1 → 2 := by
    rintro ⟨U, Z, hU, hZ, rfl⟩
    have : Z ∪ (frontier (U ∩ Z))ᶜ = univ := by
      nth_rw 1 [← hZ.closure_eq]
      rw [← compl_subset_iff_union, compl_subset_compl]
      refine frontier_subset_closure.trans (closure_mono inter_subset_right)
    rw [coborder_eq_union_frontier_compl, inter_union_distrib_right, this,
      inter_univ]
    exact hU.union isClosed_frontier.isOpen_compl

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
⊢ [IsLocallyClosed s, IsOpen[inst✝] (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)].TFAE
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
⊢ (∀ (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:
intro H

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

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

Tactic:
intro H

Goal state after:
case mpr
α : 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 : ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))
⊢ ∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst✝¹] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
⊢ (⋃₀ (irreducibleComponents α \ {Z}))ᶜ.Nonempty

Tactic:
· contrapose! hZ
    rw [hZ, closure_empty, ← Set.nonempty_iff_empty_ne]
    exact H.1.nonempty

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
⊢ IsQuasiSeparated (f '' s) → IsQuasiSeparated s

Tactic:
intro H

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
⊢ IsQuasiSeparated s
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 Y
f : X → Y
hf : IsInducing f
hf' : IsSpectralMap f
⊢ ∀ (U : Set X) (x : Set Y), IsOpen[inst✝¹] x → IsCompact x → f ⁻¹' x = U → IsCompact U

Tactic:
rintro _ U h₁ h₂ rfl

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace Y
f : X → Y
hf : IsInducing f
hf' : IsSpectralMap f
U : Set Y
h₁ : IsOpen[inst✝¹] U
h₂ : IsCompact U
⊢ IsCompact (f ⁻¹' U)
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
U V : Opens X
⊢ (∀ (W : CompactOpens X), ↑W ⊆ ↑U → ↑W ⊆ ↑V) → U ≤ V

Tactic:
intro H

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U V : Opens X
H : ∀ (W : CompactOpens X), ↑W ⊆ ↑U → ↑W ⊆ ↑V
⊢ U ≤ V
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S U : Set α
h : IsGenericPoint x S
hU : IsOpen U
⊢ Disjoint S U ↔ x ∉ U

Tactic:
by
  rw [h.mem_open_set_iff hU, ← not_disjoint_iff_nonempty_inter, Classical.not_not]

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ IsGenericPoint hS.genericPoint S

Tactic:
convert! hS.isGenericPoint_genericPoint_closure; exact hS'.closure_eq.symm

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₂
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
refine ⟨W₁ᶜ, W₂ᶜ, by simpa using hW₁.1.1, by simpa using hW₂.1.1, by simp [hW₁.1.2],
    by simp [hW₂.1.2], fun z hz ↦ ?_, ⟨x₁, by grind⟩, ⟨x₂, by grind⟩⟩

Goal state after:
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₂
z : X
hz : z ∈ Z
⊢ z ∈ W₁ᶜ ∪ W₂ᶜ
Module: Mathlib.Topology.Sober

Goal state before:
pp: case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : R1Space α
S✝ : Set α
h : IsIrreducible S✝
hs : IsClosed S✝
x : α
hx : x ∈ S✝
⊢ closure {x} ⊆ S✝

Tactic:
← hs.closure_eq

Goal state after:
case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : R1Space α
S✝ : Set α
h : IsIrreducible S✝
hs : IsClosed S✝
x : α
hx : x ∈ S✝
⊢ closure {x} ⊆ closure S✝
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case isSublattice
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
⊢ IsSublattice {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}

Tactic:
| isSublattice =>

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

Goal state before:
pp: R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ (algebraMap R S).Flat

Tactic:
exact flat_algebraMap_iff.mpr (IsLocalization.flat _ (Submonoid.powers r))

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

Goal state before:
pp: case e'_5
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
a✝ : ↑s
e_4✝ : OreLocalization.instAddCommMonoidOreLocalization = CommRing.toCommSemiring.toAddCommMonoid
x✝¹ : R
x✝ : OreLocalization (Submonoid.powers ↑a✝) S
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝

Tactic:
apply Algebra.smul_def

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

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ zeroLocus ↑x.asIdeal ⊆ {x} → x.asIdeal.IsMaximal

Tactic:
intro H

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
⊢ x.asIdeal.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ x.asIdeal.IsMaximal → zeroLocus ↑x.asIdeal ⊆ {x}

Tactic:
intro H

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : x.asIdeal.IsMaximal
⊢ zeroLocus ↑x.asIdeal ⊆ {x}
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsClosed {x} ↔ x.asIdeal.IsMaximal

Tactic:
by
  rw [← closure_subset_iff_isClosed, ← zeroLocus_vanishingIdeal_eq_closure,
      vanishingIdeal_singleton]
  constructor <;> intro H
  · rcases x.asIdeal.exists_le_maximal x.2.1 with ⟨m, hm, hxm⟩
    exact (congr_arg asIdeal (@H ⟨m, hm.isPrime⟩ hxm)) ▸ hm
  · exact fun p hp ↦ PrimeSpectrum.ext (H.eq_of_le p.2.1 hp).symm

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
inst✝ : IsDomain R
⊢ IrreducibleSpace (PrimeSpectrum R)

Tactic:
simpa [irreducibleSpace_iff_isPrime_nilradical] using Ideal.isPrime_bot

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✝
ι✝ : Type u
S : ι✝ → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι✝), IsClosed (S i)
S_empty : ⋂ i, S i = ∅
⊢ ∃ u, ⋂ i ∈ u, S i = ∅

Tactic:
choose I hI using fun i ↦ (isClosed_iff_zeroLocus_ideal (S i)).mp (S_closed i)

Goal state after:
R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
ι✝ : Type u
S : ι✝ → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι✝), IsClosed (S i)
S_empty : ⋂ i, S i = ∅
I : ι✝ → Ideal R
hI : ∀ (i : ι✝), S i = zeroLocus ↑(I i)
⊢ ∃ u, ⋂ i ∈ u, S i = ∅
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
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : R
y : M
⊢ f (d (f_inv (x • y))) = (RingHom.id R) x • f (d (f_inv y))

Tactic:
suffices f (d (f_inv (x • y) - x • f_inv y)) = 0 by simpa [sub_eq_zero]

Goal state after:
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
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : R
y : M
⊢ f (d (f_inv (x • y) - x • f_inv y)) = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case h_nhds
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
hp : p ∈ Uᶜᶜ
s : Set R
hs : zeroLocus s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), p ∈ v ∧ v ⊆ U

Tactic:
Set.mem_compl_iff,

Goal state after:
case h_nhds
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
hp : p ∉ Uᶜ
s : Set R
hs : zeroLocus s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), p ∈ v ∧ v ⊆ U
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ IsCyclic α ↔ ∃ g, Nat.card α ≤ orderOf g

Tactic:
by
  rw [isCyclic_iff_exists_orderOf_eq_natCard]
  apply exists_congr
  intro g
  exact ⟨Eq.ge, le_antisymm orderOf_le_card⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ False

Tactic:
have h₃ : exponent G ≤ n % exponent G := by
      apply exponent_min' _ h
      simp_rw [← pow_eq_mod_exponent]
      exact hG

Goal state after:
case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
h₃ : exponent G ≤ n % exponent G
⊢ False
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: G : Type u_3
inst✝² : Group G
H : Subgroup G
g : G
inst✝¹ : Finite (G ⧸ H)
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this✝ : Fintype (G ⧸ H)
this : (q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))) → Fintype ↑(orbit (↥(zpowers g)) q.out)
⊢ Fintype.card (G ⧸ H) = ∑ x, Fintype.card ↑(orbit (↥(zpowers g)) x.out)

Tactic:
rw [← Fintype.card_sigma]

Goal state after:
G : Type u_3
inst✝² : Group G
H : Subgroup G
g : G
inst✝¹ : Finite (G ⧸ H)
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this✝ : Fintype (G ⧸ H)
this : (q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))) → Fintype ↑(orbit (↥(zpowers g)) q.out)
⊢ Fintype.card (G ⧸ H) = Fintype.card ((x : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))) × ↑(orbit (↥(zpowers g)) x.out))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x y : PrimeSpectrum R
h : x ⤳ y
⊢ ∀ (y_1 : ↥y.asIdeal.primeCompl), IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑y_1)

Tactic:
rintro ⟨a, ha⟩

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x y : PrimeSpectrum R
h : x ⤳ y
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑⟨a, ha⟩)
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
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
⊢ StableUnderSpecialization s

Tactic:
← stableUnderGeneralization_compl_iff

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
⊢ StableUnderGeneralization sᶜ
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ DenseRange (comap f) → ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)

Tactic:
intro H

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
H : DenseRange (comap f)
⊢ ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)) →
    DenseRange (comap f)

Tactic:
intro H

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
H : ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)
⊢ DenseRange (comap f)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite

Tactic:
have := exponent_ne_zero_iff_range_orderOf_finite h

Goal state after:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ (Set.range orderOf).Finite
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
H : Type u_1
inst✝ : Monoid H
e : G →* H
e_inj : Function.Injective ⇑e
g : G
⊢ e (g ^ exponent H) = e 1

Tactic:
map_pow,

Goal state after:
G : Type u
inst✝¹ : Monoid G
H : Type u_1
inst✝ : Monoid H
e : G →* H
e_inj : Function.Injective ⇑e
g : G
⊢ e g ^ exponent H = e 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : ↑a.val = ↑b.val
⊢ a = b

Tactic:
simpa [ZMod.natCast_val, ZMod.cast_id'] using h

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ e * f = 0 ∧ f + e = 1 ∧ s = ↑(basicOpen f) ↔ e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}

Tactic:
add_comm,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen f) ↔ e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod n) G
⊢ IsPGroup n (Multiplicative G)

Tactic:
simpa [IsPGroup, Multiplicative.forall] using
    fun _ ↦ ⟨1, by simp [← ofAdd_nsmul, ZModModule.char_nsmul_eq_zero]⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
⊢ ∑ m ∈ c.divisors, #{a | orderOf a = m} = ∑ m ∈ c.divisors.erase d, #{a | orderOf a = m}

Tactic:
eq_comm

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
⊢ ∑ m ∈ c.divisors.erase d, #{a | orderOf a = m} = ∑ m ∈ c.divisors, #{a | orderOf a = m}
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ Nat.card ↑(orbit G P)
⊢ Nat.card ↑{⟨P, ⋯⟩} = Nat.card ↑(fixedPoints ↥↑P ↑(orbit G P))

Tactic:
eq_comm

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ Nat.card ↑(orbit G P)
⊢ Nat.card ↑(fixedPoints ↥↑P ↑(orbit G P)) = Nat.card ↑{⟨P, ⋯⟩}
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
x✝ : ℤ
⊢ (∃ c, x✝ = ↑(addOrderOf g) * c) ↔ ∃ k, ↑(addOrderOf g) * k = x✝

Tactic:
eq_comm

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case h
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
hQ : ¬p ∣ Q.index
⊢ map f ↑(hpQ.toSylow hQ) = ↑P

Tactic:
eq_comm

Goal state after:
case h
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
hQ : ¬p ∣ Q.index
⊢ ↑P = map f ↑(hpQ.toSylow hQ)
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ Finset.univ ↔ a✝ ∈ {⊤, ⊥}

Tactic:
simpa using (eq_bot_or_eq_top _).symm

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

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ (monoidHomOfForallMemZpowers hg hg') g = g'

Tactic:
by
  simp only [monoidHomOfForallMemZpowers, MonoidHom.coe_mk, OneHom.coe_mk]
  nth_rw 2 [← zpow_one g']
  rw [zpow_eq_zpow_iff_modEq]
  apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')
  rw [← zpow_eq_zpow_iff_modEq, zpow_one]
  exact Classical.choose_spec <| mem_zpowers_iff.mp <| hg g

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : 0 = Nat.card (↥(normalizer ↑H) ⧸ comap (normalizer ↑H).subtype H) % p
⊢ Nat.card (↥(normalizer ↑H) ⧸ comap (normalizer ↑H).subtype H) % p = 0

Tactic:
eq_comm

Goal state after:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : Nat.card (↥(normalizer ↑H) ⧸ comap (normalizer ↑H).subtype H) % p = 0
⊢ Nat.card (↥(normalizer ↑H) ⧸ comap (normalizer ↑H).subtype H) % p = 0
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : 0 = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
⊢ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p = 0

Tactic:
eq_comm

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p = 0
⊢ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p = 0