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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s ∩ closure[inst✝] s = s

Tactic:
rw [coborder, ← sdiff_eq_compl_inter, sdiff_sdiff_right_self, inter_eq_right]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ closure[inst✝] s
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
⊢ ∀ (x : ↑(f ⁻¹' s)), 𝓝 x = comap ((f ⁻¹' s).domRestrict f) (𝓝 ((f ⁻¹' s).domRestrict f x))

Tactic:
domRestrict_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
⊢ ∀ (x : ↑(f ⁻¹' s)), 𝓝 x = comap (f ∘ Subtype.val) (𝓝 ((f ∘ Subtype.val) x))
Module: Mathlib.Topology.LocalAtTarget

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

Tactic:
domRestrict_eq,

Goal state after:
α : 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 (f ∘ Subtype.val) (𝓝 ((f ∘ Subtype.val) x))
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
⊢ IsCompact s

Tactic:
refine isCompact_iff_finite_subcover.2 fun U hUo hs => ?_
  rcases ((noetherianSpace_iff_opens α).mp ‹_› ⟨⋃ i, U i, isOpen_iUnion hUo⟩).elim_finite_subcover U
    hUo Set.Subset.rfl with ⟨t, ht⟩
  exact ⟨t, hs.trans ht⟩

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ s = s ⊓ z₁ ⊔ sSup S₂

Tactic:
← h₂,

Goal state after:
case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ s = s ⊓ z₁ ⊔ s ⊓ z₂
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
x : α
hx : x ∈ closure s
⊢ p x hx

Tactic:
obtain ⟨t, rfl⟩ := (mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mp hx

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
hx : (t.sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s
⊢ p (t.sup fun x ↦ ↑x.1 \ ↑x.2) hx
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 : (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = ∅
⊢ closure[inst✝¹] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ ≠ Z

Tactic:
rw [hZ, closure_empty, ← Set.nonempty_iff_empty_ne]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = ∅
⊢ Z.Nonempty
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' V)

Tactic:
· rw [h.isCompact_iff]
    convert! hV''
    rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
    exact hV.trans (Set.image_subset_range _ _)

Goal state after:
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
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
⊢ U ∈ ↑{ carrier := {V | ↑V ⊆ ↑(⨆ U ∈ I, U.toOpens)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ } ↔ U ∈ ↑I

Tactic:
change U.toOpens ≤ _ ↔ _

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
⊢ U.toOpens ≤ ⨆ U ∈ I, U.toOpens ↔ U ∈ ↑I
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Z Y : IrreducibleCloseds X
h : Z ≤ Y
x : X
hx : x ∈ Y
z : X
hz : z ∈ Z.carrier
⊢ x ∈ Z

Tactic:
rwa [DiscreteTopology.isDiscrete.subsingleton_of_isPreirreducible Y.2.isPreirreducible hx (h hz)]

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : QuasiSober Y
inst✝² : T0Space Y
inst✝¹ : QuasiSober X
inst✝ : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ coheight (irreducibleSetEquivPoints.symm (f x)) = coheight x

Tactic:
← coheight_orderIso (irreducibleSetEquivPoints (α := X)).symm x,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : QuasiSober Y
inst✝² : T0Space Y
inst✝¹ : QuasiSober X
inst✝ : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ coheight (irreducibleSetEquivPoints.symm (f x)) = coheight (irreducibleSetEquivPoints.symm x)
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:
rw [← hs.closure_eq]
      exact closure_mono (singleton_subset_iff.mpr hx)

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
⊢ IsConstructible ((inclusion ⋯ ⁻¹' U ↓∩ s) ∩ inclusion ⋯ ⁻¹' V ↓∩ t)

Tactic:
exact .inter (hsU.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)
    (htV.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
⊢ T1Space (PrimeSpectrum R)

Tactic:
refine ⟨fun x => (isClosed_singleton_iff_isMaximal x).2 ?_⟩
    by_cases hx : x.asIdeal = ⊥
    · let := h.toSemifield
      exact hx.symm ▸ Ideal.bot_isMaximal
    · exact absurd h (Ring.not_isField_iff_exists_prime.2 ⟨x.asIdeal, ⟨hx, x.2⟩⟩)

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ (g ^ if h : ExponentExists G then Nat.find h else 0) = 1

Tactic:
dif_pos h

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find h = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ g, zpowers g = ⊤) ↔ ∃ g, zpowers g = H

Tactic:
← map_subtype_inj,

Goal state after:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ g, map H.subtype (zpowers g) = map H.subtype ⊤) ↔ ∃ g, zpowers g = H
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
⊢ sigmaToPi R '' Sigma.mk i '' ↑(basicOpen f) = ↑(basicOpen (Pi.single i f))

Tactic:
by
  simp only [Set.image_image, sigmaToPi_apply]
  exact PrimeSpectrum.comap_evalRingHom_basicOpen _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α ∣ p
⊢ IsCyclic α

Tactic:
by
  rcases (Nat.dvd_prime hp.out).mp h with h | h
  · exact @isCyclic_of_subsingleton α _ (Nat.card_eq_one_iff_unique.mp h).1
  · exact isCyclic_of_prime_card h

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
⊢ ∃ g, orderOf g = exponent G

Tactic:
have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩

Goal state after:
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
⊢ ∃ g, orderOf g = exponent G
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
⊢ a = b

Tactic:
by
  obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
  specialize h g
  subst hGcard
  rw [pow_eq_pow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers hg,
    ← ZMod.natCast_eq_natCast_iff] at h
  simpa [ZMod.natCast_val, ZMod.cast_id'] using h

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
hp : p ≠ 0
q : ℕ
hq : q ∈ (Nat.card G).primeFactors
hqp : Nat.Prime q
hqdvd : q ∣ Nat.card G
right✝ : Nat.card G ≠ 0
g : G
hg : orderOf g = q
⊢ q ∈ p.primeFactors

Tactic:
have ⟨k, hk⟩ := h.exists_orderOf_dvd_pow g

Goal state after:
case inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
hp : p ≠ 0
q : ℕ
hq : q ∈ (Nat.card G).primeFactors
hqp : Nat.Prime q
hqdvd : q ∣ Nat.card G
right✝ : Nat.card G ≠ 0
g : G
hg : orderOf g = q
k : ℕ
hk : orderOf g ∣ p ^ k
⊢ q ∈ p.primeFactors
Module: Mathlib.GroupTheory.PGroup

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

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:
· rcases eq_or_ne n 0 with (rfl | hn0)
    · simp_all
    grw [← Nat.primeFactors_pow p hn0, Nat.primeFactors_mono hn <| pow_ne_zero n h]

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
⊢ ∃ n, Nat.card G ∣ p ^ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Infinite G
⊢ 0 = 1 ∨ p ∣ 0

Tactic:
exact Or.inr ⟨0, rfl⟩

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

Goal state before:
pp: case right
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ (fun x ↦ x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)

pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ Ideal.span (↑I ∪ ↑J) = ⊤

Tactic:
· rintro _ ⟨x, hx, rfl⟩; exact Ideal.mem_sup_right (Ideal.pow_mem_pow hx n)

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ Ideal.span (↑I ∪ ↑J) = ⊤
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 ^ 1)

Tactic:
pow_one,

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 ^ (orderOf t).factorization p * (p ^ (orderOf t).factorization p * p ^ a * p)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ (zeroLocus {x})ᶜ ⊆ s

Tactic:
Set.compl_subset_comm,

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ sᶜ ⊆ zeroLocus {x}
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
⊢ exponent M₂ ∣ exponent M₁

Tactic:
refine Monoid.exponent_dvd_of_forall_pow_eq_one fun m₂ ↦ ?_

Goal state after:
F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
m₂ : M₂
⊢ m₂ ^ exponent M₁ = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case neg
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)
⊢ P ≤ H ∨ Disjoint H P

Tactic:
refine h3.symm.imp (fun h4 ↦ ?_) (fun h4 ↦ ?_)

Goal state after:
case neg.refine_1
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)
h4 : H.index.Coprime (Nat.card ↥P)
⊢ P ≤ H

case neg.refine_2
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)
h4 : (Nat.card ↥H).Coprime (Nat.card ↥P)
⊢ Disjoint H P
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
⊢ (powMonoidHom d).ker.index = Nat.card G / (Nat.card G).gcd d

Tactic:
by
  rw [Subgroup.index_ker, card_powMonoidHom_range]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : IsCompactElement ↑b
⊢ IsCompactElement b

Tactic:
simp only [CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup,
    Finset.sup_eq_iSup] at h ⊢
  intro ι s hb
  replace hb : (b : α) ≤ iSup ((↑) ∘ s) := le_trans hb <| (coe_iSup s) ▸ le_refl _
  obtain ⟨t, ht⟩ := h ι ((↑) ∘ s) hb
  exact ⟨t, (by simpa using ht : (b : α) ≤ _)⟩

Goal state after:
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))
⊢ Nat.card ↥(Subgroup.map (normalizer ↑H).subtype (comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x))) =
    p ^ (n + 1)

Tactic:
show Nat.card (Subgroup.map (normalizer (H : Set G)).subtype
      (comap (mk' (H.subgroupOf (normalizer H))) (Subgroup.zpowers x))) = p ^ (n + 1)
    suffices Nat.card (Subtype.val ''
      ((zpowers x).comap (mk' (H.subgroupOf (normalizer H))) : Set (normalizer H))) = p ^ (n + 1)
      by convert! this using 2
    rw [Nat.card_image_of_injective Subtype.val_injective
        ((zpowers x).comap (mk' (H.subgroupOf (normalizer H))) : Set (normalizer (H : Set G))),
      pow_succ, ← hH, Nat.card_congr hequiv, ← hx, ← Nat.card_zpowers, ← Nat.card_prod]
    exact Nat.card_congr
      (preimageMkEquivSubgroupProdSet (H.subgroupOf (normalizer H)) (zpowers x))

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

Goal state before:
pp: ι : 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 : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
this : ↑(μ a) ∈ ⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j
⊢ ↑(μ a) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose h), I j

Tactic:
mem_iInf

Goal state after:
ι : 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 : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
this : ∀ (i : ι), ↑(μ a) ∈ ⨅ (_ : i ∈ Finset.cons a t hat), ⨅ (_ : i ≠ a), I i
⊢ ∀ (i : ι), ↑(μ a) ∈ ⨅ (_ : i ∈ t), ⨅ (_ : i ≠ Exists.choose h), I i
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: ι : 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 : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
i : ι
this : i ∈ Finset.cons a t hat → ↑(μ a) ∈ ⨅ (_ : i ≠ a), I i
⊢ i ∈ t → ↑(μ a) ∈ ⨅ (_ : i ≠ Exists.choose h), I i

Tactic:
mem_iInf

Goal state after:
ι : 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 : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
i : ι
this : i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
⊢ i ∈ t → i ≠ Exists.choose h → ↑(μ a) ∈ I i
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
⊢ Iso
    (x₁,
      ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun
        (Fin.last ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)).succ)
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (Fin.last s.length).castSucc.castSucc,
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (Fin.last s.length).castSucc.succ)

Tactic:
Fin.succ_last,

Goal state after:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
⊢ Iso
    (x₁,
      ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun
        (Fin.last ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length).succ))
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (Fin.last s.length).castSucc.castSucc,
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (Fin.last s.length).castSucc.succ)