mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: 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
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)

Tactic:
refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩

Goal state after:
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

case refine_2
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 ∈ closure[inst✝] s ↓∩ s → x ∈ Subtype.val ⁻¹' ⋃ x, ⋃ (h : x ∈ s), U x h
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: 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
⊢ [IsLocallyClosed s, IsOpen[inst✝] (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)].TFAE

Tactic:
tfae_have 4 → 5
  | H => by
    choose U hxU hU e using H
    refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
    · rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩
      exact e y hy ⟨hxU, x.2⟩
    · exact (subset_iUnion₂ _ _ <| hxU x ·)

Goal state after:
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
tfae_4_to_5 :
  (∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s) →
    IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
⊢ [IsLocallyClosed s, IsOpen[inst✝] (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)].TFAE
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case inr
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
⊢ IsEmbedding f

Tactic:
let f₀ : X → Set.range f := fun x ↦ ⟨f x, ⟨x, rfl⟩⟩
    suffices IsEmbedding f₀ from IsEmbedding.subtypeVal.comp this
    have hU'' : (⨆ i, (U i).comap ⟨Subtype.val, continuous_subtype_val⟩ :
        Opens (Set.range f)) = ⊤ := by
      rw [← top_le_iff]
      simpa [Set.range_subset_iff, SetLike.le_def] using hU
    refine this _ ?_ _ ?_ V iV hiV ?_ ?_ hU''
    · fun_prop
    · rw [hU'']; simp
    · exact hV
    · exact fun i ↦ IsEmbedding.of_comp (by fun_prop) continuous_subtype_val (hV' i)

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ f x ∈ f '' s

Tactic:
exact hU hx

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' U)

pp: case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f ⁻¹' V ⊆ s

pp: case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' V)

Tactic:
· rw [h.isCompact_iff]
    convert! hU''
    rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
    exact hU.trans (Set.image_subset_range _ _)

Goal state after:
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f ⁻¹' V ⊆ s

case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' V)
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
⊢ Opens.IsBasis {U | IsCompact ↑U}

Tactic:
by
  dsimp only [TopologicalSpace.Opens.IsBasis]
  convert! isTopologicalBasis (X := X)
  ext s
  exact ⟨fun ⟨V, hV, heq⟩ ↦ heq ▸ ⟨V.2, hV⟩, fun h ↦ ⟨⟨s, h.1⟩, h.2, rfl⟩⟩

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i

Tactic:
dsimp only [sequenceOfCofinals, Nat.add]
  rw [Encodable.encodek]
  apply Cofinal.above_mem

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ topologicalKrullDim X ≤ 0

Tactic:
by
  refine krullDim_nonpos_iff_forall_isMax.mpr fun Z Y h ↦ (h.antisymm' fun x hx ↦ ?_).le
  obtain ⟨z, hz⟩ := Z.2.nonempty
  rwa [DiscreteTopology.isDiscrete.subsingleton_of_isPreirreducible Y.2.isPreirreducible hx (h hz)]

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑W
hV : IsClosed V
⊢ QuasiSober ↑(W ∩ V)

Tactic:
refine QuasiSober.of_subset ?_ (Set.inter_subset_left : W ∩ V ⊆ W)
  rw [Subtype.preimage_coe_self_inter W V]
  exact IsClosed.preimage_val hV

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑V
hW : IsClosed W
⊢ QuasiSober ↑(W ∩ V)

Tactic:
rw [inter_comm]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑V
hW : IsClosed W
⊢ QuasiSober ↑(V ∩ W)
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
h : ∀ (f : AddAut (ZMod n)) (x : ZMod n), f 1 * x = f x
f g : AddAut (ZMod n)
⊢ Additive.ofMul (Units.mkOfMulEqOne ((f + g) 1) ((-(f + g)) 1) ⋯) =
    Additive.ofMul (Units.mkOfMulEqOne (f 1) ((-f) 1) ⋯) + Additive.ofMul (Units.mkOfMulEqOne (g 1) ((-g) 1) ⋯)

Tactic:
simp [← Additive.toMul_symm_eq, Equiv.symm_apply_eq, Units.ext_iff, h]

Goal state after:
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

Tactic:
nth_rewrite 2 [← prod_factorization_pow_eq_self hb]

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ b.factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ a.factorizationLCMRight b ∣ b

Tactic:
rcases eq_or_ne a 0 with rfl | ha
  · simp [factorizationLCMRight]
  rcases eq_or_ne b 0 with rfl | hb
  · simp only [dvd_zero]
  nth_rewrite 2 [← prod_factorization_pow_eq_self hb]
  rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
  · 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
  · intro p hp; rw [mem_support_iff] at hp ⊢
    rw [factorization_lcm ha hb]; exact (lt_sup_iff.mpr <| .inr <| Nat.pos_of_ne_zero hp).ne'
  · intros; rw [pow_zero]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring A
inst✝¹⁴ : CommSemiring B
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
S : Type u_5
T : Type u_6
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulCommClass S A M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulCommClass T A M
r : S
D : Derivation R A M
⊢ (r • ↑D) 1 = 0

Tactic:
LinearMap.smul_apply,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring A
inst✝¹⁴ : CommSemiring B
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
S : Type u_5
T : Type u_6
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulCommClass S A M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulCommClass T A M
r : S
D : Derivation R A M
⊢ r • ↑D 1 = 0
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ a • b • D a + a • a • D b = a • (a • D b + b • D a)

Tactic:
smul_add,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ a • b • D a + a • a • D b = a • a • D b + a • b • D a
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: 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 b : K
⊢ D (a / b) = b⁻¹ ^ 2 • (b • D a - a • D b)

Tactic:
simp only [div_eq_mul_inv, leibniz, leibniz_inv, inv_pow, neg_smul, smul_neg, smul_smul, add_comm,
    sub_eq_add_neg, smul_add]

Goal state after:
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 b : K
⊢ b⁻¹ • D a + -((a * (b ^ 2)⁻¹) • D b) = ((b ^ 2)⁻¹ * b) • D a + -(((b ^ 2)⁻¹ * a) • D b)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ IsCyclic α

Tactic:
by
  have : Finite α := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)
  have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp (h ▸ hp.1.one_lt)
  obtain ⟨g, hg⟩ : ∃ g : α, g ≠ 1 := exists_ne 1
  exact ⟨g, fun g' ↦ mem_zpowers_of_prime_card h hg⟩

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

Goal state before:
pp: case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
⊢ IsOpenMap fun a ↦ sigmaToPi R ⟨i, a⟩

Tactic:
simp only [sigmaToPi_apply, PrimeSpectrum.isTopologicalBasis_basic_opens.isOpenMap_iff]

Goal state after:
case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
⊢ ∀ s ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen ((fun a ↦ comap (Pi.evalRingHom R i) a) '' s)
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
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
hg : g ^ (k * p ^ t) ≠ 1
ht : (exponent G).factorization p = t.succ
⊢ ¬(g ^ k) ^ p ^ t = 1

Tactic:
pow_mul

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 : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
hg : (g ^ k) ^ p ^ t ≠ 1
ht : (exponent G).factorization p = t.succ
⊢ ¬(g ^ k) ^ p ^ t = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

Tactic:
let ⟨m, hm⟩ := Nat.gcd_dvd_right n (Fintype.card α)

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

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ n, Nat.card G ∣ p ^ n

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨n, hn⟩ ↦ of_card_dvd_pow hn⟩

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
⊢ ∃ n, Nat.card G ∣ p ^ n
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
⊢ #{a | orderOf a = d} = φ d

Tactic:
rcases Finset.card_pos.1 hpos with ⟨a, ha'⟩

Goal state after:
case h.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
⊢ #{a | orderOf a = d} = φ d
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ Nat.card ↑(orbit G P)
⊢ 1 ≡ 0 [MOD p]

Tactic:
calc
      1 = Nat.card (fixedPoints P (orbit G P)) := ?_
      _ ≡ Nat.card (orbit G P) [MOD p] := (P.2.card_modEq_card_fixedPoints (orbit G P)).symm
      _ ≡ 0 [MOD p] := Nat.modEq_zero_iff_dvd.mpr h

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ Nat.card ↑(orbit G P)
⊢ 1 = Nat.card ↑(fixedPoints ↥↑P ↑(orbit G P))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ I.radical ∈ minimalPrimes R

Tactic:
rw [← vanishingIdeal_zeroLocus_eq_radical]
  conv_lhs => rw [← (isClosed_zeroLocus _).closure_eq]
  exact vanishingIdeal_mem_minimalPrimes.symm

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ IsClosed {closedPoint R}

Tactic:
rw [PrimeSpectrum.isClosed_singleton_iff_isMaximal, closedPoint]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ { asIdeal := maximalIdeal R, isPrime := ⋯ }.asIdeal.IsMaximal
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hα : Nontrivial α
⊢ Nat.Prime (Nat.card α)

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)

Goal state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hα : Nontrivial α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Nat.Prime (Nat.card α)
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
tG : IsMulTorsion G
g : G
⊢ IsOfFinOrder (f g)

Tactic:
exact f.isOfFinOrder (tG g)

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : ExponentExists G
g : G
⊢ IsOfFinOrder g

Tactic:
obtain ⟨n, npos, hn⟩ := h
  exact isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, hn g⟩

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ ∃ n, orderOf g = p ^ n

Tactic:
← orderOf_submonoid,

Goal state after:
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ ∃ n, orderOf ↑g = p ^ n
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
⊢ IsCyclic (M × N) ↔ IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)

Tactic:
refine ⟨fun h ↦ ⟨isCyclic_left_of_prod M N, isCyclic_right_of_prod M N, ?_⟩, fun ⟨hM, hN, h⟩ ↦ ?_⟩
  · cases (finite_or_infinite M).symm
    · cases subsingleton_or_nontrivial N; · simp
      exact (not_isCyclic_prod_of_infinite_nontrivial M N h).elim
    cases (finite_or_infinite N).symm
    · cases subsingleton_or_nontrivial M; · simp
      rw [(MulEquiv.prodComm ..).isCyclic] at h
      exact (not_isCyclic_prod_of_infinite_nontrivial N M h).elim
    apply coprime_card_of_isCyclic_prod
  · let f := MonoidHom.snd M N
    let e : f.ker ≃* M := by
      rw [MonoidHom.ker_snd]
      exact ((Subgroup.prodEquiv ..).trans .prodUnique).trans Subgroup.topEquiv
    let _ := hM.commGroup; let _ := hN.commGroup
    rw [← e.isCyclic] at hM
    rw [← Nat.card_congr e.toEquiv] at h
    exact isCyclic_of_coprime_card_ker f h Prod.snd_surjective

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

Goal state before:
pp: case h
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
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ (b * a) • (x + y) = 0

Tactic:
smul_add,

Goal state after:
case h
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
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ (b * a) • x + (b * a) • y = 0
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
f✝ : End (End R M) M
s : Finset M
x : ↥s →₀ M := Finsupp.equivFunOnFinite.symm fun x ↦ ↑x
w✝ : Submodule R (↥s →₀ M)
h : IsCompl (R ∙ x) w✝
p : (↥s →₀ M) →ₗ[R] ↥s →₀ M := (R ∙ x).projection w✝ h
f : End (End R (↥s →₀ M)) (↥s →₀ M) := (End.ringHomEndFinsupp ↥s) f✝
this✝ : f (p • x) = f x
this : f x ∈ R ∙ x
r : R
hr : r • x = f x
m : M
hm : m ∈ s
⊢ f✝ m = r • m

Tactic:
by simpa [x] using! congr($hr ⟨m, hm⟩).symm

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

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
p : R[X]
f g : PolynomialModule R M
e₁ : (map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • (map R' f✝) f
e₂ : (map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • (map R' f✝) g
⊢ (map R' f✝) (p • (f + g)) = Polynomial.map (algebraMap R R') p • (map R' f✝) (f + g)

Tactic:
smul_add,

Goal state after:
case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
p : R[X]
f g : PolynomialModule R M
e₁ : (map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • (map R' f✝) f
e₂ : (map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • (map R' f✝) g
⊢ (map R' f✝) (p • f + p • g) = Polynomial.map (algebraMap R R') p • (map R' f✝) (f + g)
Module: Mathlib.Algebra.Polynomial.Module.Basic

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

Tactic:
smul_add,

Goal state after:
case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ : (eval r) (p • f) = Polynomial.eval r p • (eval r) f
e₂ : (eval r) (p • g) = Polynomial.eval r p • (eval r) g
⊢ (eval r) (p • f + p • g) = Polynomial.eval r p • (eval r) (f + g)