mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : IsLocalRing R
inst✝¹² : CommRing S
inst✝¹¹ : IsLocalRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : IsLocalRing T
inst✝⁸ : Algebra R S
inst✝⁷ : IsLocalHom (algebraMap R S)
R₀ : Type u_4
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : IsLocalRing R₀
inst✝¹ : IsLocalHom (algebraMap R₀ R)
inst✝ : IsLocalHom (algebraMap R₀ S)
⊢ IsScalarTower (ResidueField R₀) (ResidueField R) (ResidueField S)

Tactic:
by
  refine .of_algebraMap_eq fun x ↦ ?_
  obtain ⟨x, rfl⟩ := residue_surjective x
  simp [← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
reg : IsSMulRegular M x
p : Ideal R
hp : p ∈ (Module.annihilator R M).minimalPrimes
hx : x ∈ p
y : R
hy : y ∉ Module.annihilator R M
hxy : x * y ∈ Module.annihilator R M
m : M
hm : ¬y • m = 0
⊢ False

Tactic:
exact hm (reg.right_eq_zero_of_smul ((smul_smul x y m).trans (Module.mem_annihilator.mp hxy m)))

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : v.IsMaximal
⊢ (algebraMap R K) y = (algebraMap R K) y * 1⁻¹

Tactic:
inv_one,

Goal state after:
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : v.IsMaximal
⊢ (algebraMap R K) y = (algebraMap R K) y * 1
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : ↑(f ⁻¹' s)
y : ↑s
⊢ (fun x1 x2 ↦ x1 ⤳ x2) y (s.restrictPreimage f x) → ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : ↑(f ⁻¹' s)
y : ↑s
h : y ⤳ s.restrictPreimage f x
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective ⇑f
⊢ map f (L ⊓ M) = map f L ⊓ map f M

Tactic:
by
  rw [← SetLike.coe_set_eq]
  simp [Set.image_inter hf]

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst✝ : ∀ (i : ι), PrespectralSpace ↥(U i)
⊢ PrespectralSpace X

Tactic:
by
  refine .of_isTopologicalBasis (hU.isTopologicalBasis fun i ↦ isTopologicalBasis) ?_
  simp only [Set.mem_iUnion, Set.mem_image, Set.mem_ofPred_eq, forall_exists_index, and_imp,
    forall_comm (α := Set _), forall_apply_eq_imp_iff₂]
  exact fun i V hV hV' ↦ hV'.image continuous_subtype_val

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact (t i ⊓ s.inf t)

Tactic:
exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst✝¹] U
⊢ IsCompact (f ⁻¹' s ∩ U)

Tactic:
hf.isCompact_iff,

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst✝¹] U
⊢ IsCompact (f '' (f ⁻¹' s ∩ U))
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
s : TopologicalSpace.IrreducibleCloseds α
⊢ (fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }) ((fun s ↦ ⋯.genericPoint) s) = s

Tactic:
refine TopologicalSpace.IrreducibleCloseds.ext ?_
    simp only [IsIrreducible.genericPoint_closure_eq, TopologicalSpace.IrreducibleCloseds.coe_mk,
      closure_eq_iff_isClosed.mpr s.3]
    rfl

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ IsLocallyConstructible (t i ⊓ s.inf t)

Tactic:
exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

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
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 f g).Flat

Tactic:
heq

Goal state after:
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 f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)).Flat
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
⊢ Zs ⊆ Set.range zeroLocus → ⋂₀ Zs ∈ Set.range zeroLocus

Tactic:
h

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
⊢ ⋂₀ Zs ∈ Set.range zeroLocus
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : zeroLocus ↑I = zeroLocus ↑J
⊢ vanishingIdeal (zeroLocus ↑I) = vanishingIdeal (zeroLocus ↑J)

Tactic:
h

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
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
⊢ comap (algebraMap R S) p = comap (algebraMap R S) q → p = q

Tactic:
h

Goal state after:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h : comap (algebraMap R S) p = comap (algebraMap R S) q
⊢ p = q
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case neg.inl
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
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
h

Goal state after:
case neg.inl
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
⊢ D (a ^ ↑n.natAbs) = ↑n.natAbs • a ^ (↑n.natAbs - 1) • D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
⊢ q ∈ ↑(basicOpen f)

Tactic:
simpa using hp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = 0

Tactic:
orderOf_eq_card_of_forall_mem_zpowers h,

Goal state after:
α : Type u_1
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ Nat.card α = 0
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
⊢ g ^ ⋯.choose = g ^ (⋯.choose * ⋯.choose)

Tactic:
zpow_mul',

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
⊢ g ^ ⋯.choose = (g ^ ⋯.choose) ^ ⋯.choose
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
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : (I * J) ^ n ≤ 0
hnz : n ≠ 0
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
mul_pow,

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
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ 0
hnz : n ≠ 0
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ 1 = (a * b) ^ 2

Tactic:
h

Goal state after:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ 1 = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
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
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
⊢ b.coeff 0 = 1

Tactic:
h

Goal state after:
case refine_1
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
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
⊢ 1 = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (hGpn ▸ pow_ne_zero n (NeZero.ne p))
  have hcG := to_subgroup (of_card hGpn) (center G)
  rcases iff_card.1 hcG with _
  have : Nontrivial G := (nontrivial_iff_card <| of_card hGpn).2 ⟨n, hn, hGpn⟩
  exact (nontrivial_iff_card hcG).mp (center_nontrivial (of_card hGpn))

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : H →* G
hf : IsPGroup p ↥f.ker
inst✝ : Finite (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P ↦ exists_comap_eq_of_ker_isPGroup P hf
g : Sylow p H → Sylow p G := fun P ↦ Classical.choose ⋯
hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P
P Q : Sylow p H
h : g P = g Q
⊢ comap f ↑(g P) = ↑Q

Tactic:
h

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : H →* G
hf : IsPGroup p ↥f.ker
inst✝ : Finite (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P ↦ exists_comap_eq_of_ker_isPGroup P hf
g : Sylow p H → Sylow p G := fun P ↦ Classical.choose ⋯
hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P
P Q : Sylow p H
h : g P = g Q
⊢ comap f ↑(g Q) = ↑Q
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
⊢ rank G = 0

Tactic:
rw [← le_zero_iff, ← Finset.card_empty]
  exact rank_le (Subsingleton.elim _ _)

Goal state after:
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 ⋯
⊢ closure ↑t = ⊤

Tactic:
Finset.coe_preimage

Goal state after:
G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
⊢ closure (Subtype.val ⁻¹' ↑s) = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : ¬0 < #{a | orderOf a = d}
⊢ False

Tactic:
not_lt,

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : #{a | orderOf a = d} ≤ 0
⊢ False
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClopen ↑(basicOpen e)

Tactic:
refine ⟨?_, (basicOpen e).2⟩

Goal state after:
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClosed ↑(basicOpen e)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ a * b = b * a

Tactic:
calc
    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.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommMonoid G
inst✝ : CommMonoid H
p : ℕ
a b : G
x✝¹ : a ∈ {g | ∃ k, g ^ p ^ k = 1}
x✝ : b ∈ {g | ∃ k, g ^ p ^ k = 1}
m : ℕ
hm : a ^ p ^ m = 1
n : ℕ
hn : b ^ p ^ n = 1
⊢ (a * b) ^ p ^ (m + n) = 1

Tactic:
mul_pow,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : CommMonoid G
inst✝ : CommMonoid H
p : ℕ
a b : G
x✝¹ : a ∈ {g | ∃ k, g ^ p ^ k = 1}
x✝ : b ∈ {g | ∃ k, g ^ p ^ k = 1}
m : ℕ
hm : a ^ p ^ m = 1
n : ℕ
hn : b ^ p ^ n = 1
⊢ a ^ p ^ (m + n) * b ^ p ^ (m + n) = 1
Module: Mathlib.Order.Atoms.Finite

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

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ IsStronglyAtomic αᵒᵈ
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr.inr
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Nat.card ↥f.ker * Nat.card ↥f.range ∣ Monoid.exponent M

Tactic:
apply h.mul_dvd_of_dvd_of_dvd

Goal state after:
case inr.inr.hm
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Nat.card ↥f.ker ∣ Monoid.exponent M

case inr.inr.hn
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Nat.card ↥f.range ∣ Monoid.exponent M
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
⊢ t.Nonempty →
    ((∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) →
      ((∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔ (↑(Finset.cons a t hat)).Pairwise fun i j ↦ I i ⊔ I j = ⊤)

Tactic:
h

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
⊢ ((∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) →
    ((∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔ (↑(Finset.cons a t hat)).Pairwise fun i j ↦ I i ⊔ I j = ⊤)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card ↥↑P = p ^ n
⊢ Nat.card ↥↑P ∣ Nat.card G

Tactic:
exact P.1.card_subgroup_dvd_card

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
⊢ ((p : ↥ps) → (P : Sylow (↑p) G) → ↥P) ≃* G

Tactic:
have hcomm : Pairwise fun p₁ p₂ : ps => ∀ x y : G, x ∈ P p₁ → y ∈ P p₂ → Commute x y := by
    rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
    have hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
    have hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
    have hne' : p₁ ≠ p₂ := by simpa using hne
    apply Subgroup.commute_of_normal_of_disjoint _ _ (hn (P p₁)) (hn (P p₂))
    apply IsPGroup.disjoint_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ((p : ↥ps) → (P : Sylow (↑p) G) → ↥P) ≃* G
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ 1 ∈ torsionOf R M m

Tactic:
h

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ 1 ∈ ⊤
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 : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
a : R
x : M
x✝ : x ∈ {x | ∃ a, a • x = 0}
b : S
h : b • x = 0
⊢ b • a • x = 0

Tactic:
smul_comm,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
a : R
x : M
x✝ : x ∈ {x | ∃ a, a • x = 0}
b : S
h : b • x = 0
⊢ a • b • x = 0
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: case smul
R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite (End R M) M
s : Finset M
hs : span (End R M) ↑s = ⊤
f : End (End R M) M
r : R
hr : ∀ m ∈ s, f m = r • m
m : M
g : End R M
x✝ : M
hx✝ : x✝ ∈ span (End R M) ↑s
h : ((toModuleEnd (End R M) M) r) x✝ = f x✝
⊢ g • ((toModuleEnd (End R M) M) r) x✝ = g • f x✝

Tactic:
h

Goal state after:
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
h : torsionBySet R M s = ⊤
x : M
⊢ x ∈ torsionBySet R M s

Tactic:
h

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
h : torsionBySet R M s = ⊤
x : M
⊢ x ∈ ⊤
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M✝ : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_5
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
x✝ y✝ : PolynomialModule R M✝
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
x : S
y : R[X]
⊢ ∀ (z : PolynomialModule R M), (x • y) • z = x • y • z

Tactic:
z

Goal state after:
ι : Type u_1
R : Type u_2
M✝ : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_5
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
x✝ y✝ : PolynomialModule R M✝
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
x : S
y : R[X]
z : PolynomialModule R M
⊢ (x • y) • z = x • y • z
Module: Mathlib.Order.JordanHolder

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

Tactic:
eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb ht hle

Goal state after:
case zero
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hle : s₁.length = 0
⊢ s₂.Equivalent 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 : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : S
x : ↥(torsion' R M S)
⊢ s • ↑x ∈ torsion' R M S

Tactic:
obtain ⟨x, a, h⟩ := x

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : S
x : M
a : S
h : a • x = 0
⊢ s • ↑⟨x, ⋯⟩ ∈ torsion' R M S