internlm/Lean-Github huggingface dataset:
Theorem: n1_2_5'
Proof state before:
case a.intro.intro.cons
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ List.prod (y_hd :: tail) ∈ i
Tactic:
simp only [List.prod_cons]
Proof state after:
case a.intro.intro.cons
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ y_hd * List.prod tail ∈ i
Theorem: n1_2_5'
Proof state before:
case a.intro.intro.cons
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ y_hd * List.prod tail ∈ i
Tactic:
apply mul_mem
Proof state after:
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ y_hd ∈ i

case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ List.prod tail ∈ i
Theorem: n1_2_5'
Proof state before:
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ y_hd ∈ i
Tactic:
specialize h1 y_hd (List.mem_cons_self _ _)
Proof state after:
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : y_hd ∈ X ∪ X⁻¹
⊢ y_hd ∈ i
Theorem: n1_2_5'
Proof state before:
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : y_hd ∈ X ∪ X⁻¹
⊢ y_hd ∈ i
Tactic:
obtain h1 | h1 := (Set.mem_union _ _ _).mp h1
Proof state after:
case a.intro.intro.cons.a.inl
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X
⊢ y_hd ∈ i

case a.intro.intro.cons.a.inr
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X⁻¹
⊢ y_hd ∈ i
Theorem: n1_2_5'
Proof state before:
case a.intro.intro.cons.a.inl
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X
⊢ y_hd ∈ i
Tactic:
exact hi h1
Proof state after:
no goals
Theorem: n1_2_5'
Proof state before:
case a.intro.intro.cons.a.inr
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X⁻¹
⊢ y_hd ∈ i
Tactic:
rw [← inv_inv y_hd]
Proof state after:
case a.intro.intro.cons.a.inr
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X⁻¹
⊢ y_hd⁻¹⁻¹ ∈ i
Theorem: n1_2_5'
Proof state before:
case a.intro.intro.cons.a.inr
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X⁻¹
⊢ y_hd⁻¹⁻¹ ∈ i
Tactic:
exact Subgroup.inv_mem _ (hi h1)
Proof state after:
no goals
Theorem: n1_2_5'
Proof state before:
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ List.prod tail ∈ i
Tactic:
exact y_ih fun y hy => h1 _ (List.mem_cons_of_mem _ hy)
Proof state after:
no goals
Theorem: d1_2_10'
Proof state before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H
Tactic:
have : Fintype H := by classical infer_instance
Proof state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H
Theorem: d1_2_10'
Proof state before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H
Tactic:
have : 0 < Nat.card H := by
  rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
  exact ⟨⟨1, one_mem _⟩⟩
Proof state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this✝ : Fintype ↥H
this : 0 < Nat.card ↥H
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H
Theorem: d1_2_10'
Proof state before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this✝ : Fintype ↥H
this : 0 < Nat.card ↥H
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H
Tactic:
rw [← Subgroup.card_mul_index H, Nat.mul_div_cancel_left _ this, Subgroup.index]
Proof state after:
no goals
Theorem: d1_2_10'
Proof state before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
⊢ Fintype ↥H
Tactic:
classical infer_instance
Proof state after:
no goals
Theorem: d1_2_10'
Proof state before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
⊢ Fintype ↥H
Tactic:
infer_instance
Proof state after:
no goals
Theorem: d1_2_10'
Proof state before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ 0 < Nat.card ↥H
Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
Proof state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ Nonempty ↥H
Theorem: d1_2_10'
Proof state before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ Nonempty ↥H
Tactic:
exact ⟨⟨1, one_mem _⟩⟩
Proof state after:
no goals
Theorem: xmp_1_2_11
Proof state before:
n : ℕ+
⊢ AddSubgroup.index (ex1232 ↑↑n) = ↑n
Tactic:
simp [ex1232, AddSubgroup.index, Nat.card_congr (Int.quotientZMultiplesNatEquivZMod n).toEquiv,
  Nat.card_eq_fintype_card, ZMod.card]
Proof state after:
no goals
Theorem: n_1_2_13
Proof state before:
case mpr
G : Type u_1
inst✝ : Group G
A B : Set G
g : G
⊢ {x | ∃ a ∈ A, g⁻¹ * a = x} = B → A = {x | ∃ b ∈ B, g * b = x}
Tactic:
rintro rfl
Proof state after:
case mpr
G : Type u_1
inst✝ : Group G
A : Set G
g : G
⊢ A = {x | ∃ b ∈ {x | ∃ a ∈ A, g⁻¹ * a = x}, g * b = x}
Theorem: n_1_2_13
Proof state before:
case mpr
G : Type u_1
inst✝ : Group G
A : Set G
g : G
⊢ A = {x | ∃ b ∈ {x | ∃ a ∈ A, g⁻¹ * a = x}, g * b = x}
Tactic:
ext
Proof state after:
case mpr.h
G : Type u_1
inst✝ : Group G
A : Set G
g x✝ : G
⊢ x✝ ∈ A ↔ x✝ ∈ {x | ∃ b ∈ {x | ∃ a ∈ A, g⁻¹ * a = x}, g * b = x}
Theorem: n_1_2_13
Proof state before:
case mpr.h
G : Type u_1
inst✝ : Group G
A : Set G
g x✝ : G
⊢ x✝ ∈ A ↔ x✝ ∈ {x | ∃ b ∈ {x | ∃ a ∈ A, g⁻¹ * a = x}, g * b = x}
Tactic:
simp
Proof state after:
no goals
Theorem: ex_1_2_4
Proof state before:
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ x_1 ∈ A ×ˢ B, ex124' x_1 = x} ≤ #↑A * #↑B
Tactic:
simp only [ex124', Set.mem_prod, exists_prop, Prod.exists]
Proof state after:
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} ≤ #↑A * #↑B
Theorem: ex_1_2_4
Proof state before:
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} ≤ #↑A * #↑B
Tactic:
calc
  (#{x | ∃ a b : G, (a ∈ A ∧ b ∈ B) ∧ a * b = x}) =
      (#(⋃ (a ∈ A) (b ∈ B), ({(a : G) * (b : G)} : Set G))) := ?_
  _ = (#(⋃ (a : A) (b : B), ({(a : G) * (b : G)} : Set G))) := ?_
  _ ≤ Cardinal.sum fun a : A => Cardinal.sum fun b : B => #({(a : G) * (b : G)} : Set G) := ?_
  _ = (#A) * (#B) := ?_
Proof state after:
case calc_1
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} = #↑(⋃ a ∈ A, ⋃ b ∈ B, {a * b})

case calc_2
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑(⋃ a ∈ A, ⋃ b ∈ B, {a * b}) = #↑(⋃ a, ⋃ b, {↑a * ↑b})

case calc_3
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑(⋃ a, ⋃ b, {↑a * ↑b}) ≤ Cardinal.sum fun a => Cardinal.sum fun b => #↑{↑a * ↑b}

case calc_4
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ (Cardinal.sum fun a => Cardinal.sum fun b => #↑{↑a * ↑b}) = #↑A * #↑B
Theorem: ex_1_2_4
Proof state before:
case calc_1
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} = #↑(⋃ a ∈ A, ⋃ b ∈ B, {a * b})
Tactic:
congr 2 with x
Proof state after:
case calc_1.e_a.e_s.h
G : Type u_1
inst✝ : Group G
A B : Set G
x : G
⊢ x ∈ {x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} ↔ x ∈ ⋃ a ∈ A, ⋃ b ∈ B, {a * b}
Theorem: ex_1_2_4
Proof state before:
case calc_1.e_a.e_s.h
G : Type u_1
inst✝ : Group G
A B : Set G
x : G
⊢ x ∈ {x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} ↔ x ∈ ⋃ a ∈ A, ⋃ b ∈ B, {a * b}
Tactic:
simp [Set.setOf_exists, Set.setOf_and, and_assoc]
Proof state after:
no goals
Theorem: ex_1_2_4
Proof state before:
case calc_2
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑(⋃ a ∈ A, ⋃ b ∈ B, {a * b}) = #↑(⋃ a, ⋃ b, {↑a * ↑b})
Tactic:
simp only [Set.iUnion_coe_set]
Proof state after:
no goals
Theorem: ex_1_2_4
Proof state before:
case calc_3
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑(⋃ a, ⋃ b, {↑a * ↑b}) ≤ Cardinal.sum fun a => Cardinal.sum fun b => #↑{↑a * ↑b}
Tactic:
exact
  Cardinal.mk_iUnion_le_sum_mk.trans
    (Cardinal.sum_le_sum _ _ fun a => Cardinal.mk_iUnion_le_sum_mk)
Proof state after:
no goals
Theorem: ex_1_2_4
Proof state before:
case calc_4
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ (Cardinal.sum fun a => Cardinal.sum fun b => #↑{↑a * ↑b}) = #↑A * #↑B
Tactic:
simp_rw [Cardinal.mk_singleton, Cardinal.sum_const', mul_one]
Proof state after:
no goals
Theorem: ex_1_2_5
Proof state before:
G : Type u_1
inst✝ : Group G
A B : Set G
g : G
⊢ {x | ∃ x_1 ∈ A ∩ B, g * x_1 = x} = {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Tactic:
ext y
Proof state after:
case h
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ y ∈ {x | ∃ x_1 ∈ A ∩ B, g * x_1 = x} ↔ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Theorem: ex_1_2_5
Proof state before:
case h
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ y ∈ {x | ∃ x_1 ∈ A ∩ B, g * x_1 = x} ↔ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Tactic:
simp only [Set.mem_inter, Set.mem_setOf_eq, exists_prop]
Proof state after:
case h
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ (∃ x ∈ A ∩ B, g * x = y) ↔ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Theorem: ex_1_2_5
Proof state before:
case h
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ (∃ x ∈ A ∩ B, g * x = y) ↔ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Tactic:
constructor
Proof state after:
case h.mp
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ (∃ x ∈ A ∩ B, g * x = y) → y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}

case h.mpr
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x} → ∃ x ∈ A ∩ B, g * x = y
Theorem: ex_1_2_5
Proof state before:
case h.mp
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ (∃ x ∈ A ∩ B, g * x = y) → y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Tactic:
rintro ⟨x, ⟨ha, hb⟩, hx⟩
Proof state after:
case h.mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
hx : g * x = y
ha : x ∈ A
hb : x ∈ B
⊢ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Theorem: ex_1_2_5
Proof state before:
case h.mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
hx : g * x = y
ha : x ∈ A
hb : x ∈ B
⊢ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Tactic:
exact ⟨⟨x, ha, hx⟩, ⟨x, hb, hx⟩⟩
Proof state after:
no goals
Theorem: ex_1_2_5
Proof state before:
case h.mpr
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x} → ∃ x ∈ A ∩ B, g * x = y
Tactic:
rintro ⟨⟨x, ha, hx⟩, ⟨x', hb, hx'⟩⟩
Proof state after:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
x' : G
hb : x' ∈ B
hx' : g * x' = y
⊢ ∃ x ∈ A ∩ B, g * x = y
Theorem: ex_1_2_5
Proof state before:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
x' : G
hb : x' ∈ B
hx' : g * x' = y
⊢ ∃ x ∈ A ∩ B, g * x = y
Tactic:
obtain rfl : x = x' := by rw [← mul_right_inj g, hx, hx']
Proof state after:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
hb : x ∈ B
hx' : g * x = y
⊢ ∃ x ∈ A ∩ B, g * x = y
Theorem: ex_1_2_5
Proof state before:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
hb : x ∈ B
hx' : g * x = y
⊢ ∃ x ∈ A ∩ B, g * x = y
Tactic:
exact ⟨x, ⟨ha, hb⟩, hx⟩
Proof state after:
no goals
Theorem: ex_1_2_5
Proof state before:
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
x' : G
hb : x' ∈ B
hx' : g * x' = y
⊢ x = x'
Tactic:
rw [← mul_right_inj g, hx, hx']
Proof state after:
no goals
Theorem: l1_2_15_ii
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
⊢ ↑(Subgroup.closure {g}) = {x | ∃ k, g ^ k = x}
Tactic:
ext
Proof state after:
case h
G : Type u_1
inst✝ : Group G
g x✝ : G
⊢ x✝ ∈ ↑(Subgroup.closure {g}) ↔ x✝ ∈ {x | ∃ k, g ^ k = x}
Theorem: l1_2_15_ii
Proof state before:
case h
G : Type u_1
inst✝ : Group G
g x✝ : G
⊢ x✝ ∈ ↑(Subgroup.closure {g}) ↔ x✝ ∈ {x | ∃ k, g ^ k = x}
Tactic:
simp only [SetLike.mem_coe, Set.mem_setOf_eq, Subgroup.mem_closure_singleton]
Proof state after:
no goals
Theorem: l1_2_17
Proof state before:
G : Type u_1
inst✝ : Group G
g a b : G
ha : a ∈ Subgroup.closure {g}
hb : b ∈ Subgroup.closure {g}
⊢ a * b = b * a
Tactic:
rw [Subgroup.mem_closure_singleton] at ha hb
Proof state after:
G : Type u_1
inst✝ : Group G
g a b : G
ha : ∃ n, g ^ n = a
hb : ∃ n, g ^ n = b
⊢ a * b = b * a
Theorem: l1_2_17
Proof state before:
G : Type u_1
inst✝ : Group G
g a b : G
ha : ∃ n, g ^ n = a
hb : ∃ n, g ^ n = b
⊢ a * b = b * a
Tactic:
obtain ⟨n, rfl⟩ := ha
Proof state after:
case intro
G : Type u_1
inst✝ : Group G
g b : G
hb : ∃ n, g ^ n = b
n : ℤ
⊢ g ^ n * b = b * g ^ n
Theorem: l1_2_17
Proof state before:
case intro
G : Type u_1
inst✝ : Group G
g b : G
hb : ∃ n, g ^ n = b
n : ℤ
⊢ g ^ n * b = b * g ^ n
Tactic:
obtain ⟨m, rfl⟩ := hb
Proof state after:
case intro.intro
G : Type u_1
inst✝ : Group G
g : G
n m : ℤ
⊢ g ^ n * g ^ m = g ^ m * g ^ n
Theorem: l1_2_17
Proof state before:
case intro.intro
G : Type u_1
inst✝ : Group G
g : G
n m : ℤ
⊢ g ^ n * g ^ m = g ^ m * g ^ n
Tactic:
rw [← zpow_add, ← zpow_add, add_comm]
Proof state after:
no goals
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
⊢ y ∈ closure {x} ↔ ∃ n < orderOf x, x ^ n = y
Tactic:
simp only [← zpowers_eq_closure, exists_prop]
Proof state after:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
⊢ y ∈ zpowers x ↔ ∃ n < orderOf x, x ^ n = y
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
⊢ y ∈ zpowers x ↔ ∃ n < orderOf x, x ^ n = y
Tactic:
constructor <;>
rintro ⟨i, hi⟩
Proof state after:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
⊢ ∃ n < orderOf x, x ^ n = y

case mpr.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℕ
hi : i < orderOf x ∧ x ^ i = y
⊢ y ∈ zpowers x
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
⊢ ∃ n, 0 ≤ n ∧ n < ↑(orderOf x) ∧ x ^ n = y
Tactic:
have ho : 0 < (orderOf x : ℤ) := by
  rwa [Int.coe_nat_pos, pos_iff_ne_zero, Ne.def, orderOf_eq_zero_iff, Classical.not_not]
Proof state after:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ ∃ n, 0 ≤ n ∧ n < ↑(orderOf x) ∧ x ^ n = y
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ ∃ n, 0 ≤ n ∧ n < ↑(orderOf x) ∧ x ^ n = y
Tactic:
refine' ⟨i % orderOf x, Int.emod_nonneg _ ho.ne', Int.emod_lt_of_pos _ ho, _⟩
Proof state after:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ x ^ (i % ↑(orderOf x)) = y
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ x ^ (i % ↑(orderOf x)) = y
Tactic:
rw [← hi, l1_2_20_i _ _ _ _ h]
Proof state after:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ i % ↑(orderOf x) ≡ i [ZMOD ↑(orderOf x)]
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ i % ↑(orderOf x) ≡ i [ZMOD ↑(orderOf x)]
Tactic:
exact Int.mod_modEq _ _
Proof state after:
no goals
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
this : ∃ n, 0 ≤ n ∧ n < ↑(orderOf x) ∧ x ^ n = y
⊢ ∃ n < orderOf x, x ^ n = y
Tactic:
obtain ⟨n, hnonneg, hlt, heq⟩ := this
Proof state after:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ ∃ n < orderOf x, x ^ n = y
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ ∃ n < orderOf x, x ^ n = y
Tactic:
refine' ⟨n.natAbs, _, _⟩
Proof state after:
case intro.intro.intro.refine'_1
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ Int.natAbs n < orderOf x

case intro.intro.intro.refine'_2
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ x ^ Int.natAbs n = y
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
case intro.intro.intro.refine'_1
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ Int.natAbs n < orderOf x
Tactic:
rwa [← Int.ofNat_lt, Int.natAbs_of_nonneg hnonneg]
Proof state after:
no goals
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
case intro.intro.intro.refine'_2
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ x ^ Int.natAbs n = y
Tactic:
rwa [← zpow_ofNat, Int.natAbs_of_nonneg hnonneg]
Proof state after:
no goals
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
⊢ 0 < ↑(orderOf x)
Tactic:
rwa [Int.coe_nat_pos, pos_iff_ne_zero, Ne.def, orderOf_eq_zero_iff, Classical.not_not]
Proof state after:
no goals
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
case mpr.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℕ
hi : i < orderOf x ∧ x ^ i = y
⊢ y ∈ zpowers x
Tactic:
use i
Proof state after:
case h
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℕ
hi : i < orderOf x ∧ x ^ i = y
⊢ (fun x_1 => x ^ x_1) ↑i = y
Theorem: Subgroup.mem_closure_singleton'
Proof state before:
case h
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℕ
hi : i < orderOf x ∧ x ^ i = y
⊢ (fun x_1 => x ^ x_1) ↑i = y
Tactic:
simp only [zpow_ofNat, hi.2]
Proof state after:
no goals
Theorem: l1_2_20_i'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
⊢ ↑(Subgroup.closure {g}) = {x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x}
Tactic:
ext
Proof state after:
case h
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
x✝ : G
⊢ x✝ ∈ ↑(Subgroup.closure {g}) ↔ x✝ ∈ {x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x}
Theorem: l1_2_20_i'
Proof state before:
case h
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
x✝ : G
⊢ x✝ ∈ ↑(Subgroup.closure {g}) ↔ x✝ ∈ {x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x}
Tactic:
simp [Subgroup.mem_closure_singleton' h]
Proof state after:
no goals
Theorem: l1_2_20_ii
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
i j : ℤ
h : ¬IsOfFinOrder g
⊢ g ^ i = g ^ j ↔ i = j
Tactic:
rw [← orderOf_eq_zero_iff] at h
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
i j : ℤ
h : orderOf g = 0
⊢ g ^ i = g ^ j ↔ i = j
Theorem: l1_2_20_ii
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
i j : ℤ
h : orderOf g = 0
⊢ g ^ i = g ^ j ↔ i = j
Tactic:
rw [zpow_eq_zpow_iff_modEq, h, Int.ofNat_zero, Int.modEq_zero_iff]
Proof state after:
no goals
Theorem: l1_2_20_ii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
⊢ ↑(Subgroup.closure {g}) = {x | ∃ i, g ^ i = x}
Tactic:
rw [← Subgroup.zpowers_eq_closure]
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
⊢ ↑(Subgroup.zpowers g) = {x | ∃ i, g ^ i = x}
Theorem: l1_2_20_ii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
⊢ ↑(Subgroup.zpowers g) = {x | ∃ i, g ^ i = x}
Tactic:
ext
Proof state after:
case h
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
x✝ : G
⊢ x✝ ∈ ↑(Subgroup.zpowers g) ↔ x✝ ∈ {x | ∃ i, g ^ i = x}
Theorem: l1_2_20_ii'
Proof state before:
case h
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
x✝ : G
⊢ x✝ ∈ ↑(Subgroup.zpowers g) ↔ x✝ ∈ {x | ∃ i, g ^ i = x}
Tactic:
simp [Subgroup.mem_zpowers_iff]
Proof state after:
no goals
Theorem: l1_2_20_iii
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
⊢ #↑↑(Subgroup.closure {g}) = ↑(orderOf g)
Tactic:
have := (IsOfFinOrder.orderOf_pos h).ne'
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑↑(Subgroup.closure {g}) = ↑(orderOf g)
Theorem: l1_2_20_iii
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑↑(Subgroup.closure {g}) = ↑(orderOf g)
Tactic:
rw [l1_2_20_i' _ _ h]
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑{x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x} = ↑(orderOf g)
Theorem: l1_2_20_iii
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑{x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x} = ↑(orderOf g)
Tactic:
trans #((Set.Ico 0 (orderOf g)).image fun i => g ^ i)
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑{x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x} = #↑((fun i => g ^ i) '' Set.Ico 0 (orderOf g))

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑((fun i => g ^ i) '' Set.Ico 0 (orderOf g)) = ↑(orderOf g)
Theorem: l1_2_20_iii
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑((fun i => g ^ i) '' Set.Ico 0 (orderOf g)) = ↑(orderOf g)
Tactic:
simp only [Cardinal.mk_fintype, Nat.cast_inj, Fintype.card_ofFinset]
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ (Finset.image (fun i => g ^ i) (Set.toFinset (Set.Ico 0 (orderOf g)))).card = orderOf g