internlm/Lean-Github huggingface dataset:
Theorem: l1_2_20_iii
Proof state before:
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
Tactic:
rw [Finset.card_image_of_injOn]
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ (Set.toFinset (Set.Ico 0 (orderOf g))).card = orderOf g

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ Set.InjOn (fun i => g ^ i) ↑(Set.toFinset (Set.Ico 0 (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
⊢ (Set.toFinset (Set.Ico 0 (orderOf g))).card = orderOf g

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ Set.InjOn (fun i => g ^ i) ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
Tactic:
simp only [tsub_zero, eq_self_iff_true, Set.toFinset_card, Nat.card_fintypeIco]
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ Set.InjOn (fun i => g ^ i) ↑(Set.toFinset (Set.Ico 0 (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
⊢ Set.InjOn (fun i => g ^ i) ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
Tactic:
intro x hx y hy hxy
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : (fun i => g ^ i) x = (fun i => g ^ i) y
⊢ x = y
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 : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : (fun i => g ^ i) x = (fun i => g ^ i) y
⊢ x = y
Tactic:
rwa [pow_eq_pow_iff_modEq, Nat.ModEq, Nat.mod_eq_of_lt, Nat.mod_eq_of_lt] at hxy
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x = y % orderOf g
⊢ y < orderOf g

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x % orderOf g = y % orderOf g
⊢ 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 : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x = y % orderOf g
⊢ y < orderOf g

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x % orderOf g = y % orderOf g
⊢ x < orderOf g
Tactic:
simpa using hy
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x % orderOf g = y % orderOf g
⊢ 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 : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x % orderOf g = y % orderOf g
⊢ x < orderOf g
Tactic:
simpa using hx
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
this : orderOf g ≠ 0
⊢ #↑{x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x} = #↑((fun i => g ^ i) '' Set.Ico 0 (orderOf g))
Tactic:
congr
Proof state after:
no goals
Theorem: zpow_inj_iff_of_orderOf_eq_zero
Proof state before:
G : Type u
A : Type v
x y : G
a b : A
n✝ m✝ : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
h : orderOf x = 0
n m : ℤ
⊢ x ^ n = x ^ m ↔ n = m
Tactic:
rw [orderOf_eq_zero_iff] at h
Proof state after:
G : Type u
A : Type v
x y : G
a b : A
n✝ m✝ : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
h : ¬IsOfFinOrder x
n m : ℤ
⊢ x ^ n = x ^ m ↔ n = m
Theorem: zpow_inj_iff_of_orderOf_eq_zero
Proof state before:
G : Type u
A : Type v
x y : G
a b : A
n✝ m✝ : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
h : ¬IsOfFinOrder x
n m : ℤ
⊢ x ^ n = x ^ m ↔ n = m
Tactic:
exact l1_2_20_ii _ _ n m h
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
⊢ Set.Infinite ↑(Subgroup.closure {g})
Tactic:
rw [l1_2_20_ii' _ _ h]
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : ¬IsOfFinOrder g
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
Theorem: l1_2_20_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : ¬IsOfFinOrder g
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
Tactic:
rw [← orderOf_eq_zero_iff] at h
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
Theorem: l1_2_20_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
Tactic:
have : ((Set.univ : Set ℕ).image fun i => g ^ i).Infinite := by
  simp
  apply Set.infinite_range_of_injective
  intro x y hxy
  rwa [pow_inj_iff_of_orderOf_eq_zero h] at hxy
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
Theorem: l1_2_20_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
Tactic:
apply Set.Infinite.mono _ this
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
⊢ (fun i => g ^ i) '' Set.univ ⊆ {x | ∃ i, g ^ i = x}
Theorem: l1_2_20_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
⊢ (fun i => g ^ i) '' Set.univ ⊆ {x | ∃ i, g ^ i = x}
Tactic:
intro x hx
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : x ∈ (fun i => g ^ i) '' Set.univ
⊢ x ∈ {x | ∃ i, g ^ i = x}
Theorem: l1_2_20_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : x ∈ (fun i => g ^ i) '' Set.univ
⊢ x ∈ {x | ∃ i, g ^ i = x}
Tactic:
simp only [Set.image_univ, Set.mem_range] at hx
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : ∃ y, g ^ y = x
⊢ x ∈ {x | ∃ i, g ^ i = x}
Theorem: l1_2_20_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : ∃ y, g ^ y = x
⊢ x ∈ {x | ∃ i, g ^ i = x}
Tactic:
simp only [Set.mem_setOf]
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : ∃ y, g ^ y = x
⊢ ∃ i, g ^ i = x
Theorem: l1_2_20_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : ∃ y, g ^ y = x
⊢ ∃ i, g ^ i = x
Tactic:
obtain ⟨n, hn⟩ := hx
Proof state after:
case intro
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
n : ℕ
hn : g ^ n = x
⊢ ∃ i, g ^ i = x
Theorem: l1_2_20_iii'
Proof state before:
case intro
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
n : ℕ
hn : g ^ n = x
⊢ ∃ i, g ^ i = x
Tactic:
use n
Proof state after:
case h
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
n : ℕ
hn : g ^ n = x
⊢ g ^ ↑n = x
Theorem: l1_2_20_iii'
Proof state before:
case h
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
n : ℕ
hn : g ^ n = x
⊢ g ^ ↑n = x
Tactic:
simp only [zpow_ofNat, hn]
Proof state after:
no goals
Theorem: l1_2_20_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite ((fun i => g ^ i) '' Set.univ)
Tactic:
simp
Proof state after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite (Set.range fun i => g ^ i)
Theorem: l1_2_20_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite (Set.range fun i => g ^ i)
Tactic:
apply Set.infinite_range_of_injective
Proof state after:
case hi
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Function.Injective fun i => g ^ i
Theorem: l1_2_20_iii'
Proof state before:
case hi
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Function.Injective fun i => g ^ i
Tactic:
intro x y hxy
Proof state after:
case hi
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
x y : ℕ
hxy : (fun i => g ^ i) x = (fun i => g ^ i) y
⊢ x = y
Theorem: l1_2_20_iii'
Proof state before:
case hi
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
x y : ℕ
hxy : (fun i => g ^ i) x = (fun i => g ^ i) y
⊢ x = y
Tactic:
rwa [pow_inj_iff_of_orderOf_eq_zero h] at hxy
Proof state after:
no goals
Theorem: Int.gcd_val
Proof state before:
a b : ℤ
⊢ gcd a b = gcd (b % a) a
Tactic:
rw [← natAbs_euclideanDomain_gcd, EuclideanDomain.gcd_val, natAbs_euclideanDomain_gcd]
Proof state after:
no goals
Theorem: coe_mul_inv_eq_one''
Proof state before:
n : ℕ
x : ℤ
h : IsCoprime x ↑n
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
cases n with
| zero =>
  simp [isCoprime_zero_right] at h
  rw [ZMod.mul_inv_eq_gcd, Nat.gcd_zero_right, Nat.cast_eq_one]
  simp only [ZMod.val]
  rw [Int.cast_id, Int.IsUnit.natAbs_eq h]
| succ n =>
  haveI := n.succ_pos
  rw [← Int.gcd_eq_one_iff_coprime, Int.gcd_comm, Int.gcd_val] at h
  rw [ZMod.mul_inv_eq_gcd, ← Int.coe_nat_gcd, ZMod.val_int_cast, h, Nat.cast_one]
Proof state after:
no goals
Theorem: coe_mul_inv_eq_one''
Proof state before:
case zero
x : ℤ
h : IsCoprime x ↑Nat.zero
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
simp [isCoprime_zero_right] at h
Proof state after:
case zero
x : ℤ
h : IsUnit x
⊢ ↑x * (↑x)⁻¹ = 1
Theorem: coe_mul_inv_eq_one''
Proof state before:
case zero
x : ℤ
h : IsUnit x
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
rw [ZMod.mul_inv_eq_gcd, Nat.gcd_zero_right, Nat.cast_eq_one]
Proof state after:
case zero
x : ℤ
h : IsUnit x
⊢ ZMod.val ↑x = 1
Theorem: coe_mul_inv_eq_one''
Proof state before:
case zero
x : ℤ
h : IsUnit x
⊢ ZMod.val ↑x = 1
Tactic:
simp only [ZMod.val]
Proof state after:
case zero
x : ℤ
h : IsUnit x
⊢ Int.natAbs ↑x = 1
Theorem: coe_mul_inv_eq_one''
Proof state before:
case zero
x : ℤ
h : IsUnit x
⊢ Int.natAbs ↑x = 1
Tactic:
rw [Int.cast_id, Int.IsUnit.natAbs_eq h]
Proof state after:
no goals
Theorem: coe_mul_inv_eq_one''
Proof state before:
case succ
x : ℤ
n : ℕ
h : IsCoprime x ↑(Nat.succ n)
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
haveI := n.succ_pos
Proof state after:
case succ
x : ℤ
n : ℕ
h : IsCoprime x ↑(Nat.succ n)
this : 0 < Nat.succ n
⊢ ↑x * (↑x)⁻¹ = 1
Theorem: coe_mul_inv_eq_one''
Proof state before:
case succ
x : ℤ
n : ℕ
h : IsCoprime x ↑(Nat.succ n)
this : 0 < Nat.succ n
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
rw [← Int.gcd_eq_one_iff_coprime, Int.gcd_comm, Int.gcd_val] at h
Proof state after:
case succ
x : ℤ
n : ℕ
h : Int.gcd (x % ↑(Nat.succ n)) ↑(Nat.succ n) = 1
this : 0 < Nat.succ n
⊢ ↑x * (↑x)⁻¹ = 1
Theorem: coe_mul_inv_eq_one''
Proof state before:
case succ
x : ℤ
n : ℕ
h : Int.gcd (x % ↑(Nat.succ n)) ↑(Nat.succ n) = 1
this : 0 < Nat.succ n
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
rw [ZMod.mul_inv_eq_gcd, ← Int.coe_nat_gcd, ZMod.val_int_cast, h, Nat.cast_one]
Proof state after:
no goals
Theorem: ZMod.pow_totient'
Proof state before:
n : ℕ
x : (ZMod n)ˣ
⊢ x ^ φ n = 1
Tactic:
cases n
Proof state after:
case zero
x : (ZMod Nat.zero)ˣ
⊢ x ^ φ Nat.zero = 1

case succ
n✝ : ℕ
x : (ZMod (Nat.succ n✝))ˣ
⊢ x ^ φ (Nat.succ n✝) = 1
Theorem: ZMod.pow_totient'
Proof state before:
case succ
n✝ : ℕ
x : (ZMod (Nat.succ n✝))ˣ
⊢ x ^ φ (Nat.succ n✝) = 1
Tactic:
apply ZMod.pow_totient
Proof state after:
no goals
Theorem: ZMod.pow_totient'
Proof state before:
case zero
x : (ZMod Nat.zero)ˣ
⊢ x ^ φ Nat.zero = 1
Tactic:
simp
Proof state after:
no goals
Theorem: l1_2_23
Proof state before:
n : ℕ+
x : ℤ
h : IsCoprime x ↑↑n
⊢ x ^ φ ↑n ≡ 1 [ZMOD ↑↑n]
Tactic:
rw [← CharP.intCast_eq_intCast (ZMod n), Int.cast_pow, Int.cast_one, ←
  coe_unitOfIsCoprime' _ h, ← Units.val_pow_eq_pow_val, Units.val_eq_one, ← ZMod.pow_totient' _]
Proof state after:
no goals
Theorem: n1_2_24
Proof state before:
⊢ ∃ G x, (∀ (g : G), IsOfFinAddOrder g) ∧ AddMonoid.exponent G = 0
Tactic:
refine' ⟨ℚ ⧸ AddSubgroup.zmultiples (1 : ℚ), inferInstance, fun g => _, _⟩
Proof state after:
case refine'_1
g : ℚ ⧸ AddSubgroup.zmultiples 1
⊢ IsOfFinAddOrder g

case refine'_2

⊢ AddMonoid.exponent (ℚ ⧸ AddSubgroup.zmultiples 1) = 0
Theorem: n1_2_24
Proof state before:
case refine'_1
g : ℚ ⧸ AddSubgroup.zmultiples 1
⊢ IsOfFinAddOrder g
Tactic:
induction g using QuotientAddGroup.induction_on' with | H g => ?_
Proof state after:
case refine'_1.H
g : ℚ
⊢ IsOfFinAddOrder ↑g
Theorem: n1_2_24
Proof state before:
case refine'_1.H
g : ℚ
⊢ IsOfFinAddOrder ↑g
Tactic:
rw [isOfFinAddOrder_iff_nsmul_eq_zero]
Proof state after:
case refine'_1.H
g : ℚ
⊢ ∃ n, 0 < n ∧ n • ↑g = 0
Theorem: n1_2_24
Proof state before:
case refine'_1.H
g : ℚ
⊢ ∃ n, 0 < n ∧ n • ↑g = 0
Tactic:
refine' ⟨g.den, g.pos, _⟩
Proof state after:
case refine'_1.H
g : ℚ
⊢ g.den • ↑g = 0
Theorem: n1_2_24
Proof state before:
case refine'_1.H
g : ℚ
⊢ g.den • ↑g = 0
Tactic:
rw [← QuotientAddGroup.mk_nsmul, nsmul_eq_mul, QuotientAddGroup.eq_zero_iff,
  AddSubgroup.mem_zmultiples_iff]
Proof state after:
case refine'_1.H
g : ℚ
⊢ ∃ k, k • 1 = ↑g.den * g
Theorem: n1_2_24
Proof state before:
case refine'_1.H
g : ℚ
⊢ ∃ k, k • 1 = ↑g.den * g
Tactic:
use g.num
Proof state after:
case h
g : ℚ
⊢ g.num • 1 = ↑g.den * g
Theorem: n1_2_24
Proof state before:
case h
g : ℚ
⊢ g.num • 1 = ↑g.den * g
Tactic:
rw [Int.smul_one_eq_coe, ← Rat.mul_den_eq_num, mul_comm]
Proof state after:
no goals
Theorem: n1_2_24
Proof state before:
case refine'_2

⊢ AddMonoid.exponent (ℚ ⧸ AddSubgroup.zmultiples 1) = 0
Tactic:
rw [AddMonoid.exponent_eq_zero_iff, AddMonoid.ExponentExists]
Proof state after:
case refine'_2

⊢ ¬∃ n, 0 < n ∧ ∀ (g : ℚ ⧸ AddSubgroup.zmultiples 1), n • g = 0
Theorem: n1_2_24
Proof state before:
case refine'_2

⊢ ¬∃ n, 0 < n ∧ ∀ (g : ℚ ⧸ AddSubgroup.zmultiples 1), n • g = 0
Tactic:
push_neg
Proof state after:
case refine'_2

⊢ ∀ (n : ℕ), 0 < n → ∃ g, n • g ≠ 0
Theorem: n1_2_24
Proof state before:
case refine'_2

⊢ ∀ (n : ℕ), 0 < n → ∃ g, n • g ≠ 0
Tactic:
refine' fun n hn => ⟨(1 / (2 * n) : ℚ), _⟩
Proof state after:
case refine'_2
n : ℕ
hn : 0 < n
⊢ n • ↑(1 / (2 * ↑n)) ≠ 0
Theorem: n1_2_24
Proof state before:
case refine'_2
n : ℕ
hn : 0 < n
⊢ n • ↑(1 / (2 * ↑n)) ≠ 0
Tactic:
rw [← QuotientAddGroup.mk_nsmul, nsmul_eq_mul, Ne.def, QuotientAddGroup.eq_zero_iff,
  AddSubgroup.mem_zmultiples_iff, not_exists]
Proof state after:
case refine'_2
n : ℕ
hn : 0 < n
⊢ ∀ (x : ℤ), ¬x • 1 = ↑n * (1 / (2 * ↑n))
Theorem: n1_2_24
Proof state before:
case refine'_2
n : ℕ
hn : 0 < n
⊢ ∀ (x : ℤ), ¬x • 1 = ↑n * (1 / (2 * ↑n))
Tactic:
refine' fun x => ne_of_apply_ne Rat.den _
Proof state after:
case refine'_2
n : ℕ
hn : 0 < n
x : ℤ
⊢ (x • 1).den ≠ (↑n * (1 / (2 * ↑n))).den
Theorem: n1_2_24
Proof state before:
case refine'_2
n : ℕ
hn : 0 < n
x : ℤ
⊢ (x • 1).den ≠ (↑n * (1 / (2 * ↑n))).den
Tactic:
rw [Int.smul_one_eq_coe, Rat.coe_int_den, one_div, mul_inv_rev, ← mul_assoc,
  mul_inv_cancel ((@Nat.cast_ne_zero ℚ _ _ _).mpr hn.ne'), one_mul, ← Int.cast_two,
  Rat.inv_coe_int_den]
Proof state after:
case refine'_2
n : ℕ
hn : 0 < n
x : ℤ
⊢ 1 ≠ if 2 = 0 then 1 else Int.natAbs 2
Theorem: n1_2_24
Proof state before:
case refine'_2
n : ℕ
hn : 0 < n
x : ℤ
⊢ 1 ≠ if 2 = 0 then 1 else Int.natAbs 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: l1_2_25'
Proof state before:
G : Type u_1
inst✝ : Group G
⊢ d1224 G ∣ Nat.card G
Tactic:
cases fintypeOrInfinite G
Proof state after:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ d1224 G ∣ Nat.card G

case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ d1224 G ∣ Nat.card G
Theorem: l1_2_25'
Proof state before:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ d1224 G ∣ Nat.card G
Tactic:
rw [Nat.card_eq_fintype_card]
Proof state after:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ d1224 G ∣ Fintype.card G
Theorem: l1_2_25'
Proof state before:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ d1224 G ∣ Fintype.card G
Tactic:
exact l1_2_25
Proof state after:
no goals
Theorem: l1_2_25'
Proof state before:
case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ d1224 G ∣ Nat.card G
Tactic:
rw [Nat.card_eq_zero_of_infinite]
Proof state after:
case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ d1224 G ∣ 0
Theorem: l1_2_25'
Proof state before:
case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ d1224 G ∣ 0
Tactic:
exact dvd_zero _
Proof state after:
no goals
Theorem: n1_2_26_ii
Proof state before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ ⁅g, h⁆ = ⁅h, g⁆⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: n1_2_26_ii'
Proof state before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ ⁅g, h⁆ = 1 ↔ g * h = h * g
Tactic:
rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul]
Proof state after:
no goals
Theorem: l1_2_26_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
⊢ ↑(d1226Iii G) = {1} ↔ ∀ (g h : G), g * h = h * g
Tactic:
simp only [d1226Iii]
Proof state after:
G : Type u_1
inst✝ : Group G
⊢ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) = {1} ↔ ∀ (g h : G), g * h = h * g
Theorem: l1_2_26_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
⊢ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) = {1} ↔ ∀ (g h : G), g * h = h * g
Tactic:
rw [Set.ext_iff]
Proof state after:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) ↔ x ∈ {1}) ↔ ∀ (g h : G), g * h = h * g
Theorem: l1_2_26_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) ↔ x ∈ {1}) ↔ ∀ (g h : G), g * h = h * g
Tactic:
simp_rw [← n1_2_26_ii']
Proof state after:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) ↔ x ∈ {1}) ↔ ∀ (g h : G), ⁅g, h⁆ = 1
Theorem: l1_2_26_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) ↔ x ∈ {1}) ↔ ∀ (g h : G), ⁅g, h⁆ = 1
Tactic:
simp only [SetLike.mem_coe, Set.mem_singleton_iff, Set.setOf_exists, Subgroup.closure_iUnion,
  Set.setOf_eq_eq_singleton']
Proof state after:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1) ↔ ∀ (g h : G), ⁅g, h⁆ = 1
Theorem: l1_2_26_iii'
Proof state before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1) ↔ ∀ (g h : G), ⁅g, h⁆ = 1
Tactic:
constructor
Proof state after:
case mp
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1) → ∀ (g h : G), ⁅g, h⁆ = 1

case mpr
G : Type u_1
inst✝ : Group G
⊢ (∀ (g h : G), ⁅g, h⁆ = 1) → ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
Theorem: l1_2_26_iii'
Proof state before:
case mp
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1) → ∀ (g h : G), ⁅g, h⁆ = 1
Tactic:
intro h g g'
Proof state after:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ = 1
Theorem: l1_2_26_iii'
Proof state before:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ = 1
Tactic:
rw [← h]
Proof state after:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
Theorem: l1_2_26_iii'
Proof state before:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
Tactic:
apply Subgroup.mem_iSup_of_mem g
Proof state after:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ ⨆ i, Subgroup.closure {⁅g, i⁆}
Theorem: l1_2_26_iii'
Proof state before:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ ⨆ i, Subgroup.closure {⁅g, i⁆}
Tactic:
apply Subgroup.mem_iSup_of_mem g'
Proof state after:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ Subgroup.closure {⁅g, g'⁆}
Theorem: l1_2_26_iii'
Proof state before:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ Subgroup.closure {⁅g, g'⁆}
Tactic:
rw [Subgroup.mem_closure_singleton]
Proof state after:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ∃ n, ⁅g, g'⁆ ^ n = ⁅g, g'⁆
Theorem: l1_2_26_iii'
Proof state before:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ∃ n, ⁅g, g'⁆ ^ n = ⁅g, g'⁆
Tactic:
use 1
Proof state after:
case h
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ^ 1 = ⁅g, g'⁆
Theorem: l1_2_26_iii'
Proof state before:
case h
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ^ 1 = ⁅g, g'⁆
Tactic:
rw [zpow_one]
Proof state after:
no goals
Theorem: l1_2_26_iii'
Proof state before:
case mpr
G : Type u_1
inst✝ : Group G
⊢ (∀ (g h : G), ⁅g, h⁆ = 1) → ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
Tactic:
intro h g
Proof state after:
case mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ g = 1
Theorem: l1_2_26_iii'
Proof state before:
case mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ g = 1
Tactic:
constructor
Proof state after:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} → g = 1

case mpr.mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g = 1 → g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
Theorem: l1_2_26_iii'
Proof state before:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} → g = 1
Tactic:
intro h'
Proof state after:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
h' : g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
⊢ g = 1
Theorem: l1_2_26_iii'
Proof state before:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
h' : g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
⊢ g = 1
Tactic:
symm
Proof state after:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
h' : g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
⊢ 1 = g
Theorem: l1_2_26_iii'
Proof state before:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
h' : g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
⊢ 1 = g
Tactic:
simpa only [h, ciSup_const, Subgroup.mem_closure_singleton, one_zpow, exists_const] using h'
Proof state after:
no goals
Theorem: l1_2_26_iii'
Proof state before:
case mpr.mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g = 1 → g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
Tactic:
rintro rfl
Proof state after:
case mpr.mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
⊢ 1 ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
Theorem: l1_2_26_iii'
Proof state before:
case mpr.mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
⊢ 1 ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
Tactic:
exact Subgroup.one_mem _
Proof state after:
no goals