awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
| n
have rw : orderOf μ
Tactic: rw [hμ.eq_orderOf]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
| h.choose (p := fun (m : ℕ) ↦
        (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) %
      n ≡
    h.choose (p := fun (m : ℕ) ↦
      (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) [MOD
    orderOf hμ.toRootsOfUnity]
have enter : orderOf μ
Tactic: enter [2, 2]; rw [hμ.eq_orderOf]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
⊢ h.choose (p := fun (m : ℕ) ↦
        (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) %
      n ≡
    h.choose (p := fun (m : ℕ) ↦
      (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) [MOD
    orderOf hμ.toRootsOfUnity]
have e_self : h.choose (p := fun (m : ℕ) ↦
      (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) %
    orderOf μ ≡
  h.choose (p := fun (m : ℕ) ↦
    (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) [MOD
  orderOf hμ.toRootsOfUnity]
Tactic: conv => enter [2, 2]; rw [hμ.eq_orderOf]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
⊢ h.choose (p := fun (m : ℕ) ↦
        (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) %
      orderOf μ ≡
    h.choose (p := fun (m : ℕ) ↦
      (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) [MOD
    orderOf hμ.toRootsOfUnity]
have e_self : h.choose (p := fun (m : ℕ) ↦
      (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) %
    orderOf μ ≡
  h.choose (p := fun (m : ℕ) ↦
    (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) [MOD
  orderOf (↑(↑hμ.toRootsOfUnity : Sˣ) : S)]
Tactic: rw [← Subgroup.orderOf_coe, ← orderOf_units]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
hG' : ∃ (ζ : G'), IsPrimitiveRoot ζ (Nat.card G)
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
⊢ ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
have obtain : ∀ (ζ : G') (hζ : IsPrimitiveRoot ζ (Nat.card G)),
  ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
Tactic: obtain ⟨ζ, hζ⟩ := hG'
Cleared hypotheses: hG'
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
⊢ ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
have obtain : ∀ (g : G) (hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x),
  ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
Tactic: obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
⊢ orderOf ζ ∣ orderOf g
have rw : Nat.card G ∣ orderOf g
Tactic: rw [← hζ.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
rw : Nat.card G ∣ orderOf g
⊢ orderOf ζ ∣ orderOf g
have rw₁ : Nat.card G ∣ Nat.card G
Tactic: rw [← hζ.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
rw : Nat.card G ∣ orderOf g
rw₁ : Nat.card G ∣ Nat.card G
⊢ orderOf ζ ∣ orderOf g
have rw₂ : Fintype.card G ∣ Fintype.card G
Tactic: rw [← hζ.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
⊢ ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
have hζg : orderOf ζ ∣ orderOf g
Tactic: have hζg : orderOf ζ ∣ orderOf g := by
    rw [← hζ.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
⊢ ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
have hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
Tactic: have hφg : IsPrimitiveRoot (φ g) (Nat.card G) := by
    rwa [monoidHomOfForallMemZpowers_apply_gen hg hζg]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
⊢ ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
have h : Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
Tactic: use φ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
⊢ Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
have h : ∀ (ha : Eq.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')), a = 1
Tactic: contrapose ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
ha : Eq.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
⊢ a = 1
have hg₁ : Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) a
Tactic: specialize hg a
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg_1 : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg_1 hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
ha : Eq.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
hg : Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) a
⊢ a = 1
have hg₁ : ∃ (n : ℕ), g ^ n = a
Tactic: rw [← mem_powers_iff_mem_zpowers, Submonoid.mem_powers_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg_1 : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg_1 hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
ha : Eq.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
hg : ∃ (n : ℕ), g ^ n = a
⊢ a = 1
have h : ∀ (k : ℕ) (hk : g ^ k = a), a = 1
Tactic: obtain ⟨k, hk⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
ha : Eq.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
k : ℕ
hk : g ^ k = a
⊢ a = 1
have ha₁ : HPow.hPow (α := G') ((φ : (a : G) → G') g : G') k = 1
Tactic: rw [← hk, map_pow] at ha
Cleared hypotheses: ha, hk
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
k : ℕ
ha : HPow.hPow (α := G') ((φ : (a : G) → G') g : G') k = 1
hk : g ^ k = a
⊢ a = 1
have h : ∀ (l : ℕ) (ha : HPow.hPow (α := G') ((φ : (a : G) → G') g : G') (Nat.card G * l) = 1) (hk : g ^ (Nat.card G * l) = a),
  a = 1
Tactic: obtain ⟨l, rfl⟩ := (hφg.pow_eq_one_iff_dvd k).mp ha
Cleared hypotheses: k, ha, hk
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
l : ℕ
ha : HPow.hPow (α := G') ((φ : (a : G) → G') g : G') (Nat.card G * l) = 1
hk : g ^ (Nat.card G * l) = a
⊢ a = 1
have h : g ^ (Nat.card G * l) = 1
Tactic: rw [← hk, pow_mul, Nat.card_eq_fintype_card, pow_card_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
l : ℕ
ha : HPow.hPow (α := G') ((φ : (a : G) → G') g : G') (Nat.card G * l) = 1
hk : g ^ (Nat.card G * l) = a
h : g ^ (Nat.card G * l) = 1
⊢ a = 1
have h₁ : (g ^ Nat.card G) ^ l = 1
Tactic: rw [← hk, pow_mul, Nat.card_eq_fintype_card, pow_card_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
l : ℕ
ha : HPow.hPow (α := G') ((φ : (a : G) → G') g : G') (Nat.card G * l) = 1
hk : g ^ (Nat.card G * l) = a
h : g ^ (Nat.card G * l) = 1
h₁ : (g ^ Nat.card G) ^ l = 1
⊢ a = 1
have h₂ : (g ^ Fintype.card G) ^ l = 1
Tactic: rw [← hk, pow_mul, Nat.card_eq_fintype_card, pow_card_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
l : ℕ
ha : HPow.hPow (α := G') ((φ : (a : G) → G') g : G') (Nat.card G * l) = 1
hk : g ^ (Nat.card G * l) = a
h : g ^ (Nat.card G * l) = 1
h₁ : (g ^ Nat.card G) ^ l = 1
h₂ : (g ^ Fintype.card G) ^ l = 1
⊢ a = 1
have h₃ : HPow.hPow (α := G) 1 l = 1
Tactic: rw [← hk, pow_mul, Nat.card_eq_fintype_card, pow_card_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_7
G' : Type u_8
inst_1 : Group G
inst_2 : IsCyclic G
inst_3 : Finite G
inst_4 : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)
l : ℕ
ha : HPow.hPow (α := G') ((φ : (a : G) → G') g : G') (Nat.card G * l) = 1
hk : g ^ (Nat.card G * l) = a
h : g ^ (Nat.card G * l) = 1
h₁ : (g ^ Nat.card G) ^ l = 1
h₂ : (g ^ Fintype.card G) ^ l = 1
h₃ : HPow.hPow (α := G) 1 l = 1
⊢ a = 1
have h₄ : Eq.{u_7 + 1} (α := G) 1 1
Tactic: rw [← hk, pow_mul, Nat.card_eq_fintype_card, pow_card_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
M : Type u_7
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
hG : ∃ (ζ : M), IsPrimitiveRoot ζ n
a : ZMod n
ha : a ≠ 0
⊢ ∃ (φ : Multiplicative (ZMod n) →* Mˣ),
    Ne (α := Mˣ)
      ((φ : (a : Multiplicative (ZMod n)) → Mˣ)
          ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) a : Multiplicative (ZMod n)) :
        Mˣ)
      (1 : Mˣ)
have obtain : ∀ (ζ : M) (hζ : IsPrimitiveRoot ζ n),
  ∃ (φ : Multiplicative (ZMod n) →* Mˣ),
    Ne (α := Mˣ)
      ((φ : (a : Multiplicative (ZMod n)) → Mˣ)
          ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) a : Multiplicative (ZMod n)) :
        Mˣ)
      (1 : Mˣ)
Tactic: obtain ⟨ζ, hζ⟩ := hG
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
M : Type u_7
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ ∃ (φ : Multiplicative (ZMod n) →* Mˣ),
    Ne (α := Mˣ)
      ((φ : (a : Multiplicative (ZMod n)) → Mˣ)
          ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) a : Multiplicative (ZMod n)) :
        Mˣ)
      (1 : Mˣ)
have hc : n = Nat.card (Multiplicative (ZMod n))
Tactic: have hc : n = Nat.card (Multiplicative (ZMod n)) := by
    simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, card]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
⊢ ∃ (y : M), 0 ≠ y
have h : Ne.{u_4 + 1} (α := Submodule R M) ⊥ ⊤
Tactic: have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
h : Ne.{u_4 + 1} (α := Submodule R M) ⊥ ⊤
⊢ ∃ (y : M), 0 ≠ y
have contrapose! : ∀ (h : ∀ (y : M), 0 = y), Eq.{u_4 + 1} (α := Submodule R M) ⊥ ⊤
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
h : ∀ (y : M), 0 = y
⊢ Eq.{u_4 + 1} (α := Submodule R M) ⊥ ⊤
have h₁ : ∀ (x : M), Membership.mem (γ := Submodule R M) ⊥ x ↔ Membership.mem (γ := Submodule R M) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
inst_6 : RingHomSurjective σ
l : M →ₛₗ[σ] N
hl : Function.Bijective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
⊢ IsSimpleModule R M ↔ IsSimpleModule S N
have simp_rw : IsSimpleOrder.{u_4} (Submodule R M) ↔ IsSimpleOrder.{u_5} (Submodule S N)
Tactic: simp_rw [isSimpleModule_iff, (Submodule.orderIsoMapComapOfBijective l hl).isSimpleOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
S : Type u_3
inst : Ring S
M : Type u_4
inst_1 : AddCommGroup M
R : Type u_6
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
h : Function.Surjective.{u_6 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsSimpleModule R M ↔ IsSimpleModule S M
have rw : IsSimpleOrder.{u_4} (Submodule R M) ↔ IsSimpleModule S M
Tactic: rw [isSimpleModule_iff, isSimpleModule_iff,
    (Submodule.orderIsoOfAlgebraMapSurjective h).isSimpleOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
S : Type u_3
inst : Ring S
M : Type u_4
inst_1 : AddCommGroup M
R : Type u_6
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
h : Function.Surjective.{u_6 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw : IsSimpleOrder.{u_4} (Submodule R M) ↔ IsSimpleModule S M
⊢ IsSimpleModule R M ↔ IsSimpleModule S M
have rw₁ : IsSimpleOrder.{u_4} (Submodule R M) ↔ IsSimpleOrder.{u_4} (Submodule S M)
Tactic: rw [isSimpleModule_iff, isSimpleModule_iff,
    (Submodule.orderIsoOfAlgebraMapSurjective h).isSimpleOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
S : Type u_3
inst : Ring S
M : Type u_4
inst_1 : AddCommGroup M
R : Type u_6
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
h : Function.Surjective.{u_6 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw : IsSimpleOrder.{u_4} (Submodule R M) ↔ IsSimpleModule S M
rw₁ : IsSimpleOrder.{u_4} (Submodule R M) ↔ IsSimpleOrder.{u_4} (Submodule S M)
⊢ IsSimpleModule R M ↔ IsSimpleModule S M
have rw₂ : IsSimpleOrder.{u_4} (Submodule R M) ↔ IsSimpleOrder.{u_4} (Submodule R M)
Tactic: rw [isSimpleModule_iff, isSimpleModule_iff,
    (Submodule.orderIsoOfAlgebraMapSurjective h).isSimpleOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
m : Submodule R M
⊢ IsSimpleModule.{u_2, u_4} R ↥m ↔ IsAtom m
have rw : IsSimpleOrder.{u_4} (Submodule R ↥m) ↔ IsSimpleOrder.{u_4} (↑(Set.Iic m) : Type u_4)
Tactic: rw [← Set.isSimpleOrder_Iic_iff_isAtom, isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
m : Submodule R M
⊢ IsSimpleModule.{u_2, u_4} R (M ⧸ m) ↔ IsCoatom m
have rw : IsSimpleOrder.{u_4} (Submodule R (M ⧸ m)) ↔ IsSimpleOrder.{u_4} (↑(Set.Ici m) : Type u_4)
Tactic: rw [← Set.isSimpleOrder_Ici_iff_isCoatom, isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
A B : Submodule R M
hAB : A ≤ B
⊢ A ⋖ B ↔ IsSimpleModule.{u_2, u_4} R (↥B ⧸ Submodule.comap B.subtype A)
have hf : let f := B.mapIic;
f = B.mapIic
Tactic: set f : Submodule R B ≃o Set.Iic B := B.mapIic with hf
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
A B : Submodule R M
hAB : A ≤ B
f : Submodule R ↥B ≃o (↑(Set.Iic B) : Type u_4) := B.mapIic
hf : f = B.mapIic
⊢ A ⋖ B ↔ IsSimpleModule.{u_2, u_4} R (↥B ⧸ Submodule.comap B.subtype A)
have rw : IsCoatom (α := { x : Submodule R M // x ∈ Set.Iic B })
    (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic B) A hAB) ↔
  IsCoatom (α := (↑(Set.Iic B) : Type u_4))
    ((B.mapIic : (a : Submodule R ↥B) → (↑(Set.Iic B) : Type u_4)) (Submodule.comap B.subtype A) :
      (↑(Set.Iic B) : Type u_4))
Tactic: rw [covBy_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
S_1 : Type u_3
inst : Ring R
inst_1 : Ring S_1
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSimpleModule R M
S : Submodule R M
⊢ ∃ (a : M), S = R ∙ a
have inl : ∃ (a : M), Eq (α := Submodule R M) ⊥ (R ∙ a)
Tactic: obtain rfl | rfl := eq_bot_or_eq_top S
Cleared hypotheses: S