mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R N
⊢ Nontrivial (M ⊗[R] N) ↔ Nontrivial M

Tactic:
by
  contrapose!; exact subsingleton_tensorProduct_iff_left R M

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : -↑n ≠ 0
h : -↑n • x = (algebraMap S K) s
⊢ n • x = (algebraMap S K) (-s)

Tactic:
simp [← h]

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
x : S
inst✝ : Away x Sₘ
hx : IsIntegral R ((algebraMap S Sₘ) x)
⊢ IsIntegral R x

Tactic:
by
  obtain ⟨p, hpm, hp⟩ := hx
  simp only [IsScalarTower.algebraMap_eq R S Sₘ, IsLocalization.map_eq_zero_iff (.powers x),
    Subtype.exists, Submonoid.mem_powers_iff, ← hom_eval₂, exists_prop, exists_exists_eq_and] at hp
  obtain ⟨n, hn⟩ := hp
  exact ⟨X ^ n * p, (monic_X_pow n).mul hpm, by simpa⟩

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
m : Ideal R
inst✝ : m.IsMaximal
I : PrimeSpectrum R
h : I ∈ {{ asIdeal := m, isPrime := ⋯ }}
⊢ I ∈ zeroLocus ↑m

Tactic:
simp [Set.mem_singleton_iff.mp h]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
⊢ IsAlgebraic (↥Rt) a

Tactic:
have : IsScalarTower Rs Rts A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ rfl

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this : IsScalarTower (↥Rs) (↥Rts) A
⊢ IsAlgebraic (↥Rt) a
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
H : f.SurjectiveOnStalks
I : Ideal R
inst✝¹ : I.IsPrime
J : Ideal S
inst✝ : J.IsPrime
hf : I = Ideal.comap f J
⊢ Function.Bijective ⇑(Ideal.ResidueField.map I J f hf)

Tactic:
subst hf

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
H : f.SurjectiveOnStalks
J : Ideal S
inst✝¹ : J.IsPrime
inst✝ : (Ideal.comap f J).IsPrime
⊢ Function.Bijective ⇑(Ideal.ResidueField.map (Ideal.comap f J) J f ⋯)
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a).1 * (↑b).1 = (↑a).1
hbc : (↑b).1 * (↑c).1 = (↑b).1
⊢ (↑a).1 * (↑c).1 = (↑a).1

Tactic:
← hab,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a).1 * (↑b).1 = (↑a).1
hbc : (↑b).1 * (↑c).1 = (↑b).1
⊢ (↑a).1 * (↑b).1 * (↑c).1 = (↑a).1 * (↑b).1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a).1 * (↑b).1 = (↑a).1
hba : (↑b).1 * (↑a).1 = (↑b).1
⊢ (↑a).1 = (↑b).1

Tactic:
← hab,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a).1 * (↑b).1 = (↑a).1
hba : (↑b).1 * (↑a).1 = (↑b).1
⊢ (↑a).1 * (↑b).1 = (↑b).1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hbc : ↑b * ↑c = ↑b
⊢ ↑a * ↑c = ↑a

Tactic:
← hab,

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hbc : ↑b * ↑c = ↑b
⊢ ↑a * ↑b * ↑c = ↑a * ↑b
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hba : ↑b * ↑a = ↑b
⊢ ↑a = ↑b

Tactic:
← hab,

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hba : ↑b * ↑a = ↑b
⊢ ↑a * ↑b = ↑b
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ comap f x = p

Tactic:
have hp : ker f ≤ p.asIdeal := (Ideal.comap_mono bot_le).trans h_I_p

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ comap f x = p
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝¹ : (i : ι) → CommSemiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
h : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Finite ι

Tactic:
contrapose! h

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝¹ : (i : ι) → CommSemiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
h : Infinite ι
⊢ ¬Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum R
⊢ (mapPiLocalization (RingHom.id R)) x✝¹ x✝ = (RingHom.id (PiLocalization R)) x✝¹ x✝

Tactic:
exact congr($(Localization.localRingHom_id _) _)

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ↑L = univ ↔ L = ⊤

Tactic:
by rw [← coe_top, coe_inj]

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

Goal state before:
pp: case h.refine_2
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
s : Finset κ
hs : W.carrier ⊆ ⋃ i ∈ s, (U (a i)).carrier
⊢ ⨆ k, U ((a ∘ Subtype.val) k) ≤ W

Tactic:
rw [heq, iSup_le_iff]

Goal state after:
case h.refine_2
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
s : Finset κ
hs : W.carrier ⊆ ⋃ i ∈ s, (U (a i)).carrier
⊢ ∀ (i : ↥s), U ((a ∘ Subtype.val) i) ≤ ⨆ k, U (a k)
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ IsCompactElement s ↔ IsCompact ↑s

Tactic:
by
  rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup]
  refine ⟨?_, fun H ι U hU => ?_⟩
  · introv H hU hU'
    obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)
    refine ⟨t, Set.Subset.trans ht ?_⟩
    rw [coe_finset_sup, Finset.sup_eq_iSup]
    rfl
  · obtain ⟨t, ht⟩ :=
      H (fun i => U i) (fun i => (U i).isOpen) (by simpa using show (s : Set α) ⊆ ↑(iSup U) from hU)
    refine ⟨t, Set.Subset.trans ht ?_⟩
    simp only [Set.iUnion_subset_iff]
    change ∀ i ∈ t, U i ≤ t.sup U
    exact fun i => Finset.le_sup

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
h : Subsingleton (Compacts α)
⊢ IsEmpty α

Tactic:
contrapose! h

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
h : Nonempty α
⊢ Nontrivial (Compacts α)
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
⊢ IsLocallyConstructible (s ∩ t)

Tactic:
rintro x

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝] U ∧ IsConstructible (U ↓∩ s ∩ t)
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
⊢ IsLocallyConstructible (s ∩ t)

Tactic:
by
  rintro x
  obtain ⟨U, hxU, hU, hsU⟩ := hs x
  obtain ⟨V, hxV, hV, htV⟩ := ht x
  refine ⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩
  change IsConstructible
    (inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∩ inclusion inter_subset_right ⁻¹' (V ↓∩ t))
  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.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
⊢ IsLocallyConstructible (s ∪ t)

Tactic:
rintro x

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝] U ∧ IsConstructible (U ↓∩ (s ∪ t))
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ l.toList[0].asIdeal = under R (RelSeries.toList L)[0].asIdeal

Tactic:
Ideal.under_def

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ l.toList[0].asIdeal = comap (algebraMap R S) (RelSeries.toList L)[0].asIdeal
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: ⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ Flat

Tactic:
introv R hsp h
  algebraize_only [f]
  refine Module.flat_of_isLocalized_span _ _ s hsp _
    (fun r ↦ Algebra.linearMap S <| Localization.Away r.1) ?_
  dsimp only [RingHom.Flat] at h
  convert! h; ext
  apply Algebra.smul_def

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

Goal state before:
pp: a b : ℕ
⊢ ((a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1).Coprime
    (a.factorizationLCMRight b)

Tactic:
factorizationLCMRight

Goal state after:
a b : ℕ
⊢ ((a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1).Coprime
    ((a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (fun a_1 b_1 ↦
      (if b.factorization a_1 ≤ a.factorization a_1 then a_1 ^ b_1 else 1) *
        if b.factorization a_1 ≤ a.factorization a_1 then 1 else a_1 ^ b_1) =
    fun x1 x2 ↦ x1 ^ x2

Tactic:
ext p n

Goal state after:
case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
⊢ ((if b.factorization p ≤ a.factorization p then p ^ n else 1) *
      if b.factorization p ≤ a.factorization p then 1 else p ^ n) =
    p ^ n
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) i ((a.lcm b).factorization i) ∣
      i ^ a.factorization i

Tactic:
rintro p -

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p) ∣
    p ^ a.factorization p
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) i ((a.lcm b).factorization i) ∣
      i ^ b.factorization i

Tactic:
rintro p -

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : fin.toFinset.inf id ≤ I
⊢ I.IsMaximal

Tactic:
hI.inf_le'

Goal state after:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ zeroLocus (⋃ i, {f i}) = Set.univᶜ ↔ zeroLocus ↑(Ideal.span (Set.range f)) = ∅

Tactic:
simp only [Set.iUnion_singleton_eq_range, Set.compl_univ, PrimeSpectrum.zeroLocus_span]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (n.gcd (Fintype.card α) * m / n.gcd (Fintype.card α)) ≤ n

Tactic:
rw [Nat.mul_div_cancel_left _ (gcd_pos_of_pos_left _ hn0), gcd_mul_left_left, hm,
        Nat.mul_div_cancel _ hm0]

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ n.gcd (Fintype.card α) ≤ n
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ (toMonoidHom G m) g = g ^ k

Tactic:
(MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec g,

Goal state after:
G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ g ^ ⋯.choose = g ^ k
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: 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
⊢ orderOf (t ^ p ^ k) = orderOf t / p ^ k

Tactic:
rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]

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 ↔ ∃ n, Nat.card G ∣ p ^ n

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨n, hn⟩ ↦ of_card_dvd_pow hn⟩
  rcases eq_or_ne p 0 with rfl | hp
  · exact ⟨1, by simp⟩
  refine ⟨Nat.card G, Nat.dvd_pow_self_iff NeZero.out hp |>.mpr fun q hq ↦ ?_⟩
  have ⟨hqp, hqdvd, _⟩ := Nat.mem_primeFactors.mp hq
  have ⟨g, hg⟩ := exists_prime_orderOf_dvd_card' q (hp := ⟨hqp⟩) hqdvd
  have ⟨k, hk⟩ := h.exists_orderOf_dvd_pow g
  exact Nat.mem_primeFactors.mpr ⟨hqp, hqp.dvd_of_dvd_pow <| hg ▸ hk, hp⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
h : p₁.Coprime p₂
g : G
hg₁✝ : g ∈ H₁
hg₂ : g ∈ H₂
k₁ : ℕ
hk₁ : ⟨g, hg₁✝⟩ ^ p₁ ^ k₁ = 1
hg₁ : orderOf g ∣ p₁ ^ k₁
⊢ g = 1

Tactic:
have ⟨k₂, hk₂⟩ := hH₂ ⟨g, hg₂⟩

Goal state after:
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
h : p₁.Coprime p₂
g : G
hg₁✝ : g ∈ H₁
hg₂ : g ∈ H₂
k₁ : ℕ
hk₁ : ⟨g, hg₁✝⟩ ^ p₁ ^ k₁ = 1
hg₁ : orderOf g ∣ p₁ ^ k₁
k₂ : ℕ
hk₂ : ⟨g, hg₂⟩ ^ p₂ ^ k₂ = 1
⊢ g = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: 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
k : ℕ
hk : Nat.card ↥P = p ^ k
⊢ (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)

Tactic:
refine hk ▸ Or.imp hp.out.coprime_pow_of_not_dvd hp.out.coprime_pow_of_not_dvd ?_

Goal state after:
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
k : ℕ
hk : Nat.card ↥P = p ^ k
⊢ ¬p ∣ Nat.card ↥H ∨ ¬p ∣ H.index
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ t.card ≤ s.card

Tactic:
← Finset.card_image_of_injOn H,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ (Finset.image Subtype.val t).card ≤ s.card
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ orderOf g ≠ 0

Tactic:
contrapose! h

Goal state after:
case h1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : orderOf g = 0
⊢ ∃ n, ¬orderOf g ∣ n ∧ n.gcd (orderOf g) ≠ 1
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ⊥ ≠ ⊤
⊢ ∃ y, 0 ≠ y

Tactic:
contrapose! h

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ∀ (y : M), 0 = y
⊢ ⊥ = ⊤
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_3
ι : 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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
⊢ ∑ i ∈ Finset.cons a t hat, ↑(if hi : i = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ i), ⋯⟩) = 1

Tactic:
rw [Finset.sum_cons, dif_pos rfl, add_comm]

Goal state after:
case refine_2.mpr.refine_3
ι : 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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
⊢ ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) + ↑⟨v, ⋯⟩ = 1
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
this :
  ∃ t,
    head t = (eraseLast s).head ∧
      t.length + 1 = n ∧
        ∃ (htx : last t = x ⊓ (eraseLast s).last), Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
⊢ ∃ t, head t = head s ∧ t.length + 1 = n + 1 ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)

Tactic:
rcases this with ⟨t, htb, htl, htt, hteqv⟩

Goal state after:
case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
⊢ ∃ t, head t = head s ∧ t.length + 1 = n + 1 ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
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
s : Set R
⊢ torsionBySet R M s = torsionBySet R M ↑(Ideal.span s)

Tactic:
refine le_antisymm (fun x hx => ?_) (torsionBySet_le_torsionBySet_of_subset subset_span)
  rw [mem_torsionBySet_iff] at hx ⊢
  suffices Ideal.span s ≤ Ideal.torsionOf R M x by
    rintro ⟨a, ha⟩
    exact this ha
  rw [Ideal.span_le]
  exact fun a ha => hx ⟨a, ha⟩

Goal state after: