mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
⊢ SDiff α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
⊢ HNot α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
⊢ HImp α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
⊢ Compl α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
sSup : Set α → α
⊢ SupSet α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
⊢ Max α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
⊢ SupSet α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α

Tactic:
infer_instance

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

Goal state before:
pp: case h_empty
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_5
inst✝ : Finite ι
U : PEmpty.{u_5 + 1} → Opens α
⊢ ↑(⨅ i, U i) = ⋂ i, ↑(U i)

Tactic:
| h_empty =>

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
⊢ U.carrier ⊆ ⋃ i, ↑↑i

Tactic:
by simp [hsup]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)) →
    ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst✝] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst✝] s ⊆ s
x : { x // x ∈ closure[inst✝] s }
⊢ x ∈ Subtype.val ⁻¹' ⋃ x, ⋃ (h : x ∈ s), U x h → x ∈ closure[inst✝] s ↓∩ s

Tactic:
rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩
      exact e y hy ⟨hxU, x.2⟩

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst✝¹] t
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
⊢ IsCompact (⋂₀ s)

Tactic:
rw [heq, Set.sInter_union]

Goal state after:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst✝¹] t
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x : P
I✝ J✝ s t I J : Ideal P
⊢ {x | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}.Nonempty

Tactic:
obtain ⟨w, h⟩ := inter_nonempty I J
        exact ⟨w, w, h.1, w, h.2, le_sup_left⟩

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

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

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) C
hNe : C.Nonempty
⊢ IsIdeal (⋃₀ C)

Tactic:
refine ⟨isLowerSet_sUnion (fun I hI ↦ (hidl I hI).1), Set.nonempty_sUnion.2 ?_,
    directedOn_sUnion hD (fun J hJ => (hidl J hJ).3)⟩

Goal state after:
P : Type u_1
inst✝ : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) C
hNe : C.Nonempty
⊢ ∃ s ∈ C, s.Nonempty
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
⊢ IsRetrocompact Set.univ

Tactic:
simp +contextual [IsRetrocompact]

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case union
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
t : Set Y
ht : IsConstructible t
hs' : IsConstructible (f ⁻¹' s)
ht' : IsConstructible (f ⁻¹' t)
⊢ IsConstructible (f ⁻¹' (s ∪ t))

Tactic:
preimage_union

Goal state after:
case union
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
t : Set Y
ht : IsConstructible t
hs' : IsConstructible (f ⁻¹' s)
ht' : IsConstructible (f ⁻¹' t)
⊢ IsConstructible (f ⁻¹' s ∪ f ⁻¹' t)
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: R S T : Type u_3
x✝⁵ : CommRing R
x✝⁴ : CommRing S
x✝³ : CommRing T
x✝² : Algebra R S
x✝¹ : Algebra R T
x✝ : Module.FaithfullyFlat R T
⊢ Module.FaithfullyFlat S (TensorProduct R S T)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.Flat
algInst✝ : Algebra A B := f.toAlgebra
algebraizeInst✝ : Module.Flat A B
⊢ PreservesFiniteLimits (tensorLeft (of A B))

Tactic:
infer_instance

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

Goal state before:
pp: case singleton
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
q : PrimeSpectrum R
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.singleton {(a, b) | a < b} q).last.asIdeal
⊢ ∃ L,
    L.length = (RelSeries.singleton {(a, b) | a < b} q).length ∧
      RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) =
          (RelSeries.singleton {(a, b) | a < b} q).toList

Tactic:
use RelSeries.singleton _ ⟨P, inferInstance⟩
    simp only [RelSeries.singleton_length, RelSeries.last_singleton, RelSeries.toList_singleton,
      List.map_cons, List.map_nil, List.cons.injEq, and_true, true_and]
    ext : 1
    simpa using lo.over.symm

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

Goal state before:
pp: R S T : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Flat R T
⊢ Module.Flat S (S ⊗[R] T)

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Module.Flat R S
⊢ Algebra.HasGoingDown R S

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hR : IsField R
f : R →+* S
this✝ : Algebra R S := f.toAlgebra
this : Field R := hR.toField
⊢ Module.Flat R S

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
⊢ ↑(basicOpen (f * g)) = ↑(basicOpen f ⊓ basicOpen g)

Tactic:
by simp [zeroLocus_singleton_mul]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (orbitZMultiplesEquiv a b).symm ↑k = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩

Tactic:
rw [AddAction.orbitZMultiplesEquiv_symm_apply, ZMod.coe_intCast]

Goal state after:
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (k % ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩ = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
a : ↑(Set.range f)
⊢ IsLocalization.Away (↑a) (Localization.Away ↑a)

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
⊢ Function.Surjective ⇑(MaximalSpectrum.toPiLocalization R)

Tactic:
by
  rw [← piLocalizationToMaximal_comp_toPiLocalization]
  exact (piLocalizationToMaximal_surjective R).comp
    (toPiLocalization_surjective_of_discreteTopology R)

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

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ¬∃ x ∈ ⊥, x ≠ 1
⊢ IsCyclic ↥⊥

Tactic:
infer_instance

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

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
obtain ⟨I, hI, hI'⟩ := isCompact_isOpen_iff_ideal.mp ⟨hs.1.isCompact, hs.2⟩

Goal state after:
case inr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
hI' : (zeroLocus ↑I)ᶜ = s
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p✝ : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p
⊢ ¬p ∣ H.index

Tactic:
rw [← mul_dvd_mul_iff_left (Nat.card_pos (α := H)).ne', card_mul_index, card_eq, ← pow_succ]
    exact Nat.pow_succ_factorization_not_dvd Nat.card_pos.ne' Fact.out

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
⊢ ↑(minimalPrimes R) ≃o (↑(irreducibleComponents (PrimeSpectrum R)))ᵒᵈ

Tactic:
let e : {p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} ≃o PrimeSpectrum R :=
    ⟨⟨fun x ↦ ⟨x.1, x.2.1⟩, fun x ↦ ⟨x.1, x.2, bot_le⟩, fun _ ↦ rfl, fun _ ↦ rfl⟩, Iff.rfl⟩
  rw [irreducibleComponents_eq_maximals_closed]
  exact OrderIso.setOfPredMinimalIsoSetOfPredMaximal
    (e.trans ((PrimeSpectrum.pointsEquivIrreducibleCloseds R).trans
    (TopologicalSpace.IrreducibleCloseds.orderIsoSubtype' (PrimeSpectrum R)).dual))

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ { asIdeal := maximalIdeal R, isPrime := ⋯ }.asIdeal.IsMaximal

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ Finite α

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ IsStronglyAtomic αᵒᵈ

Tactic:
infer_instance

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

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

Tactic:
index_powMonoidHom_ker,

Goal state after:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
h : (powMonoidHom d).ker.index ≠ 0
⊢ Nat.card G = (Nat.card G).gcd d * (Nat.card G / (Nat.card G).gcd d)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : f = 1
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M

Tactic:
← f.ker_eq_top_iff

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : f.ker = ⊤
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM : IsCyclic M
hN : IsCyclic N
x✝¹ : CommGroup (M × N) := IsCyclic.commGroup
x✝ : CommGroup M := IsCyclic.commGroup
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
let _ := hN.commGroup

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM : IsCyclic M
hN : IsCyclic N
x✝² : CommGroup (M × N) := IsCyclic.commGroup
x✝¹ : CommGroup M := IsCyclic.commGroup
x✝ : CommGroup N := IsCyclic.commGroup
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝ : Infinite M
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
cases subsingleton_or_nontrivial N; · simp
      exact (not_isCyclic_prod_of_infinite_nontrivial M N h).elim

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

Goal state before:
pp: case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝¹ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
e : ↥f.ker ≃* M := ⋯.mpr (((⊤.prodEquiv ⊥).trans MulEquiv.prodUnique).trans Subgroup.topEquiv)
x✝ : CommGroup M := IsCyclic.commGroup
⊢ IsCyclic (M × N)

Tactic:
let _ := hN.commGroup

Goal state after:
case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝² : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
e : ↥f.ker ≃* M := ⋯.mpr (((⊤.prodEquiv ⊥).trans MulEquiv.prodUnique).trans Subgroup.topEquiv)
x✝¹ : CommGroup M := IsCyclic.commGroup
x✝ : CommGroup N := IsCyclic.commGroup
⊢ IsCyclic (M × N)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
⊢ Nat.card G ∣ ∏ g, orderOf g

Tactic:
refine Nat.dvd_iff_prime_pow_dvd_dvd .. |>.mpr fun p k hp h ↦ ?_

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
⊢ p ^ k ∣ ∏ g, orderOf g
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: M : Type u_4
inst✝² : AddCommGroup M
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R M
simple : IsSimpleModule R M
I : Ideal R
max : I.IsMaximal
e : M ≃ₗ[R] R ⧸ I
⊢ (Module.annihilator R M).IsMaximal

Tactic:
rwa [e.annihilator_eq, I.annihilator_quotient]

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

Goal state before:
pp: ι✝ : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁸ : Ring R✝
inst✝⁷ : Ring S
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R✝ M
m : Submodule R✝ M
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R✝ N
ι : Type u_7
inst✝² : Finite ι
R : ι → Type u_6
inst✝¹ : (i : ι) → Ring (R i)
inst✝ : ∀ (i : ι), IsSemisimpleRing (R i)
x✝ : (i : ι) → Module ((i : ι) → R i) (R i) := fun i ↦ Module.compHom (R i) (Pi.evalRingHom R i)
e : (i : ι) → R i →ₛₗ[Pi.evalRingHom R i] R i :=
  fun i ↦
    let __src := AddMonoidHom.id (R i);
    { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
this : ∀ (i : ι), IsSemisimpleModule ((i : ι) → R i) (R i)
⊢ IsSemisimpleRing ((i : ι) → R i)

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
e : S →ₛₗ[f] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleModule R S

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single.add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : (eval r) (p✝ • single R i m) = Polynomial.eval r p✝ • (eval r) (single R i m)
e₂ : (eval r) (q✝ • single R i m) = Polynomial.eval r q✝ • (eval r) (single R i m)
⊢ (eval r) ((p✝ + q✝) • single R i m) = Polynomial.eval r (p✝ + q✝) • (eval r) (single R i m)

Tactic:
rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
⊢ Function.LeftInverse (fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ })
    (restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun

Tactic:
intro

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
x✝ : Submodule (R ⧸ R ∙ a) ↥(torsionBy R M a)
⊢ (fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ })
      ((restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun x✝) =
    x✝
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
⊢ Function.RightInverse (fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ })
    (restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun

Tactic:
intro

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
x✝ : Submodule R ↥(torsionBy R M a)
⊢ (restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun
      ((fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }) x✝) =
    x✝
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : b * c = x
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x

Tactic:
mul_comm

Goal state after:
case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
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 = F.N (n + 1)

Tactic:
h.choose_spec (n + 1) (by lia),

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