awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
enter : orderOf μ
| 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]

Tactic:
enter [2, 2]; rw [hμ.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
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]
⊢ 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]

Tactic:
conv => enter [2, 2]; rw [hμ.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
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)]
⊢ 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:
rw [← Subgroup.orderOf_coe, ← orderOf_units]

Premises used: orderOf_units, Subgroup.orderOf_coe
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 : Sˣ) : S)]

Tactic:
Nat.mod_modEq _ _

Premises used: Nat.mod_modEq
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 : Sˣ) : S)]

Tactic:
exact Nat.mod_modEq _ _

Premises used: Nat.mod_modEq
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
obtain :
  ∀ (ζ : G') (hζ : IsPrimitiveRoot ζ (Nat.card G)),
    ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
⊢ ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')

Tactic:
obtain ⟨ζ, hζ⟩ := hG'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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)
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')
⊢ ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')

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

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
rw₂ rw₃ : Fintype.card G ∣ Fintype.card G
⊢ orderOf ζ ∣ orderOf g

Tactic:
rw [← hζ.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]

Premises used: IsPrimitiveRoot.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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

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]
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
rwa rwa₁ rwa₂ rwa₃ : IsPrimitiveRoot ζ (Nat.card G)
⊢ IsPrimitiveRoot.{u_8} (M := G') ((φ : (a : G) → G') g : G') (Nat.card G)

Tactic:
rwa [monoidHomOfForallMemZpowers_apply_gen hg hζg]

Premises used: monoidHomOfForallMemZpowers_apply_gen
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
⊢ 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]
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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)
h : Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')
⊢ ∃ (φ : G →* G'), Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')

Tactic:
use φ
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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)
h : ∀ (ha : Eq.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')), a = 1
⊢ Ne.{u_8 + 1} (α := G') ((φ : (a : G) → G') a : G') (1 : G')

Tactic:
contrapose ha
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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')
⊢ Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) a

Tactic:
specialize hg a
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
⊢ ∃ (n : ℕ), g ^ n = a

Tactic:
rw [← mem_powers_iff_mem_zpowers, Submonoid.mem_powers_iff] at hg

Premises used: Submonoid.mem_powers_iff, mem_powers_iff_mem_zpowers
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
h : ∀ (k : ℕ) (hk : g ^ k = a), a = 1
⊢ a = 1

Tactic:
obtain ⟨k, hk⟩ := hg
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
⊢ HPow.hPow (α := G') ((φ : (a : G) → G') g : G') k = 1

Tactic:
rw [← hk, map_pow] at ha

Premises used: map_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
ha₁ : HPow.hPow (α := G') ((φ : (a : G) → G') g : G') k = 1
⊢ g ^ k = a

Tactic:
rw [← hk, map_pow] at ha

Premises used: map_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
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
⊢ a = 1

Tactic:
obtain ⟨l, rfl⟩ := (hφg.pow_eq_one_iff_dvd k).mp ha

Premises used: Iff.mp, IsPrimitiveRoot.pow_eq_one_iff_dvd, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
h₄ h₅ : Eq.{u_7 + 1} (α := G) 1 1
⊢ a = 1

Tactic:
rw [← hk, pow_mul, Nat.card_eq_fintype_card, pow_card_eq_one, one_pow]

Premises used: pow_card_eq_one, one_pow, pow_mul, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_7
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
hG : ∃ (ζ : M), IsPrimitiveRoot ζ n
a : ZMod n
ha : a ≠ 0
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ˣ)
⊢ ∃ (φ : 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
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_7
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ n = Nat.card (Multiplicative (ZMod n))

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, card]

Premises used: Fintype.card_multiplicative, ZMod.card, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_7
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ 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]
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_7
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
hc : n = Nat.card (Multiplicative (ZMod n))
⊢ Ne (α := Multiplicative (ZMod n))
    ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) a : Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))

Tactic:
simp only [ne_eq, ofAdd_eq_one, ha, not_false_eq_true]

Premises used: ne_eq, ofAdd_eq_one, not_false_eq_true
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_7
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
hc : n = Nat.card (Multiplicative (ZMod 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:
exact IsCyclic.exists_apply_ne_one
    (hc ▸ ⟨hζ.toRootsOfUnity.val, IsPrimitiveRoot.coe_units_iff.mp hζ⟩) <|
    by simp only [ne_eq, ofAdd_eq_one, ha, not_false_eq_true]

Premises used: IsCyclic.exists_apply_ne_one
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
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
inst_4 : Subsingleton R
⊢ IsSemisimpleRing R

Tactic:
(isSemisimpleModule_iff R R).mpr Subsingleton.instComplementedLattice

Premises used: Iff.mpr, Subsingleton.instComplementedLattice, isSemisimpleModule_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
e : R ≃+* S
⊢ IsSemisimpleRing R ↔ IsSemisimpleRing S

Tactic:
⟨fun _ ↦ e.isSemisimpleRing, fun _ ↦ e.symm.isSemisimpleRing⟩

Premises used: Iff.intro, RingEquiv.isSemisimpleRing, RingEquiv.symm
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
⊢ Ne.{u_4 + 1} (α := Submodule R M) ⊥ ⊤

Tactic:
have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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) ⊥ ⊤
contrapose! : ∀ (h : ∀ (y : M), 0 = y), Eq.{u_4 + 1} (α := Submodule R M) ⊥ ⊤
⊢ ∃ (y : M), 0 ≠ y

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
h₁ : ∀ (x : M), Membership.mem (γ := Submodule R M) ⊥ x ↔ Membership.mem (γ := Submodule R M) ⊤ x
⊢ Eq.{u_4 + 1} (α := Submodule R M) ⊥ ⊤

Tactic:
ext x
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
x : M
⊢ Membership.mem (γ := Submodule R M) ⊥ x ↔ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
simp [Submodule.mem_bot, Submodule.mem_top, h x]

Premises used: Submodule.mem_bot, Submodule.mem_top
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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)
simp_rw : IsSimpleOrder.{u_4} (Submodule R M) ↔ IsSimpleOrder.{u_5} (Submodule S N)
⊢ IsSimpleModule R M ↔ IsSimpleModule S N

Tactic:
simp_rw [isSimpleModule_iff, (Submodule.orderIsoMapComapOfBijective l hl).isSimpleOrder_iff]

Premises used: isSimpleModule_iff, OrderIso.isSimpleOrder_iff, Submodule.orderIsoMapComapOfBijective
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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)
rw₂ rw₃ : IsSimpleOrder.{u_4} (Submodule R M) ↔ IsSimpleOrder.{u_4} (Submodule R M)
⊢ IsSimpleModule R M ↔ IsSimpleModule S M

Tactic:
rw [isSimpleModule_iff, isSimpleModule_iff,
    (Submodule.orderIsoOfAlgebraMapSurjective h).isSimpleOrder_iff]

Premises used: Submodule.orderIsoOfAlgebraMapSurjective, isSimpleModule_iff, OrderIso.isSimpleOrder_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
⊢ IsSimpleModule R M ↔ IsSimpleModule R N

Tactic:
⟨(·.congr e.symm), (·.congr e)⟩

Premises used: LinearEquiv.symm, Iff.intro, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
rw : IsSimpleOrder.{u_4} (Submodule R ↥m) ↔ IsSimpleOrder.{u_4} (↑(Set.Iic m) : Type u_4)
⊢ IsSimpleModule.{u_2, u_4} R ↥m ↔ IsAtom m

Tactic:
rw [← Set.isSimpleOrder_Iic_iff_isAtom, isSimpleModule_iff]

Premises used: Set.isSimpleOrder_Iic_iff_isAtom, isSimpleModule_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
⊢ IsSimpleOrder.{u_4} (Submodule R ↥m) ↔ IsSimpleOrder.{u_4} (↑(Set.Iic m) : Type u_4)

Tactic:
m.mapIic.isSimpleOrder_iff

Premises used: Submodule.mapIic, OrderIso.isSimpleOrder_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
⊢ IsSimpleOrder.{u_4} (Submodule R ↥m) ↔ IsSimpleOrder.{u_4} (↑(Set.Iic m) : Type u_4)

Tactic:
exact m.mapIic.isSimpleOrder_iff

Premises used: Submodule.mapIic, OrderIso.isSimpleOrder_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
rw : IsSimpleOrder.{u_4} (Submodule R (M ⧸ m)) ↔ IsSimpleOrder.{u_4} (↑(Set.Ici m) : Type u_4)
⊢ IsSimpleModule.{u_2, u_4} R (M ⧸ m) ↔ IsCoatom m

Tactic:
rw [← Set.isSimpleOrder_Ici_iff_isCoatom, isSimpleModule_iff]

Premises used: isSimpleModule_iff, Set.isSimpleOrder_Ici_iff_isCoatom
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
⊢ IsSimpleOrder.{u_4} (Submodule R (M ⧸ m)) ↔ IsSimpleOrder.{u_4} (↑(Set.Ici m) : Type u_4)

Tactic:
(Submodule.comapMkQRelIso m).isSimpleOrder_iff

Premises used: OrderIso.isSimpleOrder_iff, Submodule.comapMkQRelIso
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
⊢ IsSimpleOrder.{u_4} (Submodule R (M ⧸ m)) ↔ IsSimpleOrder.{u_4} (↑(Set.Ici m) : Type u_4)

Tactic:
exact (Submodule.comapMkQRelIso m).isSimpleOrder_iff

Premises used: OrderIso.isSimpleOrder_iff, Submodule.comapMkQRelIso
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
⊢ let f := B.mapIic;
  f = B.mapIic

Tactic:
set f : Submodule R B ≃o Set.Iic B := B.mapIic with hf

Premises used: Submodule, Submodule.mapIic, Membership.mem, Subtype, Set.Iic