awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp_1 : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
hxp : orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
c : ℕ
hc : Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = orderOf f * c
h : 1 = Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i))
⊢ 1 = orderOf f * c

Tactic:
rw [← hc]
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp_1 : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
hxp : orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
c : ℕ
hc : Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = orderOf f * c
h : Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = 1
⊢ 1 = Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i))

Tactic:
symm
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp_1 : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
hxp : orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
c : ℕ
hc : Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = orderOf f * c
h :
  ∀ (a : ι) (b : a ≠ i),
    (Fintype.card.{u_3} (H (↑(Subtype.mk (p := fun (a : ι) ↦ a ≠ i) a b) : ι))).Coprime (Fintype.card.{u_3} (H i))
⊢ Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = 1

Tactic:
rw [← Nat.coprime_iff_gcd_eq_one, Nat.coprime_fintype_prod_left_iff, Subtype.forall]

Premises used: Nat.coprime_fintype_prod_left_iff, Subtype.forall, Nat.coprime_iff_gcd_eq_one
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp_1 : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
hxp : orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
c : ℕ
hc : Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = orderOf f * c
j : ι
h : j ≠ i
⊢ (Fintype.card.{u_3} (H (↑(Subtype.mk (p := fun (a : ι) ↦ a ≠ i) j h) : ι))).Coprime (Fintype.card.{u_3} (H i))

Tactic:
hcoprime h
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp_1 : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
hxp : orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
c : ℕ
hc : Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = orderOf f * c
j : ι
h : j ≠ i
⊢ (Fintype.card.{u_3} (H (↑(Subtype.mk (p := fun (a : ι) ↦ a ≠ i) j h) : ι))).Coprime (Fintype.card.{u_3} (H i))

Tactic:
exact hcoprime h
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun (i j : ι) ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
x : G
hx : x ∈ H i
y : G
hy : y ∈ H j
⊢ Commute (S := G) (((H i).subtype : (a : ↥(H i)) → G) (Subtype.mk (p := fun (x : G) ↦ x ∈ H i) x hx) : G)
    (((H j).subtype : (a : ↥(H j)) → G) (Subtype.mk (p := fun (x : G) ↦ x ∈ H j) y hy) : G)

Tactic:
hcomm hne x y hx hy
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun (i j : ι) ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
x : G
hx : x ∈ H i
y : G
hy : y ∈ H j
⊢ Commute (S := G) (((H i).subtype : (a : ↥(H i)) → G) (Subtype.mk (p := fun (x : G) ↦ x ∈ H i) x hx) : G)
    (((H j).subtype : (a : ↥(H j)) → G) (Subtype.mk (p := fun (x : G) ↦ x ∈ H j) y hy) : G)

Tactic:
exact hcomm hne x y hx hy
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun (i j : ι) ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
inst_1 : Finite ι
inst_2 : (i : ι) → Fintype ↥(H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_1} ↥(H i)).Coprime (Fintype.card.{u_1} ↥(H j))
⊢ iSupIndep H

Tactic:
simpa using
    MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype)
      (commute_subtype_of_commute hcomm) hcoprime

Premises used: Subgroup.subtype, MonoidHom.independent_range_of_coprime_order, Subgroup.commute_subtype_of_commute
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
inst_1 : Fintype ι
inst_2 : DecidableEq ι
hcomm : Pairwise fun (i j : ι) ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i : ι
y : ↥(H i)
⊢ (noncommPiCoprod hcomm : (a : (i : ι) → ↥(H i)) → G) (Pi.mulSingle (M := fun (i : ι) ↦ ↥(H i)) i y) = (↑y : G)

Tactic:
apply MonoidHom.noncommPiCoprod_mulSingle

Premises used: MonoidHom.noncommPiCoprod_mulSingle
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
inst_1 : Fintype ι
hcomm : Pairwise fun (i j : ι) ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
⊢ (noncommPiCoprod hcomm).range = ⨆ (i : ι), H i

Tactic:
simp [noncommPiCoprod, MonoidHom.noncommPiCoprod_range]

Premises used: MonoidHom.noncommPiCoprod_range, Subgroup.noncommPiCoprod
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
inst_1 : Fintype ι
hcomm : Pairwise fun (i j : ι) ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
hind₁ : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (H i).subtype.range
hinj : ∀ (i : ι), Function.Injective (α := ↥(H i)) (β := G) (⇑(H i).subtype : (a : ↥(H i)) → G)
⊢ Function.Injective (α := (i : ι) → ↥(H i)) (β := G) (⇑(noncommPiCoprod hcomm) : (a : (i : ι) → ↥(H i)) → G)

Tactic:
apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep

Premises used: MonoidHom.injective_noncommPiCoprod_of_iSupIndep
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
inst_1 : Fintype ι
hcomm : Pairwise fun (i j : ι) ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (H i).subtype.range

Tactic:
simpa using hind
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
inst_1 : Fintype ι
hcomm : Pairwise fun (i j : ι) ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
i : ι
⊢ Function.Injective (α := ↥(H i)) (β := G) (⇑(H i).subtype : (a : ↥(H i)) → G)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
inst_1 : Fintype ι
hcomm : Pairwise fun (i j : ι) ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
i : ι
⊢ Function.Injective (α := ↥(H i)) (β := G) (⇑(H i).subtype : (a : ↥(H i)) → G)

Tactic:
exact Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
inst_1 : Fintype ι
comm : Pairwise fun (i j : ι) ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
u : (i : ι) → ↥(H i)
⊢ Eq.{u_1 + 1} (α := G) ((noncommPiCoprod comm : (a : (i : ι) → ↥(H i)) → G) u : G)
    (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (↑(u i) : G)) ⋯ : G)

Tactic:
simp only [Subgroup.noncommPiCoprod, MonoidHom.noncommPiCoprod,
    coe_subtype, MonoidHom.coe_mk, OneHom.coe_mk]

Premises used: OneHom.coe_mk, Subgroup.coe_subtype, MonoidHom.coe_mk, MonoidHom.noncommPiCoprod, Subgroup.noncommPiCoprod
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
α : Type u_2
inst : Monoid α
n : ℕ∞
⊢ n ≤ minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ (↑(orderOf a) : ℕ∞)

Tactic:
simp [minOrder]

Premises used: Monoid.minOrder
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
α : Type u_2
inst : Monoid α
a : α
ha : a ≠ 1
ha' : IsOfFinOrder a
⊢ minOrder α ≤ (↑(orderOf a) : ℕ∞)

Tactic:
le_minOrder.1 le_rfl ha ha'

Premises used: le_rfl, Iff.mp, Monoid.le_minOrder
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
G : Type u_1
inst : Group G
n : ℕ∞
rw :
  (∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ (↑(orderOf a) : ℕ∞)) ↔
    ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s : Set G).Finite → n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)
⊢ n ≤ minOrder G ↔ ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s : Set G).Finite → n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)

Tactic:
rw [le_minOrder]

Premises used: Monoid.le_minOrder
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
G : Type u_1
inst : Group G
n : ℕ∞
⊢ (∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ (↑(orderOf a) : ℕ∞)) ↔
    ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s : Set G).Finite → n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)

Tactic:
⟨fun h s hs hs' ↦ ?_, fun h a ha ha' ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
G : Type u_1
inst : Group G
n : ℕ∞
refine_1 :
  ∀ (h : ∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ (↑(orderOf a) : ℕ∞)) (s : Subgroup G) (hs : s ≠ ⊥)
    (hs' : (↑s : Set G).Finite), n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)
refine_2 :
  ∀ (h : ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s : Set G).Finite → n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)) (a : G) (ha : a ≠ 1)
    (ha' : IsOfFinOrder a), n ≤ (↑(orderOf a) : ℕ∞)
⊢ (∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ (↑(orderOf a) : ℕ∞)) ↔
    ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s : Set G).Finite → n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)

Tactic:
refine ⟨fun h s hs hs' ↦ ?_, fun h a ha ha' ↦ ?_⟩
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
G : Type u_1
inst : Group G
n : ℕ∞
h : ∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ (↑(orderOf a) : ℕ∞)
s : Subgroup G
hs : s ≠ ⊥
hs' : (↑s : Set G).Finite
refine_1 : ∀ (a : G) (has : a ∈ s) (ha : a ≠ 1), n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)
⊢ n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)

Tactic:
obtain ⟨a, has, ha⟩ := s.bot_or_exists_ne_one.resolve_left hs

Premises used: Or.resolve_left, Subgroup.bot_or_exists_ne_one
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
G : Type u_1
inst : Group G
n : ℕ∞
h : ∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ (↑(orderOf a) : ℕ∞)
s : Subgroup G
hs : s ≠ ⊥
hs' : (↑s : Set G).Finite
a : G
has : a ∈ s
ha : a ≠ 1
⊢ n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)

Tactic:
(h ha <| finite_zpowers.1 <| hs'.subset <| zpowers_le.2 has).trans
        (WithTop.coe_le_coe.2 <| s.orderOf_le_card hs' has)

Premises used: Iff.mpr, finite_zpowers, Subgroup.zpowers_le, Set.Finite.subset, Iff.mp, LE.le.trans, WithTop.coe_le_coe, Subgroup.orderOf_le_card
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
G : Type u_1
inst : Group G
n : ℕ∞
h : ∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ (↑(orderOf a) : ℕ∞)
s : Subgroup G
hs : s ≠ ⊥
hs' : (↑s : Set G).Finite
a : G
has : a ∈ s
ha : a ≠ 1
⊢ n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)

Tactic:
exact
      (h ha <| finite_zpowers.1 <| hs'.subset <| zpowers_le.2 has).trans
        (WithTop.coe_le_coe.2 <| s.orderOf_le_card hs' has)

Premises used: Iff.mpr, finite_zpowers, Subgroup.zpowers_le, Set.Finite.subset, Iff.mp, LE.le.trans, WithTop.coe_le_coe, Subgroup.orderOf_le_card
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
G : Type u_1
inst : Group G
n : ℕ∞
h : ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s : Set G).Finite → n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)
a : G
ha : a ≠ 1
ha' : IsOfFinOrder a
⊢ n ≤ (↑(orderOf a) : ℕ∞)

Tactic:
simpa using h (zpowers_ne_bot.2 ha) ha'.finite_zpowers

Premises used: Iff.mpr, IsOfFinOrder.finite_zpowers, Subgroup.zpowers_ne_bot
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
hs : s ≠ ⊥
hs' : (↑s : Set G).Finite
⊢ minOrder G ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)

Tactic:
le_minOrder_iff_forall_subgroup.1 le_rfl hs hs'

Premises used: le_rfl, Monoid.le_minOrder_iff_forall_subgroup, Iff.mp
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
G : Type u_1
inst : Group G
inst_1 : IsMulTorsionFree G
⊢ minOrder G = ⊤

Tactic:
simpa [minOrder] using fun _ ↦ not_isOfFinOrder_of_isMulTorsionFree

Premises used: not_isOfFinOrder_of_isMulTorsionFree, Monoid.minOrder
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
G : Type u_1
inst : CommGroup G
⊢ minOrder G = ⊤ ↔ IsMulTorsionFree G

Tactic:
simp [minOrder, isMulTorsionFree_iff_not_isOfFinOrder]

Premises used: Monoid.minOrder, isMulTorsionFree_iff_not_isOfFinOrder
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
⊢ Fact (1 < n)

Tactic:
have : Fact (1 < n) := ⟨one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn, hn₁⟩⟩
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
rw : ¬n ∣ n / n.minFac
⊢ Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0

Tactic:
rw [Ne, ringChar.spec, ringChar.eq (ZMod n) n]

Premises used: ringChar.eq, Ne, ZMod, ringChar.spec
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ ¬n ∣ n / n.minFac

Tactic:
not_dvd_of_pos_of_lt (Nat.div_pos (minFac_le hn.bot_lt) n.minFac_pos)
        (div_lt_self hn.bot_lt (minFac_prime hn₁).one_lt)

Premises used: Nat.Prime.one_lt, Nat.minFac_le, Nat.div_lt_self, Nat.not_dvd_of_pos_of_lt, Nat.minFac_pos, Nat.div_pos, Nat.minFac_prime, Ne.bot_lt
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ ¬n ∣ n / n.minFac

Tactic:
exact
      not_dvd_of_pos_of_lt (Nat.div_pos (minFac_le hn.bot_lt) n.minFac_pos)
        (div_lt_self hn.bot_lt (minFac_prime hn₁).one_lt)

Premises used: Nat.Prime.one_lt, Nat.minFac_le, Nat.div_lt_self, Nat.not_dvd_of_pos_of_lt, Nat.minFac_pos, Nat.div_pos, Nat.minFac_prime, Ne.bot_lt
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0

Tactic:
have : (↑(n / n.minFac) : ZMod n) ≠ 0 := by
    rw [Ne, ringChar.spec, ringChar.eq (ZMod n) n]
    exact
      not_dvd_of_pos_of_lt (Nat.div_pos (minFac_le hn.bot_lt) n.minFac_pos)
        (div_lt_self hn.bot_lt (minFac_prime hn₁).one_lt)
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this_1 : Fact (1 < n)
this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
⊢ minOrder (ZMod n) = (↑n.minFac : ℕ∞)

Tactic:
((minOrder_le_natCard (zmultiples_eq_bot.not.2 this) <| toFinite _).trans ?_).antisymm <|
    le_minOrder_iff_forall_addSubgroup.2 fun s hs _ ↦ ?_

Premises used: Iff.mpr, LE.le.antisymm, Iff.not, AddMonoid.le_minOrder_iff_forall_addSubgroup, Set.toFinite, LE.le.trans, AddMonoid.minOrder_le_natCard, AddSubgroup.zmultiples_eq_bot
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this_1 : Fact (1 < n)
this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
refine_1 : LE.le (α := ℕ∞) (↑(Nat.card ↥(zmultiples (↑(n / n.minFac) : ZMod n))) : ℕ∞) (↑n.minFac : ℕ∞)
refine_2 :
  ∀ (s : AddSubgroup (ZMod n)) (hs : s ≠ ⊥),
    (↑s : Set (ZMod n)).Finite → LE.le (α := ℕ∞) (↑n.minFac : ℕ∞) (↑(Nat.card ↥s) : ℕ∞)
⊢ minOrder (ZMod n) = (↑n.minFac : ℕ∞)

Tactic:
refine ((minOrder_le_natCard (zmultiples_eq_bot.not.2 this) <| toFinite _).trans ?_).antisymm <|
    le_minOrder_iff_forall_addSubgroup.2 fun s hs _ ↦ ?_

Premises used: Iff.mpr, LE.le.antisymm, Iff.not, AddMonoid.le_minOrder_iff_forall_addSubgroup, Set.toFinite, LE.le.trans, AddMonoid.minOrder_le_natCard, AddSubgroup.zmultiples_eq_bot
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this_1 : Fact (1 < n)
this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
refine_1 : LE.le (α := ℕ∞) (↑(addOrderOf (G := ZMod n) (↑(n / n.minFac) : ZMod n)) : ℕ∞) (↑n.minFac : ℕ∞)
refine_1₁ : LE.le (α := ℕ∞) (↑(n / n.gcd (n / n.minFac)) : ℕ∞) (↑n.minFac : ℕ∞)
refine_1₂ : LE.le (α := ℕ∞) (↑(n / (n / n.minFac)) : ℕ∞) (↑n.minFac : ℕ∞)
refine_1₃ refine_1₄ : LE.le (α := ℕ∞) (↑n.minFac : ℕ∞) (↑n.minFac : ℕ∞)
⊢ LE.le (α := ℕ∞) (↑(Nat.card ↥(zmultiples (↑(n / n.minFac) : ZMod n))) : ℕ∞) (↑n.minFac : ℕ∞)

Tactic:
rw [Nat.card_zmultiples, ZMod.addOrderOf_coe _ hn,
      gcd_eq_right (div_dvd_of_dvd n.minFac_dvd), Nat.div_div_self n.minFac_dvd hn]

Premises used: ZMod.addOrderOf_coe, Nat.card_zmultiples, Nat.minFac_dvd, Nat.div_dvd_of_dvd, Nat.div_div_self, Nat.gcd_eq_right
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this_1 : Fact (1 < n)
this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
h : (↑s : Set (ZMod n)).Finite
⊢ Nontrivial ↥s

Tactic:
haveI : Nontrivial s := s.bot_or_nontrivial.resolve_left hs
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this_1 : Fact (1 < n)
this_2 : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
h : (↑s : Set (ZMod n)).Finite
this : Nontrivial ↥s
⊢ LE.le (α := ℕ∞) (↑n.minFac : ℕ∞) (↑(Nat.card ↥s) : ℕ∞)

Tactic:
WithTop.coe_le_coe.2 <| minFac_le_of_dvd Finite.one_lt_card <|
      (card_addSubgroup_dvd_card _).trans n.card_zmod.dvd

Premises used: Iff.mpr, Nat.minFac_le_of_dvd, Eq.dvd, AddSubgroup.card_addSubgroup_dvd_card, Finite.one_lt_card, Nat.card_zmod, WithTop.coe_le_coe, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this_1 : Fact (1 < n)
this_2 : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
h : (↑s : Set (ZMod n)).Finite
this : Nontrivial ↥s
⊢ LE.le (α := ℕ∞) (↑n.minFac : ℕ∞) (↑(Nat.card ↥s) : ℕ∞)

Tactic:
exact WithTop.coe_le_coe.2 <| minFac_le_of_dvd Finite.one_lt_card <|
      (card_addSubgroup_dvd_card _).trans n.card_zmod.dvd

Premises used: Iff.mpr, Nat.minFac_le_of_dvd, Eq.dvd, AddSubgroup.card_addSubgroup_dvd_card, Finite.one_lt_card, Nat.card_zmod, WithTop.coe_le_coe, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
have : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
have₁ : ∀ (this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0), minOrder (ZMod n) = (↑n.minFac : ℕ∞)
have₂ : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
have₃ have₄ : ∀ (this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0), minOrder (ZMod n) = (↑n.minFac : ℕ∞)
refine_1 :
  ∀ (this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0),
    LE.le (α := ℕ∞) (↑(Nat.card ↥(zmultiples (↑(n / n.minFac) : ZMod n))) : ℕ∞) (↑n.minFac : ℕ∞)
refine_2 refine_2₁ :
  ∀ (this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0) (s : AddSubgroup (ZMod n)) (hs : s ≠ ⊥),
    (↑s : Set (ZMod n)).Finite → LE.le (α := ℕ∞) (↑n.minFac : ℕ∞) (↑(Nat.card ↥s) : ℕ∞)
⊢ minOrder (ZMod n) = (↑n.minFac : ℕ∞)

Tactic:
classical
  have : (↑(n / n.minFac) : ZMod n) ≠ 0 := by
    rw [Ne, ringChar.spec, ringChar.eq (ZMod n) n]
    exact
      not_dvd_of_pos_of_lt (Nat.div_pos (minFac_le hn.bot_lt) n.minFac_pos)
        (div_lt_self hn.bot_lt (minFac_prime hn₁).one_lt)
  refine ((minOrder_le_natCard (zmultiples_eq_bot.not.2 this) <| toFinite _).trans ?_).antisymm <|
    le_minOrder_iff_forall_addSubgroup.2 fun s hs _ ↦ ?_
  · rw [Nat.card_zmultiples, ZMod.addOrderOf_coe _ hn,
      gcd_eq_right (div_dvd_of_dvd n.minFac_dvd), Nat.div_div_self n.minFac_dvd hn]
  · haveI : Nontrivial s := s.bot_or_nontrivial.resolve_left hs
    exact WithTop.coe_le_coe.2 <| minFac_le_of_dvd Finite.one_lt_card <|
      (card_addSubgroup_dvd_card _).trans n.card_zmod.dvd

Premises used: ZMod.addOrderOf_coe, Iff.mpr, Nat.card_zmultiples, Nat.minFac_le_of_dvd, Eq.dvd, Nat.minFac_dvd, AddSubgroup.card_addSubgroup_dvd_card, AddMonoid.le_minOrder_iff_forall_addSubgroup, Finite.one_lt_card, Nat.card_zmod, WithTop.coe_le_coe, Nat.div_dvd_of_dvd, Nat.div_div_self, Nat.gcd_eq_right, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.Order.Min
Goal:
p : ℕ
hp : Nat.Prime p
rw : Eq (α := ℕ∞) (↑p.minFac : ℕ∞) (↑p : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑p : ℕ∞) (↑p : ℕ∞)
⊢ minOrder (ZMod p) = (↑p : ℕ∞)

Tactic:
rw [ZMod.minOrder hp.ne_zero hp.ne_one, hp.minFac_eq]

Premises used: Nat.Prime.minFac_eq, ZMod.minOrder, Nat.Prime.ne_one, Nat.Prime.ne_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
x : G
rw : IsFixedPt.{u_1} (α := G) (fun (x_1 : G) ↦ x * x_1)^[n] 1 ↔ x ^ n = 1
rw₁ : Eq.{u_1 + 1} (α := G) ((fun (x_1 : G) ↦ x * x_1)^[n] 1) 1 ↔ x ^ n = 1
rw₂ rw₃ : x ^ n = 1 ↔ x ^ n = 1
⊢ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ↔ x ^ n = 1

Tactic:
rw [IsPeriodicPt, IsFixedPt, mul_left_iterate_apply_one]

Premises used: Function.IsPeriodicPt, mul_left_iterate_apply_one, Function.IsFixedPt