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

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

Tactic:
refine ⟨(⋃₀ (irreducibleComponents α \ {Z}))ᶜ, ?_, ?_, subset_closure.trans hZ.le⟩

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

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
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case sup
X : Type u_2
inst✝ : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst✝] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s✝ s : Set X
hs : s ∈ BooleanSubalgebra.closure {U | IsOpen[inst✝] U ∧ IsRetrocompact U}
t : Set X
ht : t ∈ BooleanSubalgebra.closure {U | IsOpen[inst✝] U ∧ IsRetrocompact U}
hs' : p s hs
ht' : p t ht
⊢ p (s ⊔ t) ⋯

Tactic:
exact union _ _ _ _ hs' ht'

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set Y
hfcont : Continuous[inst✝¹, inst✝] f
hf : ∀ (s : Set Y), IsOpen[inst✝] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
hs' : IsConstructible (f ⁻¹' s)
⊢ IsConstructible (f ⁻¹' sᶜ)

Tactic:
rw [preimage_compl]; exact hs'.compl

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case sup
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✝ s : Set X
hx✝ : s ∈ BooleanSubalgebra.closure {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
t : Set X
hy✝ : t ∈ BooleanSubalgebra.closure {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
hs' : P s hx✝
ht' : P t hy✝
⊢ P (s ⊔ t) ⋯

Tactic:
exact union _ _ _ _ hs' ht'

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ HasGoingDown R S ↔ GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))

Tactic:
by
  refine ⟨?_, fun h ↦ ⟨fun {p} hp Q hQ hlt ↦ ?_⟩⟩
  · intro h Q p hp
    rw [← PrimeSpectrum.le_iff_specializes] at hp
    obtain ⟨P, hle, hP, h⟩ := Q.asIdeal.exists_ideal_le_liesOver_of_le (p := p.asIdeal)
      (q := Q.asIdeal.under R) hp
    refine ⟨⟨P, hP⟩, (PrimeSpectrum.le_iff_specializes _ Q).mp hle, ?_⟩
    ext : 1
    exact h.over.symm
  · have : (⟨p, hp⟩ : PrimeSpectrum R) ⤳ (PrimeSpectrum.comap (algebraMap R S) ⟨Q, hQ⟩) :=
      (PrimeSpectrum.le_iff_specializes _ _).mp hlt.le
    obtain ⟨P, hs, heq⟩ := h this
    refine ⟨P.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, P.2, ⟨?_⟩⟩
    simpa [PrimeSpectrum.ext_iff] using heq.symm

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
⊢ (↑(Algebra.TensorProduct.map (AlgHom.id S A) g)).Flat

Tactic:
exact hg.lTensor _

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑g
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
⊢ f.Flat

Tactic:
have : f = e.symm.toRingHom.comp (e.toRingHom.comp f) := by ext; simp

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑g
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
this : f = e.symm.toRingHom.comp (e.toRingHom.comp f)
⊢ f.Flat
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
⊢ zeroLocus ↑(vanishingIdeal t) = closure t

Tactic:
by
  rcases isClosed_iff_zeroLocus (closure t) |>.mp isClosed_closure with ⟨I, hI⟩
  rw [subset_antisymm_iff, (isClosed_zeroLocus _).closure_subset_iff, hI,
      subset_zeroLocus_iff_subset_vanishingIdeal, (gc R).u_l_u_eq_u,
      ← subset_zeroLocus_iff_subset_vanishingIdeal, ← hI]
  exact ⟨subset_closure, subset_zeroLocus_vanishingIdeal t⟩

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✝
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
⊢ closure S = S

Tactic:
h₂.closure_eq

Goal state after:
R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
⊢ S = S
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
n : ℕ
⊢ D ↑n = 0

Tactic:
by
  rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]

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

Goal state before:
pp: case neg.inr
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
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ -(a ^ ↑(n.natAbs * 2))⁻¹ • ↑n.natAbs • a ^ ↑(n.natAbs - 1) • D a = ↑(-↑n.natAbs) • a ^ (-↑n.natAbs - 1) • D a

Tactic:
smul_smul,

Goal state after:
case neg.inr
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
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-(a ^ ↑(n.natAbs * 2))⁻¹ * ↑n.natAbs) • a ^ ↑(n.natAbs - 1) • D a = ↑(-↑n.natAbs) • a ^ (-↑n.natAbs - 1) • D a
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case neg.inr
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
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-(a ^ ↑(n.natAbs * 2))⁻¹ * ↑n.natAbs) • a ^ ↑(n.natAbs - 1) • D a = ↑(-↑n.natAbs) • a ^ (-↑n.natAbs - 1) • D a

Tactic:
smul_smul,

Goal state after:
case neg.inr
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
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-(a ^ ↑(n.natAbs * 2))⁻¹ * ↑n.natAbs * a ^ ↑(n.natAbs - 1)) • D a = ↑(-↑n.natAbs) • a ^ (-↑n.natAbs - 1) • D a
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ Injective
    ⇑(QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯)

Tactic:
← ker_eq_bot_iff,

Goal state after:
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ (QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯).ker =
    ⊥
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
h : n % exponent G = 0
g : G
⊢ g ^ n = 1

Tactic:
pow_eq_mod_exponent,

Goal state after:
case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
h : n % exponent G = 0
g : G
⊢ g ^ (n % exponent G) = 1
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)))
⊢ H.index = ∑ q, minimalPeriod (fun x ↦ g • x) q.out

Tactic:
by
  have : Fintype (G ⧸ H) := Fintype.ofFinite _
  have (q : Quotient (MulAction.orbitRel (zpowers g) (G ⧸ H))) :
      Fintype (MulAction.orbit (zpowers g) q.out) := Fintype.ofFinite _
  simp only [MulAction.minimalPeriod_eq_card, index_eq_card, Nat.card_eq_fintype_card]
  rw [← Fintype.card_sigma]
  exact Fintype.card_congr (MulAction.selfEquivSigmaOrbits (zpowers g) (G ⧸ H))

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬(Set.range orderOf).Finite
t : G
het : exponent G < orderOf t
⊢ False

Tactic:
exact pow_ne_one_of_lt_orderOf he het (pow_exponent_eq_one t)

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:
by
  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
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ k, ∀ (g : G), orderOf g ∣ p ^ k

Tactic:
by
  refine isPGroup_iff_orderOf_dvd_pow.trans ⟨fun h ↦ ?_, fun ⟨k, hk⟩ ↦ fun g ↦ ⟨k, hk g⟩⟩
  choose k hk using h
  have := Fintype.ofFinite G
  have ⟨g, _, hg⟩ := Finset.exists_max_image .univ k Finset.univ_nonempty
  refine ⟨k g, fun g' ↦ ?_⟩
  grw [← Nat.pow_dvd_pow p <| hg g' <| Finset.mem_univ g']
  exact hk g'

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
⊢ IsPGroup p G ↔ (Nat.card G).primeFactors ⊆ p.primeFactors

Tactic:
refine isPGroup_iff_card_dvd_pow.trans ⟨fun ⟨n, hn⟩ ↦ ?_, fun hG ↦ ?_⟩
  · 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]
  · refine ⟨Nat.card G, Nat.dvd_prod_primeFactors_pow_self NeZero.out |>.trans ?_⟩
    grw [Finset.prod_dvd_prod_of_subset _ _ (·) hG, p.prod_primeFactors_dvd]

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
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h : basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1
⊢ a ⊓ b = a

Tactic:
have := (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h : basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1
this : IsIdempotentElem (↑a).1
⊢ a ⊓ b = a
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
⊢ #{a | orderOf a = d} = φ d

Tactic:
have ha : orderOf a = d := (mem_filter.1 ha').2

Goal state after:
case h.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
⊢ #{a | orderOf a = d} = φ d
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: T : Type u
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ PrimeSpectrum.comap (residue T) x = closedPoint T

Tactic:
Subsingleton.elim x ⊥

Goal state after:
T : Type u
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ PrimeSpectrum.comap (residue T) ⊥ = closedPoint T
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝ : Monoid G
tG : IsMulTorsion G
g : G
⊢ g ^ (orderOf g - 1) * g = 1

Tactic:
← pow_succ,

Goal state after:
G : Type u_1
H : Type u_2
inst✝ : Monoid G
tG : IsMulTorsion G
g : G
⊢ g ^ (orderOf g - 1 + 1) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

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

Tactic:
by
  obtain ⟨g, h⟩ := isCyclic_iff_exists_zpowers_eq_top.mp hG
  rw [MonoidHom.range_eq_map, ← h, MonoidHom.map_zpowers, Nat.card_zpowers, powMonoidHom_apply,
    orderOf_pow, orderOf_eq_card_of_zpowers_eq_top h]

Goal state after:
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyCoatomic α
ha : (Set.Iic a).Infinite
hfin : {x | x ⋖ a}.Finite
⊢ ∃ b, b ⋖ a ∧ (Set.Iic b).Infinite

Tactic:
by
  simp_rw [← toDual_covBy_toDual_iff (α := α)] at hfin ⊢
  exact exists_covby_infinite_Ici_of_infinite_Ici (α := αᵒᵈ) ha hfin

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

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h✝ : Infinite N
f : ZMod 0 →+ ZMod 2 := (ZMod.castHom ⋯ (ZMod 2)).toAddMonoidHom
⊢ False

Tactic:
have hf := ZMod.castHom_surjective (dvd_zero 2)

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h✝ : Infinite N
f : ZMod 0 →+ ZMod 2 := (ZMod.castHom ⋯ (ZMod 2)).toAddMonoidHom
hf : Function.Surjective ⇑(ZMod.castHom ⋯ (ZMod 2))
⊢ False
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
g : G
hg : g ∈ (↑H \ {1}).toFinset
⊢ p ∣ orderOf g

Tactic:
have ⟨hg, hg1⟩ : g ∈ H ∧ g ≠ 1 := by simpa using hg

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
g : G
hg✝ : g ∈ (↑H \ {1}).toFinset
hg : g ∈ H
hg1 : g ≠ 1
⊢ p ∣ orderOf g
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
⊢ IsMaximal a y

Tactic:
have hb : x ⊔ y = b := sup_eq_of_isMaximal hxb hyb hxy
  subst a b
  exact isMaximal_inf_right_of_isMaximal_sup hxb hyb

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2) (toList s)

Tactic:
by
    simp_rw [List.isChain_iff_getElem, s.toList_getElem]
    exact fun _ _ => s.strictMono (Nat.lt_succ_self _)

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
⊢ s₁ = s₂

Tactic:
have : ∀ x, x ∈ s₁ ↔ x = s₁.last := fun x =>
    ⟨fun hx =>  subsingleton_of_length_eq_zero hs₁0 hx s₁.last_mem, fun hx => hx.symm ▸ s₁.last_mem⟩

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
this : ∀ (x : X), x ∈ s₁ ↔ x = last s₁
⊢ s₁ = s₂
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ c • d • i + c • z ∈ I • span R s

Tactic:
smul_smul,

Goal state after:
case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ (c * d) • i + c • z ∈ I • span R s
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n = 1 • n - s • 0

Tactic:
one_smul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n = n - s • 0
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 • I ^ (n - h.choose) • F.N h.choose = I ^ (n + 1 - h.choose) • F.N h.choose

Tactic:
smul_smul,

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 = I ^ (n + 1 - h.choose) • F.N h.choose
Module: Mathlib.RingTheory.Nakayama

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
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : map (I • N).mkQ N ≤ map (I • N).mkQ N'
⊢ N ≤ N'

Tactic:
apply le_of_le_smul_of_le_jacobson_bot hN hIjac

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : map (I • N).mkQ N ≤ map (I • N).mkQ N'
⊢ N ≤ N' ⊔ I • N
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.Stable

Tactic:
rw [← submodule_fg_iff_stable] at hF ⊢

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.submodule.FG

case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (i : ℕ), (F'.N i).FG

case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (i : ℕ), (F.N i).FG
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f g : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), f.app X = g.app X
⊢ f.app = g.app

Tactic:
ext1; apply h

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
w : (total β C).map f = (total β C).map g
⊢ f = g

Tactic:
ext i
    replace w := Sigma.ι (fun i : β => X i) i ≫= w
    erw [colimit.ι_map, colimit.ι_map] at w
    replace w : f i ≫ colimit.ι (Discrete.functor Y) ⟨i⟩ =
      g i ≫ colimit.ι (Discrete.functor Y) ⟨i⟩ := by simpa
    exact Mono.right_cancellation _ _ w

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
⊢ C.d i j ≫ C.d j k = 0

pp: case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ¬c.Rel i j
⊢ C.d i j ≫ C.d j k = 0

Tactic:
· by_cases hjk : c.Rel j k
    · exact C.d_comp_d' i j k hij hjk
    · rw [C.shape j k hjk, comp_zero]

Goal state after:
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ¬c.Rel i j
⊢ C.d i j ≫ C.d j k = 0
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd C 0 a).inv.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).hom.app X) ≫ eqToHom ⋯

Tactic:
by
  simp [← shiftFunctorAdd'_zero_add_inv_app, shiftFunctorAdd']

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ Subsingleton Ω[S⁄R]

Tactic:
by
  suffices (⊤ : Submodule S Ω[S⁄R]) ≤ ⊥ from
    (subsingleton_iff_forall_eq 0).mpr fun y ↦ this trivial
  rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]
  rintro _ ⟨x, rfl⟩; obtain ⟨x, rfl⟩ := h x; simp

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n : A
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n (-n) ⋯).hom.app X) =
    (shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((shiftFunctor C n).obj X)

Tactic:
apply shift_shiftFunctorCompIsoId_hom_app

Goal state after: