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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : (matPolyEquiv m).coeff k = 0
⊢ (matPolyEquiv m).coeff k i j = 0

Tactic:
hk,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : (matPolyEquiv m).coeff k = 0
⊢ 0 i j = 0
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
⊢ P.coeff n ∈ I

Tactic:
let f := mapRingHom (Ideal.Quotient.mk I)

Goal state after:
case right
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
⊢ P.coeff n ∈ I
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ toENat p.spanRank = ⨅ s, ↑(↑s).card

Tactic:
rw [spanRank_toENat_eq_iInf_encard]
  rcases eq_or_ne (⨅ (s : Set M) (_ : span R s = p), s.encard) ⊤ with (h1 | h2)
  · rw [h1, eq_comm]; simp_rw [iInf_eq_top] at h1 ⊢
    exact fun s ↦ False.elim (Set.encard_ne_top_iff.mpr s.1.finite_toSet (h1 s.1 s.2))
  · simp_rw [← Set.encard_coe_eq_coe_finsetCard]
    apply le_antisymm
    · exact le_iInf fun s ↦ iInf₂_le (s.1 : Set M) s.2
    · refine le_iInf fun s ↦ le_iInf fun h ↦ ?_
      by_cases hs : s.Finite
      · exact iInf_le_of_le ⟨hs.toFinset, by simpa⟩ (by simp)
      · rw [Set.Infinite.encard_eq hs]
        exact OrderTop.le_top _

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.spanRank = ↑p.spanFinrank ↔ p.FG

Tactic:
spanFinrank,

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.spanRank = ↑(toNat p.spanRank) ↔ p.FG
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ↑(span R s).spanFinrank ≤ s.encard

Tactic:
spanFinrank,

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ↑(toNat (span R s).spanRank) ≤ s.encard
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ toENat #↑s = ↑p.spanFinrank

Tactic:
spanFinrank,

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ toENat #↑s = ↑(toNat p.spanRank)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ↑(∏ i, M.charmatrix (c i) i).natDegree < ↑(Fintype.card n - 1)

Tactic:
Nat.cast_lt

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ (∏ i, M.charmatrix (c i) i).natDegree < Fintype.card n - 1
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
hp : p.FG
⊢ (map f p).spanRank ≤ ↑p.spanFinrank

Tactic:
← Cardinal.lift_le.{u},

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
hp : p.FG
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{u, v} ↑p.spanFinrank
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ ↑(Fintype.card n - 1) < ↑(Fintype.card n)

Tactic:
Nat.cast_lt

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ Fintype.card n - 1 < Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ ↑(Fintype.card n - 1) < ↑(Fintype.card n)

Tactic:
Nat.cast_lt

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ Fintype.card n - 1 < Fintype.card n
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
⊢ N.spanRank ≤ (restrictScalars R N).spanRank

Tactic:
obtain ⟨s, hs, e⟩ := (N.restrictScalars R).exists_span_set_card_eq_spanRank
  obtain rfl : span S s = N :=
    le_antisymm (span_le.mpr (span_le.mp e.le :)) (e.ge.trans (span_le_restrictScalars R S s))
  grw [← hs, spanRank_span_le_card]

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
hI : I.FG
⊢ Submodule.spanRank (map f I) ≤ ↑(Submodule.spanFinrank I)

Tactic:
← Cardinal.lift_le.{u},

Goal state after:
R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
hI : I.FG
⊢ Cardinal.lift.{u, v} (Submodule.spanRank (map f I)) ≤ Cardinal.lift.{u, v} ↑(Submodule.spanFinrank I)
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
⊢ (mapRingHom f) (C r) = C (f r)

Tactic:
by
    simp only [coe_mapRingHom, map_C]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - X ^ k • C.mapMatrix (M ^ k)

Tactic:
hk,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - X ^ k • C.mapMatrix 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible (g.coeff 1)
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
a : R
⊢ Invertible ((X + C a).comp g).leadingCoeff

Tactic:
simpa [leadingCoeff, hg]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
f : R[X]
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hf : (map (algebraMap R A) f).Splits
e : A →ₐ[R] B
⊢ (map (algebraMap R B) f).Splits

Tactic:
← e.comp_algebraMap,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
f : R[X]
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hf : (map (algebraMap R A) f).Splits
e : A →ₐ[R] B
⊢ (map ((↑e).comp (algebraMap R A)) f).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
a : R
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) (a ::ₘ m)).prod
ha : a ∈ a ::ₘ m
⊢ ∃ a, eval a f = 0

Tactic:
exact ⟨a, by rw [hm]; simp⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ nonZeroDivisors R
p : S[X]
w✝ : R
hb₁ : w✝ ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w✝ • p
this✝¹ : IsDomain S := isDomain_of_le_nonZeroDivisors S hM
this✝ : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr (IsLocalization.injective S hM)
this : Function.Injective ⇑(mapRingHom (algebraMap R S)) :=
  Eq.mpr (id (congrArg (fun _a ↦ Function.Injective _a) (coe_mapRingHom (algebraMap R S))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a) (propext (map_injective_iff (algebraMap R S)))))
      (IsLocalization.injective S hM))
⊢ integerNormalization M p = 0 ↔ p = 0

Tactic:
← _root_.map_eq_zero_iff (mapRingHom (algebraMap R S)) this,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ nonZeroDivisors R
p : S[X]
w✝ : R
hb₁ : w✝ ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w✝ • p
this✝¹ : IsDomain S := isDomain_of_le_nonZeroDivisors S hM
this✝ : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr (IsLocalization.injective S hM)
this : Function.Injective ⇑(mapRingHom (algebraMap R S)) :=
  Eq.mpr (id (congrArg (fun _a ↦ Function.Injective _a) (coe_mapRingHom (algebraMap R S))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a) (propext (map_injective_iff (algebraMap R S)))))
      (IsLocalization.injective S hM))
⊢ (mapRingHom (algebraMap R S)) (integerNormalization M p) = 0 ↔ p = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
⊢ (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).coeff n ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
Polynomial.coeff_scaleRoots

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)
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
h : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
hf : LinearMap.lTensor M f = 0
this : Function.Exact ⇑f ⇑LinearMap.id
x : N
⊢ f x = 0 x

Tactic:
simpa using this (f x)

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

Tactic:
simp only [surjectiveOnStalks_iff_forall_maximal, surjective_localRingHom_iff]

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case refine_2
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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ r • ((r • 1) ⊗ₜ[R] t * x) = r • r • (1 ⊗ₜ[R] t * x)

Tactic:
← smul_tmul',

Goal state after:
case refine_2
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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ r • (r • 1 ⊗ₜ[R] t * x) = r • r • (1 ⊗ₜ[R] t * x)
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)
⊢ FaithfullyFlat A B

Tactic:
refine ⟨fun m hm ↦ ?_⟩
  rw [Ideal.smul_top_eq_map, IsLocalRing.eq_maximalIdeal hm]
  by_contra eqt
  have : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) ≤
      Submodule.restrictScalars A (IsLocalRing.maximalIdeal B) :=
    ((IsLocalRing.local_hom_TFAE (algebraMap A B)).out 0 2).mp ‹_›
  rw [eqt, top_le_iff, Submodule.restrictScalars_eq_top_iff] at this
  exact Ideal.IsPrime.ne_top' this

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 : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst✝¹] U
hfUopen : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ)
⊢ IsCompact (f ⁻¹' s ∩ U)

Tactic:
simpa [inter_union_distrib_left, inter_left_comm, inter_eq_right.2 (image_subset_range ..),
    hf.isCompact_iff, image_preimage_inter] using (hs hfUcomp hfUopen).inter_left hf.isClosed_range

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : QuasiSober Y
inst✝² : T0Space Y
inst✝¹ : QuasiSober X
inst✝ : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ coheight (f x) = coheight x

Tactic:
by
  rw [← coheight_orderIso (irreducibleSetEquivPoints (α := Y)).symm (f x),
    ← coheight_orderIso (irreducibleSetEquivPoints (α := X)).symm x,
    ← Topology.IsOpenEmbedding.coheight_map hf]
  congr
  ext : 1
  simp [closure_image_closure hf.continuous]

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 X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hs : IsConstructible s
⊢ IsConstructible (f '' s)

Tactic:
by
  induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    exact (hUcomp.image_of_isEmbedding hfopen.isEmbedding hfcomp).isConstructible <|
      hfopen.isOpenMap _ hUopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_sdiff_image hfopen.injective]
    exact (hfcomp.isConstructible hfopen.isOpen_range).sdiff hs'

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
x : α
⊢ x ∈ {x | closure {x} ∈ irreducibleComponents α} ↔ x ∈ {genericPoint α}

Tactic:
irreducibleComponents_eq_singleton

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
x : α
⊢ x ∈ {x | closure {x} ∈ {univ}} ↔ x ∈ {genericPoint α}
Module: Mathlib.Data.Nat.Factorization.LCM

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

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

pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Tactic:
· apply Finset.prod_dvd_prod_of_dvd; rintro p -; dsimp only; split_ifs with le
    · apply one_dvd
    · rw [factorization_lcm ha hb]; apply pow_dvd_pow; exact sup_le (not_le.1 le).le le_rfl

Goal state after:
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: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosed (Set.range (comap (RingHom.snd R S)))

Tactic:
range_comap_snd,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosed (zeroLocus ↑(RingHom.ker (RingHom.snd R S)))
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ (orbitZPowersEquiv a b).symm ↑k = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩

Tactic:
rw [orbitZPowersEquiv_symm_apply, ZMod.coe_intCast]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ⟨a, ⋯⟩ ^ (k % ↑(minimalPeriod (fun x ↦ a • x) b)) • ⟨b, ⋯⟩ = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
Nat.dvd_iff_mod_eq_zero

Goal state after:
case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
h : n % exponent G = 0
g : G
⊢ g ^ n = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Nat.card α

Tactic:
by
  rw [← Nat.card_zpowers, (zpowers g).eq_top_iff'.mpr hx, card_top]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.hnot
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ ¬(g ^ k) ^ p ^ t = 1

Tactic:
hk,

Goal state after:
case inr.hnot
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
k : ℕ
hg : g ^ (p ^ (exponent G).factorization p * k / p) ≠ 1
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ ¬(g ^ k) ^ p ^ t = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ (t + 1) = 1

Tactic:
← Nat.succ_eq_add_one,

Goal state after:
case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ t.succ = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite : (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
g : G
⊢ orderOf g ∈ t

Tactic:
rw [← Finset.mem_coe, ht]

Goal state after:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite : (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
g : G
⊢ orderOf g ∈ Set.range orderOf
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : IsPGroup p G
g : G
hg : g ≠ 1
k : ℕ
hk : orderOf g = p ^ k
hk0 : k = 0
⊢ orderOf g = 1

Tactic:
hk,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : IsPGroup p G
g : G
hg : g ≠ 1
k : ℕ
hk : orderOf g = p ^ k
hk0 : k = 0
⊢ p ^ k = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
h : H
g : G
hg : ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ ϕ g ^ p ^ k = 1

Tactic:
← ϕ.map_pow,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
h : H
g : G
hg : ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ ϕ (g ^ p ^ k) = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
h : H
g : G
hg : ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ ϕ (g ^ p ^ k) = 1

Tactic:
hk,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
h : H
g : G
hg : ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ ϕ 1 = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Finite (G ⧸ stabilizer G a)
this : (stabilizer G a).FiniteIndex
⊢ ∃ n, Nat.card ↑(orbit G a) = p ^ n

Tactic:
rw [Nat.card_congr ϕ]

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Finite (G ⧸ stabilizer G a)
this : (stabilizer G a).FiniteIndex
⊢ ∃ n, Nat.card (G ⧸ stabilizer G a) = p ^ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ ↑(∑ a, card { x // Quotient.mk'' x = a }) = ↑(∑ _a, 1)

Tactic:
Nat.cast_sum,

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ ∑ x, ↑(card { x_1 // Quotient.mk'' x_1 = x }) = ↑(∑ _a, 1)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝¹ : Fintype α
this✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
this : k = 0
⊢ card ↑(orbit G b) = 1

Tactic:
hk,

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝¹ : Fintype α
this✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
this : k = 0
⊢ p ^ k = 1