awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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 : 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)
⊢ orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
have rw : orderOf.{u_1} (G := G)
    ((noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
            sorry :
          (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
        g :
      G) ∣
  Fintype.card ((i_1 : { j : ι // j ≠ i }) → H (↑i_1 : ι))
Tactic: rw [← hgf, ← Fintype.card_pi]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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 : 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)
⊢ Membership.mem (γ := Subgroup G) ⊥ f
have hxp₁ : orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
Tactic: have hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H j) := by
    rw [← hgf, ← Fintype.card_pi]
    exact (orderOf_map_dvd _ _).trans orderOf_dvd_card
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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 : ι))
⊢ Membership.mem (γ := Subgroup G) ⊥ f
have intro : f = 1
Tactic: change f = 1
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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 : ι))
⊢ f = 1
have intro : orderOf f ∣ 1
Tactic: rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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 : ι))
⊢ orderOf f ∣ 1
have intro : ∀ (c : ℕ)
  (hc : Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = orderOf f * c),
  orderOf f ∣ 1
Tactic: obtain ⟨c, hc⟩ := Nat.dvd_gcd hxp hxi
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ orderOf f ∣ 1
have h : 1 = orderOf f * c
Tactic: use c
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ 1 = orderOf f * c
have h : 1 = Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i))
Tactic: rw [← hc]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ 1 = Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i))
have h : Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = 1
Tactic: symm
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = 1
have 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))
Tactic: rw [← Nat.coprime_iff_gcd_eq_one, Nat.coprime_fintype_prod_left_iff, Subtype.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ Function.Injective (α := (i : ι) → ↥(H i)) (β := G) (⇑(noncommPiCoprod hcomm) : (a : (i : ι) → ↥(H i)) → G)
have hind₁ : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (H i).subtype.range
Tactic: apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ Function.Injective (α := (i : ι) → ↥(H i)) (β := G) (⇑(noncommPiCoprod hcomm) : (a : (i : ι) → ↥(H i)) → G)
have hinj : ∀ (i : ι), Function.Injective (α := ↥(H i)) (β := G) (⇑(H i).subtype : (a : ↥(H i)) → G)
Tactic: apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ∞
⊢ n ≤ minOrder G ↔ ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s : Set G).Finite → n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)
have rw : (∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ (↑(orderOf a) : ℕ∞)) ↔
  ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s : Set G).Finite → n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)
Tactic: rw [le_minOrder]
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
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) : ℕ∞)
have 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) : ℕ∞)
Tactic: refine ⟨fun h s hs hs' ↦ ?_, fun h a ha ha' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
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) : ℕ∞)
⊢ (∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ (↑(orderOf a) : ℕ∞)) ↔
    ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s : Set G).Finite → n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)
have 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) : ℕ∞)
Tactic: refine ⟨fun h s hs hs' ↦ ?_, fun h a ha ha' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
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
⊢ n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)
have refine_1 : ∀ (a : G) (has : a ∈ s) (ha : a ≠ 1), n ≤ (↑(Nat.card.{u_1} ↥s) : ℕ∞)
Tactic: obtain ⟨a, has, ha⟩ := s.bot_or_exists_ne_one.resolve_left hs
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
⊢ minOrder (ZMod n) = (↑n.minFac : ℕ∞)
have this : Fact (1 < n)
Tactic: have : Fact (1 < n) := ⟨one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn, hn₁⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
have rw : ¬n ∣ n / n.minFac
Tactic: rw [Ne, ringChar.spec, ringChar.eq (ZMod n) n]
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ minOrder (ZMod n) = (↑n.minFac : ℕ∞)
have this₁ : 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)
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
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 : ℕ∞)
have refine_1 : LE.le (α := ℕ∞) (↑(Nat.card ↥(zmultiples (↑(n / n.minFac) : 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 _ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
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 : ℕ∞)
⊢ minOrder (ZMod n) = (↑n.minFac : ℕ∞)
have refine_2 : ∀ (s : AddSubgroup (ZMod n)) (hs : s ≠ ⊥),
  (↑s : Set (ZMod n)).Finite → LE.le (α := ℕ∞) (↑n.minFac : ℕ∞) (↑(Nat.card ↥s) : ℕ∞)
Tactic: refine ((minOrder_le_natCard (zmultiples_eq_bot.not.2 this) <| toFinite _).trans ?_).antisymm <|
    le_minOrder_iff_forall_addSubgroup.2 fun s hs _ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this_1 : Fact (1 < n)
this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
⊢ LE.le (α := ℕ∞) (↑(Nat.card ↥(zmultiples (↑(n / n.minFac) : ZMod n))) : ℕ∞) (↑n.minFac : ℕ∞)
have refine_1 : LE.le (α := ℕ∞) (↑(addOrderOf (G := ZMod n) (↑(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]
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
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 : ℕ∞)
⊢ LE.le (α := ℕ∞) (↑(Nat.card ↥(zmultiples (↑(n / n.minFac) : ZMod n))) : ℕ∞) (↑n.minFac : ℕ∞)
have refine_1₁ : LE.le (α := ℕ∞) (↑(n / n.gcd (n / n.minFac)) : ℕ∞) (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
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 : ℕ∞)
⊢ LE.le (α := ℕ∞) (↑(Nat.card ↥(zmultiples (↑(n / n.minFac) : ZMod n))) : ℕ∞) (↑n.minFac : ℕ∞)
have refine_1₂ : LE.le (α := ℕ∞) (↑(n / (n / n.minFac)) : ℕ∞) (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
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 : ℕ∞)
⊢ LE.le (α := ℕ∞) (↑(Nat.card ↥(zmultiples (↑(n / n.minFac) : ZMod n))) : ℕ∞) (↑n.minFac : ℕ∞)
have refine_1₃ : LE.le (α := ℕ∞) (↑n.minFac : ℕ∞) (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (hypothesis)
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
⊢ LE.le (α := ℕ∞) (↑n.minFac : ℕ∞) (↑(Nat.card ↥s) : ℕ∞)
have this₁ : Nontrivial ↥s
Tactic: haveI : Nontrivial s := s.bot_or_nontrivial.resolve_left hs
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ minOrder (ZMod n) = (↑n.minFac : ℕ∞)
have have : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
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
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
have : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
⊢ minOrder (ZMod n) = (↑n.minFac : ℕ∞)
have have₁ : ∀ (this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0), 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
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
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 : ℕ∞)
⊢ minOrder (ZMod n) = (↑n.minFac : ℕ∞)
have refine_1 : ∀ (this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0),
  LE.le (α := ℕ∞) (↑(Nat.card ↥(zmultiples (↑(n / n.minFac) : 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