mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ (r₂ • a₁) ⊗ₜ[R] (t₂ * t₁) + a₂ ⊗ₜ[R] (r₁ • (t₁ * t₂)) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)

Tactic:
← TensorProduct.smul_tmul,

Goal state after:
case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ (r₂ • a₁) ⊗ₜ[R] (t₂ * t₁) + (r₁ • a₂) ⊗ₜ[R] (t₁ * t₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ }
this : m = Ideal.comap (algebraMap A B) m'.asIdeal
⊢ m • ⊤ ≠ ⊤

Tactic:
Ideal.smul_top_eq_map,

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ }
this : m = Ideal.comap (algebraMap A B) m'.asIdeal
⊢ Submodule.restrictScalars A (Ideal.map (algebraMap A B) m) ≠ ⊤
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
⊢ m • ⊤ ≠ ⊤

Tactic:
Ideal.smul_top_eq_map,

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
⊢ Submodule.restrictScalars A (Ideal.map (algebraMap A B) m) ≠ ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
⊢ Function.Bijective (sigmaToPi R)

Tactic:
refine ⟨sigmaToPi_injective R, ?_⟩

Goal state after:
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
⊢ Function.Surjective (sigmaToPi R)
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: case inl
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
he : s = ∅
⊢ IsPreirreducible ∅

Tactic:
exact isPreirreducible_empty

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Tactic:
tfae_have 1 → 3 := @NoetherianSpace.isCompact α _

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ (∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S) →
    ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
H

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : IsCodirectedOrder P
I J : Ideal P
⊢ (↑I ∩ ↑J).Nonempty

Tactic:
obtain ⟨a, ha⟩ := I.nonempty
  obtain ⟨b, hb⟩ := J.nonempty
  obtain ⟨c, hac, hbc⟩ := exists_le_le a b
  exact ⟨c, I.lower hac ha, J.lower hbc hb⟩

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case insert.inl
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
a✝ : Set α
ha : a✝ ∉ ∅
hs : ∅.Finite
ih :
  (∀ t ∈ ∅, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t) →
    (∀ t ∈ ∅, IsCompact t) → (∀ t ∈ ∅, IsOpen[inst✝¹] t) → ∅.Nonempty → IsCompact (⋂₀ ∅)
ho : ∀ t ∈ insert a✝ ∅, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ insert a✝ ∅, IsCompact t
h : ∀ t ∈ insert a✝ ∅, IsOpen[inst✝¹] t
⊢ (insert a✝ ∅).Nonempty → IsCompact (⋂₀ insert a✝ ∅)

pp: case insert.inr
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s✝ : Set (Set α)
a✝ : Set α
s : Set (Set α)
ha : a✝ ∉ s
hs : s.Finite
ih :
  (∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t) →
    (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen[inst✝¹] t) → s.Nonempty → IsCompact (⋂₀ s)
ho : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ insert a✝ s, IsCompact t
h : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t
hne : s.Nonempty
⊢ (insert a✝ s).Nonempty → IsCompact (⋂₀ insert a✝ s)

Tactic:
· grind

Goal state after:
case insert.inr
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s✝ : Set (Set α)
a✝ : Set α
s : Set (Set α)
ha : a✝ ∉ s
hs : s.Finite
ih :
  (∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t) →
    (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen[inst✝¹] t) → s.Nonempty → IsCompact (⋂₀ s)
ho : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ insert a✝ s, IsCompact t
h : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t
hne : s.Nonempty
⊢ (insert a✝ s).Nonempty → IsCompact (⋂₀ insert a✝ s)
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ ¬Subsingleton (NonemptyCompacts α) ↔ ¬Subsingleton α

Tactic:
subsingleton_iff

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
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingDown R S
inst✝ : HasGoingDown S T
⊢ GeneralizingMap (PrimeSpectrum.comap (algebraMap R T))

Tactic:
IsScalarTower.algebraMap_eq R S T

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingDown R S
inst✝ : HasGoingDown S T
⊢ GeneralizingMap (PrimeSpectrum.comap ((algebraMap S T).comp (algebraMap R S)))
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) ≠ 0

Tactic:
H

Goal state after:
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
⊢ False
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
⊢ (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) ≠ 0

Tactic:
H

Goal state after:
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
⊢ False
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ a.factorization.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
rw [prod_of_support_subset (s := (lcm a b).factorization.support)]

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ a.factorization x

case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization.support ⊆ (a.lcm b).factorization.support

case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ b.factorization.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
rw [prod_of_support_subset (s := (lcm a b).factorization.support)]

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ b.factorization x

case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.factorization.support ⊆ (a.lcm b).factorization.support

case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Continuous ⇑(primeSpectrumProd R S).symm

Tactic:
continuous_sum_dom

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Continuous (⇑(primeSpectrumProd R S).symm ∘ Sum.inl) ∧ Continuous (⇑(primeSpectrumProd R S).symm ∘ Sum.inr)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ g' ∈ zpowers g

Tactic:
simp_rw [zpowers_eq_top_of_prime_card h hg, Subgroup.mem_top]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
H : Subgroup G
⊢ H ≤ zpowers g ↔ ∃ n, H = zpowers (g ^ n)

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨x, rfl⟩ := (H.isCyclic_iff_exists_zpowers_eq_top).mp (isCyclic_of_le h)
    obtain ⟨k, rfl⟩ := mem_zpowers_iff.mp <| h (mem_zpowers x)
    obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg k
    · exact ⟨n, by rw [zpow_natCast]⟩
    · exact ⟨n, by simp⟩
  · rintro ⟨k, rfl⟩
    exact zpowers_le_of_mem <| npow_mem_zpowers g k

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ s_1, s_1.Finite ∧ s = ⋃ i ∈ s_1, ↑(basicOpen i)) ↔ ∃ t, (zeroLocus ↑t)ᶜ = s

Tactic:
simp only [basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂, ← zeroLocus_iUnion₂,
    Set.biUnion_of_singleton]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ s_1, s_1.Finite ∧ s = (zeroLocus s_1)ᶜ) ↔ ∃ t, (zeroLocus ↑t)ᶜ = s
Module: Mathlib.GroupTheory.Exponent

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

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

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

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
g : G
hg : orderOf g = Nat.card G
⊢ ⋯.choose ≡ 1 [ZMOD ↑n]

Tactic:
← hn,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
g : G
hg : orderOf g = Nat.card G
⊢ ⋯.choose ≡ 1 [ZMOD ↑(Nat.card G)]
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'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ ⋯.choose ≡ ⋯.choose * ⋯.choose [ZMOD ↑n✝]

Tactic:
← hn,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ ⋯.choose ≡ ⋯.choose * ⋯.choose [ZMOD ↑(Nat.card G)]
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
⊢ zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) ∩ zeroLocus ↑(Ideal.span {X}) = ∅

Tactic:
H

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
⊢ comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p}) ∩ zeroLocus ↑(Ideal.span {X}) = ∅
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
S : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module (ZMod n) M
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
hx : x ∈ K
c : ZMod n
⊢ c • x ∈ K

Tactic:
rw [← ZMod.intCast_zmod_cast c, Int.cast_smul_eq_zsmul]
  exact zsmul_mem hx (cast c)

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

Goal state before:

Tactic:
a * b = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) := by simp [mul_assoc]
    _ = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b) := by rw [mem_center_iff.1 ha]
    _ = y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) := by simp [mul_assoc]
    _ = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) := by rw [mem_center_iff.1 hb]
    _ = b * a := by group

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

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ zmultiples ↑n = zmultiples ↑(Nat.card ↥(zmultiples g))

Tactic:
← hn,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ zmultiples ↑(Nat.card G) = zmultiples ↑(Nat.card ↥(zmultiples g))
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (↑n * (i / ↑n)) • g = 0

Tactic:
mul_zsmul',

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (i / ↑n) • ↑n • g = 0
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (i / ↑n) • n • g = 0

Tactic:
← hn,

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (i / ↑(Nat.card G)) • Nat.card G • g = 0
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p G
hP : ↑P ≤ N
⊢ normalizer ↑P ⊔ N = ⊤

Tactic:
← normalizer_sup_eq_top (P.subtype hP),

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p G
hP : ↑P ≤ N
⊢ normalizer ↑P ⊔ N = normalizer ↑(map N.subtype ↑(P.subtype hP)) ⊔ N
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₁ x = f₂ x

Tactic:
← hn,

Goal state after:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₁ (g ^ n) = f₂ (g ^ n)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₁ g ^ n = f₂ g ^ n

Tactic:
H

Goal state after:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₂ g ^ n = f₂ g ^ n
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
⊢ ∀ (ι : Type u_2) (s : ι → ↑(Iic a)), b ≤ iSup s → ∃ t, b ≤ ⨆ a_2 ∈ t, s a_2

Tactic:
intro ι s hb

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : b ≤ iSup s
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a | IsAtom a}
⊢ sSup {a | IsAtom a} = ⊤

Tactic:
have hu₂ : sSup u = ⨆ i ∈ s, f i := by simp_rw [u, sSup_iUnion, biSup_congr' ht]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a | IsAtom a}
hu₂ : sSup u = ⨆ i ∈ s, f i
⊢ sSup {a | IsAtom a} = ⊤
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
⊢ ∃ H' ≤ H, Nat.card ↥H' = p ^ n

Tactic:
refine ⟨H'.map H.subtype, map_subtype_le _, ?_⟩

Goal state after:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
⊢ Nat.card ↥(Subgroup.map H.subtype H') = p ^ n
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
x✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
e : M ≃ₗ[R] Π₀ (m : ↑s), ↥↑m
h : sSupIndep s ∧ ∀ (m : ↑s), IsSimpleModule R ↥↑m
⊢ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m

Tactic:
exact ⟨s, e, h.2⟩

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 ι
M : ι → Type u_6
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), IsSemisimpleModule R (M i)
⊢ ⨆ i, (single R M i).range = ⊤

Tactic:
by simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert.refine_1
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
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
⊢ c * r - 1 ∈ I

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
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
⊢ N ≤ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)

Tactic:
· simpa only [mul_sub, mul_one, sub_add_sub_cancel] using I.add_mem (I.mul_mem_left c hr1) hc1

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
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
⊢ N ≤ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
i : ℕ
m : S
⊢ x ^ i * (algebraMap S R) m = (eval x) (single R i ((algebraMap S R) m))

Tactic:
eval_single,

Goal state after:
case single
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
i : ℕ
m : S
⊢ x ^ i * (algebraMap S R) m = x ^ i • (algebraMap S R) m
Module: Mathlib.Algebra.Polynomial.Module.Basic

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

Tactic:
eval_single,

Goal state after:
case single
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
i : ℕ
m : M
⊢ (eval r) (p ^ i • single R 0 m) = Polynomial.eval r p ^ i • m
Module: Mathlib.Algebra.Polynomial.Module.Basic

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

Tactic:
eval_single,

Goal state after:
case single
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
i : ℕ
m : M
⊢ Polynomial.eval r (p ^ i) • r ^ 0 • m = Polynomial.eval r p ^ i • m