awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
⊢ ∃ (a : ↥H), (↑a : G) * x = q

Tactic:
Quotient.eq.mp hx

Premises used: Set.Mem, setOf, MulAction.orbit, Iff.mp, Set.range, Quotient.eq
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
obtain : ∀ (a : ↥H) (ha : (↑a : G) * x = q), ∃ (a : ↥H), x = (↑a : G) * q
⊢ ∃ (a : ↥H), x = (↑a : G) * q

Tactic:
obtain ⟨a, ha⟩ : ∃ a : H, a * x = q := Quotient.eq.mp hx

Premises used: Iff.mp, Quotient.eq
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
a : ↥H
ha : (↑a : G) * x = q
⊢ (↑a : G)⁻¹ ∈ H

Tactic:
simp
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
a : ↥H
ha : (↑a : G) * x = q
⊢ ∃ (a : ↥H), x = (↑a : G) * q

Tactic:
exact ⟨⟨a⁻¹, by simp⟩, eq_inv_mul_of_mul_eq ha⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
obtain : ∀ (a : ↥H) (ha : x = (↑a : G) * q), ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y
⊢ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y

Tactic:
obtain ⟨a, ha⟩ : ∃ a : H, x = a * q := by
    obtain ⟨a, ha⟩ : ∃ a : H, a * x = q := Quotient.eq.mp hx
    exact ⟨⟨a⁻¹, by simp⟩, eq_inv_mul_of_mul_eq ha⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
a : ↥H
ha : x = (↑a : G) * q
⊢ x = (↑a : G) * q * 1

Tactic:
simpa using ha
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
a : ↥H
ha : x = (↑a : G) * q
⊢ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y

Tactic:
exact ⟨a.1, a.2, ⟨1, Subgroup.one_mem K, by simpa using ha⟩⟩
-- Module: Mathlib.GroupTheory.EckmannHilton
Goal:
X : Type u
_G : MulOneClass X
⊢ IsUnital (fun (x1 x2 : X) ↦ x1 * x2) 1

Tactic:
IsUnital.mk { left_id := MulOneClass.one_mul,
                right_id := MulOneClass.mul_one }

Premises used: Std.LawfulIdentity.mk, EckmannHilton.IsUnital.mk
-- Module: Mathlib.GroupTheory.EckmannHilton
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ e₁ = e₂

Tactic:
simpa only [h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id] using distrib e₂ e₁ e₁ e₂

Premises used: Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id
-- Module: Mathlib.GroupTheory.EckmannHilton
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
h : ∀ (a b : X), m₁ a b = m₂ a b
⊢ m₁ = m₂

Tactic:
funext a b
-- Module: Mathlib.GroupTheory.EckmannHilton
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)

Tactic:
simp only [one h₁ h₂ distrib, h₂.left_id, h₂.right_id]

Premises used: Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id, EckmannHilton.one
-- Module: Mathlib.GroupTheory.EckmannHilton
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)

Tactic:
{ simp only [one h₁ h₂ distrib, h₂.left_id, h₂.right_id] }

Premises used: Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id, EckmannHilton.one
-- Module: Mathlib.GroupTheory.EckmannHilton
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ (m₂ a e₁) (m₂ e₁ b) = m₂ a b

Tactic:
simp only [distrib, h₁.left_id, h₁.right_id]

Premises used: Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id
-- Module: Mathlib.GroupTheory.EckmannHilton
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
m₃ : m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)
m₄ : m₁ (m₂ a e₁) (m₂ e₁ b) = m₂ a b
⊢ m₁ a b = m₂ a b

Tactic:
calc
    m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) := by
      { simp only [one h₁ h₂ distrib, h₂.left_id, h₂.right_id] }
    _ = m₂ a b := by simp only [distrib, h₁.left_id, h₁.right_id]
-- Module: Mathlib.GroupTheory.EckmannHilton
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₂ a b = m₂ b a

Tactic:
simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib e₂ a b e₂

Premises used: Std.LawfulRightIdentity.right_id, EckmannHilton.mul, Std.LawfulLeftIdentity.left_id
-- Module: Mathlib.GroupTheory.EckmannHilton
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b c : X
⊢ m₂ (m₂ a b) c = m₂ a (m₂ b c)

Tactic:
simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib a b e₂ c

Premises used: Std.LawfulRightIdentity.right_id, EckmannHilton.mul, Std.LawfulLeftIdentity.left_id
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
⊢ AddMonoid.exponent.{u} (Additive G) = exponent G

Tactic:
rfl

Premises used: Monoid.ExponentExists, Additive, Monoid.exponent, rfl
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u_1
inst : AddMonoid G
⊢ exponent.{u_1} (Multiplicative G) = AddMonoid.exponent G

Tactic:
rfl

Premises used: Multiplicative, AddMonoid.exponent, rfl, AddMonoid.ExponentExists
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h₂ :
  (∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
      (h₁ : b = c) (h₂ : ∀ (h : c), x_1 ⋯ = u h) (h₃ : ∀ (h : ¬c), y ⋯ = v h), dite b x_1 y = dite c u v) →
    (∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1) → ∀ (x : ℕ), (∀ (g : Gᵐᵒᵖ), g ^ x = 1) ↔ ∀ (g : G), g ^ x = 1
h₁ : ∀ (x : ℕ), (∀ (g : Gᵐᵒᵖ), g ^ x = 1) ↔ ∀ (g : G), g ^ x = 1
⊢ Eq (α := ℕ)
    (if h : ∃ (n : ℕ), 0 < n ∧ ∀ (g : Gᵐᵒᵖ), g ^ n = 1 then
      Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : Gᵐᵒᵖ), g ^ n = 1) h
    else 0)
    (if h : ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1 then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h
    else 0)

Tactic:
congr!
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h_congr_thm :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c) (h₂ : ∀ (h : c), x_1 ⋯ = u h) (h₃ : ∀ (h : ¬c), y ⋯ = v h), dite b x_1 y = dite c u v
h : ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1
x : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x = 1) ↔ ∀ (g : G), g ^ x = 1

Tactic:
⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩

Premises used: MulOpposite.op_injective, Iff.intro, MulOpposite.unop, MulOpposite.unop_injective, MulOpposite.op
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h_congr_thm :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c) (h₂ : ∀ (h : c), x_1 ⋯ = u h) (h₃ : ∀ (h : ¬c), y ⋯ = v h), dite b x_1 y = dite c u v
h : ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1
x : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x = 1) ↔ ∀ (g : G), g ^ x = 1

Tactic:
exact ⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x = 1) ↔ ∀ (g : G), g ^ x = 1

Tactic:
⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩

Premises used: MulOpposite.op_injective, Iff.intro, MulOpposite.unop, MulOpposite.unop_injective, MulOpposite.op
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x = 1) ↔ ∀ (g : G), g ^ x = 1

Tactic:
exact ⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
g : G
h₁ : ∀ (n : ℕ), 0 < n → ∀ (this : ∀ (g : G), g ^ n = 1), g ^ n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ g ^ n = 1

Tactic:
peel 2 h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
g : G
n : ℕ
p : 0 < n
this : ∀ (g : G), g ^ n = 1
⊢ g ^ n = 1

Tactic:
this g
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
g : G
n : ℕ
p : 0 < n
this : ∀ (g : G), g ^ n = 1
⊢ g ^ n = 1

Tactic:
exact this g
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
g : G
⊢ 0 < orderOf g

Tactic:
h.isOfFinOrder.orderOf_pos

Premises used: IsOfFinOrder.orderOf_pos, Monoid.ExponentExists.isOfFinOrder
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
pos : ∀ (h : ExponentExists G), Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h ≠ 0 ↔ ExponentExists G
neg : ∀ (h : ¬ExponentExists G), Ne (α := ℕ) 0 0 ↔ ExponentExists G
⊢ Ne (α := ℕ) (if h : ExponentExists G then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h else 0) 0 ↔
    ExponentExists G

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
⊢ Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h ≠ 0 ↔ ExponentExists G

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ¬ExponentExists G
neg : Ne (α := ℕ) 0 0 → ExponentExists G
neg₁ : ExponentExists G → Ne (α := ℕ) 0 0
neg₂ : Ne (α := ℕ) 0 0 → ExponentExists G
neg₃ : ExponentExists G → Ne (α := ℕ) 0 0
⊢ Ne (α := ℕ) 0 0 ↔ ExponentExists G

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
⊢ 0 < exponent G ↔ ExponentExists G

Tactic:
pos_iff_ne_zero.trans exponent_ne_zero

Premises used: Monoid.exponent_ne_zero, Iff.trans, pos_iff_ne_zero
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
⊢ exponent G = 0 ↔ ¬ExponentExists G

Tactic:
exponent_ne_zero.not_right

Premises used: Monoid.exponent_ne_zero, Iff.not_right
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
g : G
hg : orderOf g = 0
⊢ exponent G = 0

Tactic:
exponent_eq_zero_iff.mpr fun h ↦ h.orderOf_pos g |>.ne' hg

Premises used: Iff.mpr, Monoid.ExponentExists.orderOf_pos, Monoid.exponent_eq_zero_iff, LT.lt.ne'
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
pos : ∀ (h : ExponentExists G), exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
neg : ∀ (h : ¬ExponentExists G), exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
by_cases h : Monoid.ExponentExists G

Premises used: Monoid.ExponentExists
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
⊢ Set.Nonempty (α := ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
have h' : {d : ℕ | 0 < d ∧ ∀ x : G, x ^ d = 1}.Nonempty := h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
h' : Set.Nonempty (α := ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
pos :
  Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h =
    Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1} n) h'
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
rw [Monoid.exponent, dif_pos h, Nat.sInf_def h']

Premises used: dif_pos, Nat.sInf_def, Monoid.exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
h' : Set.Nonempty (α := ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
⊢ Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h =
    Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1} n) h'

Tactic:
congr
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ¬ExponentExists G
⊢ Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1} ∅

Tactic:
have : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅ :=
      Set.eq_empty_of_forall_notMem fun n hn ↦ h ⟨n, hn⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ¬ExponentExists G
this : Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1} ∅
neg : Eq (α := ℕ) 0 (sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1})
neg₁ : Eq (α := ℕ) 0 (sInf ∅)
neg₂ neg₃ : Eq (α := ℕ) 0 0
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
rw [Monoid.exponent_eq_zero_iff.mpr h, this, Nat.sInf_empty]

Premises used: Iff.mpr, Monoid.exponent_eq_zero_iff, Nat.sInf_empty
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
rw : (¬∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1) ↔ ∀ n > 0, ∃ (g : G), g ^ n ≠ 1
⊢ exponent G = 0 ↔ ∀ n > 0, ∃ (g : G), g ^ n ≠ 1

Tactic:
rw [exponent_eq_zero_iff, ExponentExists]

Premises used: Monoid.ExponentExists, Monoid.exponent_eq_zero_iff
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
push : (∀ (n : ℕ) (_ : 0 < n), ∃ (g : G), g ^ n ≠ 1) ↔ ∀ n > 0, ∃ (g : G), g ^ n ≠ 1
⊢ (¬∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1) ↔ ∀ n > 0, ∃ (g : G), g ^ n ≠ 1

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
⊢ (∀ (n : ℕ) (_ : 0 < n), ∃ (g : G), g ^ n ≠ 1) ↔ ∀ n > 0, ∃ (g : G), g ^ n ≠ 1

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
g : G
pos : ∀ (h : ExponentExists G), g ^ exponent G = 1
neg : ∀ (h : ¬ExponentExists G), g ^ exponent G = 1
⊢ g ^ exponent G = 1

Tactic:
by_cases h : ExponentExists G

Premises used: Monoid.ExponentExists
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
g : G
h : ExponentExists G
pos : g ^ Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h = 1
⊢ g ^ exponent G = 1

Tactic:
simp_rw [exponent, dif_pos h]

Premises used: dif_pos, Monoid.exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h = 1

Tactic:
(Nat.find_spec h).2 g

Premises used: And.right, Nat.find_spec
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h = 1

Tactic:
exact (Nat.find_spec h).2 g

Premises used: And.right, Nat.find_spec
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
g : G
h : ¬ExponentExists G
neg :
  HPow.hPow (β := ℕ) g
      (if h : ExponentExists G then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h else 0) =
    1
neg₁ : HPow.hPow (β := ℕ) g 0 = 1
⊢ g ^ exponent G = 1

Tactic:
simp_rw [exponent, dif_neg h, pow_zero]

Premises used: dif_neg, pow_zero, Monoid.exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
g : G
pos : ∀ (h : ExponentExists G), g ^ exponent G = 1
neg neg₁ : ∀ (h : ¬ExponentExists G), g ^ exponent G = 1
⊢ g ^ exponent G = 1

Tactic:
classical
  by_cases h : ExponentExists G
  · simp_rw [exponent, dif_pos h]
    exact (Nat.find_spec h).2 g
  · simp_rw [exponent, dif_neg h, pow_zero]

Premises used: Monoid.ExponentExists, pow_zero, Monoid.exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
g : G
rw rw₁ : g ^ n = g ^ n
⊢ g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G))

Tactic:
rw [Nat.mod_add_div]

Premises used: Nat.mod_add_div
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
g : G
⊢ g ^ (n % exponent G + exponent G * (n / exponent G)) = g ^ (n % exponent G)

Tactic:
simp [pow_add, pow_mul, pow_exponent_eq_one]

Premises used: pow_add, pow_mul, Monoid.pow_exponent_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ 0 < exponent G

Tactic:
ExponentExists.exponent_pos ⟨n, hpos, hG⟩

Premises used: Monoid.ExponentExists.exponent_pos, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
rw : Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) ⋯ ≤ n
hc : ExponentExists G
⊢ exponent G ≤ n

Tactic:
rw [exponent, dif_pos]

Premises used: dif_pos, Monoid.exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
h : 0 < n ∧ ∀ (g : G), g ^ n = 1
⊢ Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) ⋯ ≤ n

Tactic:
apply Nat.find_min'

Premises used: Nat.find_min'
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ 0 < n ∧ ∀ (g : G), g ^ n = 1

Tactic:
⟨hpos, hG⟩

Premises used: And.intro
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ 0 < n ∧ ∀ (g : G), g ^ n = 1

Tactic:
exact ⟨hpos, hG⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ ExponentExists G

Tactic:
⟨n, hpos, hG⟩

Premises used: Monoid.ExponentExists, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ ExponentExists G

Tactic:
exact ⟨n, hpos, hG⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
rw : (if h : ExponentExists G then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h else 0) ≤ n
rw₁ : Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) ⋯ ≤ n
hc : ExponentExists G
rw₂ : Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) ⋯ ≤ n
hc₁ : ExponentExists G
rw₃ : Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) ⋯ ≤ n
hc₂ hc₃ : ExponentExists G
⊢ exponent G ≤ n

Tactic:
classical
  rw [exponent, dif_pos]
  · apply Nat.find_min'
    exact ⟨hpos, hG⟩
  · exact ⟨n, hpos, hG⟩

Premises used: dif_pos, Nat.find_min', Monoid.exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
by_contra! : ∀ (h : ∀ (g : G), g ^ m = 1), False
⊢ ∃ (g : G), g ^ m ≠ 1

Tactic:
by_contra! h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
⊢ exponent G ≤ m

Tactic:
have hcon : exponent G ≤ m := exponent_min' m hpos h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
hcon : exponent G ≤ m
⊢ False

Tactic:
lia
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
⊢ exponent G = 1 ↔ Subsingleton G

Tactic:
⟨fun eq_one => ⟨fun a b => ?a_eq_b⟩, fun h => le_antisymm ?le ?ge⟩

Premises used: le_antisymm, Subsingleton.intro, Iff.intro
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
a_eq_b : ∀ (eq_one : exponent G = 1) (a b : G), a = b
le : ∀ (h : Subsingleton G), exponent G ≤ 1
ge : ∀ (h : Subsingleton G), 1 ≤ exponent G
⊢ exponent G = 1 ↔ Subsingleton G

Tactic:
refine ⟨fun eq_one => ⟨fun a b => ?a_eq_b⟩, fun h => le_antisymm ?le ?ge⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
eq_one : exponent G = 1
a b : G
a_eq_b : HPow.hPow (β := ℕ) a 1 = b
a_eq_b₁ : HPow.hPow (β := ℕ) a 1 = HPow.hPow (β := ℕ) b 1
a_eq_b₂ : a ^ exponent G = b ^ exponent G
a_eq_b₃ : 1 = b ^ exponent G
a_eq_b₄ a_eq_b₅ : Eq.{u + 1} (α := G) 1 1
⊢ a = b

Tactic:
rw [← pow_one a, ← pow_one b, ← eq_one, Monoid.pow_exponent_eq_one, Monoid.pow_exponent_eq_one]

Premises used: pow_one, Monoid.pow_exponent_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : Subsingleton G
le : ∀ (g : G), HPow.hPow (β := ℕ) g 1 = 1
⊢ exponent G ≤ 1

Tactic:
apply exponent_min' _ Nat.one_pos

Premises used: Nat.one_pos, Monoid.exponent_min'
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : Subsingleton G
⊢ ∀ (g : G), HPow.hPow (β := ℕ) g 1 = 1

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : Subsingleton G
ge : ∀ (g : G), HPow.hPow (β := ℕ) g 1 = 1
⊢ 0 < exponent G

Tactic:
apply exponent_pos_of_exists 1 Nat.one_pos

Premises used: Nat.one_pos, OfNat.ofNat, Monoid.exponent_pos_of_exists
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
hs : Subsingleton G
⊢ exponent G = 1

Tactic:
exp_eq_one_iff.mpr hs

Premises used: Iff.mpr, Monoid.exp_eq_one_iff
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
g : G
⊢ orderOf g ∣ exponent G

Tactic:
orderOf_dvd_of_pow_eq_one <| pow_exponent_eq_one g

Premises used: orderOf_dvd_of_pow_eq_one, Monoid.pow_exponent_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
g : G
⊢ orderOf g ≤ exponent G

Tactic:
Nat.le_of_dvd h.exponent_pos (order_dvd_exponent g)

Premises used: Monoid.ExponentExists.exponent_pos, Monoid.order_dvd_exponent, Nat.le_of_dvd