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

Goal state before:
pp: 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 : ι
⊢ IsEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
let f' := (Subtype.val ∘ (f ⁻¹' U i).restrictPreimage (iV i))

Goal state after:
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)
⊢ IsEmbedding ((U i).carrier.restrictPreimage f)
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₂
⊢ IsClosed[inst✝¹] W₁ᶜ

Tactic:
simpa using hW₁.1.1

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
⊢ { carrier := closure[inst✝] ↑U, isCompact' := ⋯ } ∈ K.compactNhds

Tactic:
by
  intro x
  have H : (U : Set α) ∈ 𝓝 (x : α) :=
    U.isOpen.mem_nhds <| Compacts.subset_of_mem_openRcNhds h (by simp)
  exact Filter.mem_of_superset H subset_closure

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : NonemptyCompacts α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ s = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := s

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : NonemptyCompacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier.Nonempty
h :
  (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ } =
    (fun s ↦ s.carrier) t
⊢ { carrier := carrier✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ } = t
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : NonemptyCompacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier.Nonempty
h :
  (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ } =
    (fun s ↦ s.carrier) t
⊢ { carrier := carrier✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ } = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := t

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
nonempty'✝¹ : { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier.Nonempty
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier.Nonempty
h :
  (fun s ↦ s.carrier) { carrier := carrier✝¹, isCompact' := isCompact'✝¹, nonempty' := nonempty'✝¹ } =
    (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ }
⊢ { carrier := carrier✝¹, isCompact' := isCompact'✝¹, nonempty' := nonempty'✝¹ } =
    { carrier := carrier✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ }
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : PositiveCompacts α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ s = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := s

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : PositiveCompacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
interior_nonempty'✝ : (interior { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier).Nonempty
h :
  (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, interior_nonempty' := interior_nonempty'✝ } =
    (fun s ↦ s.carrier) t
⊢ { carrier := carrier✝, isCompact' := isCompact'✝, interior_nonempty' := interior_nonempty'✝ } = t
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : PositiveCompacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
interior_nonempty'✝ : (interior { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier).Nonempty
h :
  (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, interior_nonempty' := interior_nonempty'✝ } =
    (fun s ↦ s.carrier) t
⊢ { carrier := carrier✝, isCompact' := isCompact'✝, interior_nonempty' := interior_nonempty'✝ } = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := t

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
interior_nonempty'✝¹ : (interior { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier).Nonempty
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
interior_nonempty'✝ : (interior { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier).Nonempty
h :
  (fun s ↦ s.carrier) { carrier := carrier✝¹, isCompact' := isCompact'✝¹, interior_nonempty' := interior_nonempty'✝¹ } =
    (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, interior_nonempty' := interior_nonempty'✝ }
⊢ { carrier := carrier✝¹, isCompact' := isCompact'✝¹, interior_nonempty' := interior_nonempty'✝¹ } =
    { carrier := carrier✝, isCompact' := isCompact'✝, interior_nonempty' := interior_nonempty'✝ }
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : CompactOpens α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ s = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := s

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : CompactOpens α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
isOpen'✝ : IsOpen { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h : (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, isOpen' := isOpen'✝ } = (fun s ↦ s.carrier) t
⊢ { carrier := carrier✝, isCompact' := isCompact'✝, isOpen' := isOpen'✝ } = t
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : CompactOpens α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
isOpen'✝ : IsOpen { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h : (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, isOpen' := isOpen'✝ } = (fun s ↦ s.carrier) t
⊢ { carrier := carrier✝, isCompact' := isCompact'✝, isOpen' := isOpen'✝ } = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := t

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
isOpen'✝¹ : IsOpen { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
isOpen'✝ : IsOpen { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h :
  (fun s ↦ s.carrier) { carrier := carrier✝¹, isCompact' := isCompact'✝¹, isOpen' := isOpen'✝¹ } =
    (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, isOpen' := isOpen'✝ }
⊢ { carrier := carrier✝¹, isCompact' := isCompact'✝¹, isOpen' := isOpen'✝¹ } =
    { carrier := carrier✝, isCompact' := isCompact'✝, isOpen' := isOpen'✝ }
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case neg
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
hle : p ≤ q
h : ¬p = q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
have := Q.over_def q
    subst this
    exact Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt Q (lt_of_le_of_ne hle h)

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
this : Semifield R := h.toSemifield
⊢ x.asIdeal.IsMaximal

Tactic:
exact hx.symm ▸ Ideal.bot_isMaximal

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
⊢ D a⁻¹ = -a⁻¹ ^ 2 • D a

Tactic:
by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp
  · exact D.leibniz_of_mul_eq_one (inv_mul_cancel₀ ha)

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

Goal state before:
pp: case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit (↥(zpowers a)) b)
val✝ : Fintype ↑(orbit (↥(zpowers a)) b)
⊢ minimalPeriod (fun x ↦ a • x) b ≠ 0

Tactic:
have : Nonempty (orbit (zpowers a) b) := (nonempty_orbit b).to_subtype

Goal state after:
case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit (↥(zpowers a)) b)
val✝ : Fintype ↑(orbit (↥(zpowers a)) b)
this : Nonempty ↑(orbit (↥(zpowers a)) b)
⊢ minimalPeriod (fun x ↦ a • x) b ≠ 0
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ orderOf (g ^ k) = p ^ (exponent G).factorization p

Tactic:
rw [ht]

Goal state after:
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ orderOf (g ^ k) = p ^ t.succ
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_1.inl
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ ↑n) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ ↑n) = zpowers (g ^ n_1)

pp: case refine_1.inr
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ (-↑n)) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ (-↑n)) = zpowers (g ^ n_1)

Tactic:
· exact ⟨n, by rw [zpow_natCast]⟩

Goal state after:
case refine_1.inr
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ (-↑n)) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ (-↑n)) = zpowers (g ^ n_1)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
· exact ⟨_, mul_mem (pow_mem (subset_closure (by simp)) _) (pow_mem (subset_closure (by simp)) _),
      h.orderOf_mul_pow_eq_lcm hx hy⟩

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

Goal state before:
pp: α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i ↦ a ^ i) (range (orderOf a)) = univ

Tactic:
simp only [_root_.image_range_orderOf, Set.eq_univ_iff_forall.mpr ha, Set.toFinset_univ]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

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

Tactic:
← Nat.card_zpowers

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ (hG.powEquiv hn).symm g = g ^ (Nat.card ↥(Subgroup.zpowers g)).gcdB n
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
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)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf t / p ^ (orderOf t).factorization p * p ^ (orderOf t).factorization p * p ^ a * p

Tactic:
Nat.div_mul_cancel,

Goal state after:
case h
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)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf t * p ^ a * p

case h
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)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ p ^ (orderOf t).factorization p ∣ orderOf t
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
P : Subgroup G
hP1 : IsPGroup p ↥P
hP2 : ¬p ∣ P.index
⊢ ∀ {Q : Subgroup G}, IsPGroup p ↥Q → P ≤ Q → Q = P

Tactic:
intro Q

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
P : Subgroup G
hP1 : IsPGroup p ↥P
hP2 : ¬p ∣ P.index
Q : Subgroup G
⊢ IsPGroup p ↥Q → P ≤ Q → Q = P
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank H ≤ rank G

Tactic:
trans (S.image f).card

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank H ≤ (Finset.image (⇑f) S).card

G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ (Finset.image (⇑f) S).card ≤ rank G
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U ↔ U = ⊤

Tactic:
constructor
  · rw [eq_top_iff]
    exact fun h x _ => (specializes_closedPoint x).mem_open U.2 h
  · rintro rfl
    exact TopologicalSpace.Opens.mem_top _

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ IsClosed {closedPoint R}

Tactic:
rw [PrimeSpectrum.isClosed_singleton_iff_isMaximal, closedPoint]
  infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
⊢ exponent α = Nat.card α

Tactic:
by
  obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := α)
  apply Nat.dvd_antisymm Group.exponent_dvd_nat_card
  rw [← hg]
  exact order_dvd_exponent _

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: 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
⊢ ¬p ∣ (↑Q₀).index * (↑P).index

Tactic:
exact Nat.Prime.not_dvd_mul Fact.out Q₀.not_dvd_index P.not_dvd_index

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
g : G ⧸ (powMonoidHom n).range
a : G
⊢ ↑(a ^ n) = 1

Tactic:
QuotientGroup.eq_one_iff

Goal state after:
G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
g : G ⧸ (powMonoidHom n).range
a : G
⊢ a ^ n ∈ (powMonoidHom n).range
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr.inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Infinite ↥f.range
⊢ IsCyclic M

Tactic:
rw [Nat.card_eq_zero_of_infinite (α := f.range), Nat.coprime_zero_right] at h

Goal state after:
case inr.inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : Nat.card ↥f.ker = 1
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Infinite ↥f.range
⊢ IsCyclic M
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 : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
hy : y ∈ H
⊢ ↑⟨y, ⋯⟩ = 1

Tactic:
QuotientGroup.eq_one_iff

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 : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
hy : y ∈ H
⊢ ⟨y, ⋯⟩ ∈ H.subgroupOf (normalizer ↑H)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2.left
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 : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
hne' : p₁ ≠ p₂
⊢ (Fintype.card ↥↑(P ↑⟨p₁, hp₁⟩)).Coprime (Fintype.card ↥↑(P ↑⟨p₂, hp₂⟩))

Tactic:
simp only [← Nat.card_eq_fintype_card]

Goal state after:
case refine_2.left
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 : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
hne' : p₁ ≠ p₂
⊢ (Nat.card ↥↑(P p₁)).Coprime (Nat.card ↥↑(P p₂))
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxy : x ≠ y
hxb : IsMaximal x (x ⊔ y)
hyb : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y

Tactic:
exact isMaximal_inf_right_of_isMaximal_sup hxb hyb

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2.right
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 ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Fintype.card ((i : ↥ps) → ↥↑(P ↑i)) = Fintype.card G

Tactic:
simp only [← Nat.card_eq_fintype_card]

Goal state after:
case refine_2.right
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 : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Nat.card ((i : ↥ps) → ↥↑(P ↑i)) = Nat.card G
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ (fun i ↦ torsionBySet R M ↑(p i)) i ⊓ ⨆ a ∈ T, torsionBySet R M ↑(p a) = ⊥

Tactic:
iSup_torsionBySet_ideal_eq_torsionBySet_iInf fun i hi j hj ij => hp (hT hi) (hT hj) ij

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ (fun i ↦ torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i) = ⊥
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose
⊢ I • F.N n = F.N (n + 1)

Tactic:
h.choose_spec n hn,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose
⊢ I • I ^ (n - h.choose) • F.N h.choose = F.N (n + 1)