awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
hn₁ : ¬n = 1
⊢ (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
have this₁ : ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
  (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
Tactic: simp +contextual only [pow_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
⊢ X ^ (n + 0) = X ^ n
have zero : X ^ n = X ^ n
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
d : ℕ
hd : X ^ (n + d) = X ^ n
⊢ X ^ (n + (d + 1)) = X ^ n
have succ : ∀ (hXn : X ^ n = X ^ n * X) (hn₁ : ¬n = 1)
  (this :
    ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
      (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G))
  (d : ℕ) (hd : X ^ (n + d) = X ^ n), X ^ (n + (d + 1)) = X ^ n
Tactic: rw [pow_add, pow_one] at hXn
Cleared hypotheses: hXn, hn₁, this, d, hd
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ n * X
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
d : ℕ
hd : X ^ (n + d) = X ^ n
⊢ X ^ (n + (d + 1)) = X ^ n
have succ : X ^ (n + d + 1) = X ^ n
Tactic: rw [← add_assoc, pow_add, pow_one, hd, ← hXn]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ n * X
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
d : ℕ
hd : X ^ (n + d) = X ^ n
succ : X ^ (n + d + 1) = X ^ n
⊢ X ^ (n + (d + 1)) = X ^ n
have succ₁ : X ^ (n + d) * HPow.hPow (β := ℕ) X 1 = X ^ n
Tactic: rw [← add_assoc, pow_add, pow_one, hd, ← hXn]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ n * X
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
d : ℕ
hd : X ^ (n + d) = X ^ n
succ : X ^ (n + d + 1) = X ^ n
succ₁ : X ^ (n + d) * HPow.hPow (β := ℕ) X 1 = X ^ n
⊢ X ^ (n + (d + 1)) = X ^ n
have succ₂ : X ^ (n + d) * X = X ^ n
Tactic: rw [← add_assoc, pow_add, pow_one, hd, ← hXn]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ n * X
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
d : ℕ
hd : X ^ (n + d) = X ^ n
succ : X ^ (n + d + 1) = X ^ n
succ₁ : X ^ (n + d) * HPow.hPow (β := ℕ) X 1 = X ^ n
succ₂ : X ^ (n + d) * X = X ^ n
⊢ X ^ (n + (d + 1)) = X ^ n
have succ₃ : X ^ n * X = X ^ n
Tactic: rw [← add_assoc, pow_add, pow_one, hd, ← hXn]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ n * X
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
d : ℕ
hd : X ^ (n + d) = X ^ n
succ : X ^ (n + d + 1) = X ^ n
succ₁ : X ^ (n + d) * HPow.hPow (β := ℕ) X 1 = X ^ n
succ₂ : X ^ (n + d) * X = X ^ n
succ₃ : X ^ n * X = X ^ n
⊢ X ^ (n + (d + 1)) = X ^ n
have succ₄ : X ^ n = X ^ n
Tactic: rw [← add_assoc, pow_add, pow_one, hd, ← hXn]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
d : ℕ
⊢ X ^ (n + d) = X ^ n
have zero : X ^ (n + 0) = X ^ n
Tactic: induction d with
      | zero => rw [add_zero]
      | succ d hd =>
        rw [pow_add, pow_one] at hXn
        rw [← add_assoc, pow_add, pow_one, hd, ← hXn]
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
d : ℕ
zero : X ^ (n + 0) = X ^ n
⊢ X ^ (n + d) = X ^ n
have succ : ∀ (d : ℕ) (hd : X ^ (n + d) = X ^ n), X ^ (n + (d + 1)) = X ^ n
Tactic: induction d with
      | zero => rw [add_zero]
      | succ d hd =>
        rw [pow_add, pow_one] at hXn
        rw [← add_assoc, pow_add, pow_one, hd, ← hXn]
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
    (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
⊢ (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
have hXn₁ : ∀ (d : ℕ), X ^ (n + d) = X ^ n
Tactic: replace hXn d : X ^ (n + d) = X ^ n := by
      induction d with
      | zero => rw [add_zero]
      | succ d hd =>
        rw [pow_add, pow_one] at hXn
        rw [← add_assoc, pow_add, pow_one, hd, ← hXn]
Cleared hypotheses: hXn
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : DecidableEq G_1
X_1 : Finset G_1
n_1 : ℕ
G : Type u_1
inst_2 : Group G
inst_3 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : n = 1
⊢ (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
have subst : ∀ (hn : Ne (α := ℕ) 1 0) (hXn : HPow.hPow (β := ℕ) X 1 = X ^ HAdd.hAdd (α := ℕ) 1 1),
  HPow.hPow (β := ℕ) (↑X : Set G) 1 = (↑(closure (HPow.hPow (β := ℕ) (↑X : Set G) 1)) : Set G)
Tactic: subst hn₁
Cleared hypotheses: n, hn, hXn, hn₁
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : DecidableEq G_1
X_1 : Finset G_1
n : ℕ
G : Type u_1
inst_2 : Group G
inst_3 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : Ne (α := ℕ) 1 0
hXn : HPow.hPow (β := ℕ) X 1 = X ^ HAdd.hAdd (α := ℕ) 1 1
⊢ HPow.hPow (β := ℕ) (↑X : Set G) 1 = (↑(closure (HPow.hPow (β := ℕ) (↑X : Set G) 1)) : Set G)
have simp : ∀ (hn : True) (hXn : X = HPow.hPow (β := ℕ) X 2), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
Tactic: simp only [ne_eq, one_ne_zero, not_false_eq_true, Nat.reduceAdd, pow_one] at *
Cleared hypotheses: hn, hXn
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (hypothesis)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : DecidableEq G_1
X_1 : Finset G_1
n : ℕ
G : Type u_1
inst_2 : Group G
inst_3 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = HPow.hPow (β := ℕ) X 2
x y : G
hx : x ∈ (↑X : Set G)
hy : y ∈ (↑X : Set G)
⊢ x * y ∈ (↑X : Set G)
have hx₁ : x ∈ X
Tactic: norm_cast at *
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (hypothesis)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : DecidableEq G_1
X_1 : Finset G_1
n : ℕ
G : Type u_1
inst_2 : Group G
inst_3 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = HPow.hPow (β := ℕ) X 2
x y : G
hx : x ∈ (↑X : Set G)
hy : y ∈ (↑X : Set G)
hx₁ : x ∈ X
⊢ x * y ∈ (↑X : Set G)
have hy₁ : y ∈ X
Tactic: norm_cast at *
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (hypothesis)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : DecidableEq G_1
X_1 : Finset G_1
n : ℕ
G : Type u_1
inst_2 : Group G
inst_3 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = HPow.hPow (β := ℕ) X 2
x : G
hx : x ∈ (↑X : Set G)
⊢ x⁻¹ ∈ (↑X : Set G)
have hx₁ : x ∈ X
Tactic: norm_cast at *
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (hypothesis)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : DecidableEq G_1
X_1 : Finset G_1
n : ℕ
G : Type u_1
inst_2 : Group G
inst_3 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = HPow.hPow (β := ℕ) X 2
x : G
hx : x ∈ X
⊢ x⁻¹ ∈ X
have this : x • X ⊆ X
Tactic: have : x • X ⊆ X := by
        simpa [← hXn, add_assoc, ← sq] using smul_finset_subset_mul (t := X) hx
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (hypothesis)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : DecidableEq G_1
X_1 : Finset G_1
n : ℕ
G : Type u_1
inst_2 : Group G
inst_3 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = HPow.hPow (β := ℕ) X 2
x : G
hx : x ∈ X
this : x • X ⊆ X
⊢ x⁻¹ ∈ X
have this₁ : x • X = X
Tactic: have : x • X = X := eq_of_subset_of_card_le this (card_smul_finset ..).ge
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (hypothesis)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : DecidableEq G_1
X_1 : Finset G_1
n : ℕ
G : Type u_1
inst_2 : Group G
inst_3 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = HPow.hPow (β := ℕ) X 2
x : G
hx : x ∈ X
this_1 : x • X ⊆ X
this : x • X = X
⊢ x⁻¹ ∈ X
have this₁ : X = x⁻¹ • X
Tactic: rw [← eq_inv_smul_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : DecidableEq G_1
X_1 : Finset G_1
n : ℕ
G : Type u_1
inst_2 : Group G
inst_3 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = HPow.hPow (β := ℕ) X 2
x : G
hx : x ∈ X
this_1 : x • X ⊆ X
this : X = x⁻¹ • X
⊢ x⁻¹ ∈ X
have rw : x⁻¹ ∈ x⁻¹ • X
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
⊢ StrictMonoOn.{0, u_1} (β := Finset G) (fun (n : ℕ) ↦ X ^ n)
    {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)}
have refine : ∀ ⦃x : ℕ⦄ (hx : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} x)
  ⦃y : ℕ⦄ (hy : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} y),
  Set.Icc x y ⊆ {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)}
Tactic: refine strictMonoOn_of_lt_add_one ⟨?_⟩ fun n _ _ hn ↦
    pow_ssubset_pow_succ_of_pow_ne_closure hX₁ hX hn
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} n
m : ℕ
hmn : m ≤ n
hm : (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
⊢ False
have apply : (↑X : Set G) ^ (n - 1) = (↑(closure (↑X : Set G)) : Set G)
Tactic: apply hn
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} n
m : ℕ
hmn : m ≤ n
hm : (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
⊢ (↑X : Set G) ^ (n - 1) = (↑(closure (↑X : Set G)) : Set G)
have inl : ∀ (hmn : 0 ≤ n) (hm : (↑X : Set G) ^ HSub.hSub (α := ℕ) 0 1 = (↑(closure (↑X : Set G)) : Set G)),
  (↑X : Set G) ^ (n - 1) = (↑(closure (↑X : Set G)) : Set G)
Tactic: obtain rfl | hm₀ := m.eq_zero_or_pos
Cleared hypotheses: m, hmn, hm
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} n
m : ℕ
hmn : m ≤ n
hm : (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
inl :
  ∀ (hmn : 0 ≤ n) (hm : (↑X : Set G) ^ HSub.hSub (α := ℕ) 0 1 = (↑(closure (↑X : Set G)) : Set G)),
    (↑X : Set G) ^ (n - 1) = (↑(closure (↑X : Set G)) : Set G)
⊢ (↑X : Set G) ^ (n - 1) = (↑(closure (↑X : Set G)) : Set G)
have inr : ∀ (hm₀ : m > 0), (↑X : Set G) ^ (n - 1) = (↑(closure (↑X : Set G)) : Set G)
Tactic: obtain rfl | hm₀ := m.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} n
m : ℕ
hmn : m ≤ n
hm : (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
hm₀ : m > 0
⊢ (↑X : Set G) ^ (n - 1) = (↑X : Set G) ^ (n - m) * (↑X : Set G) ^ (m - 1)
have rw : (↑X : Set G) ^ (n - 1) = (↑X : Set G) ^ (n - m + (m - 1))
Tactic: rw [← pow_add]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} n
m : ℕ
hmn : m ≤ n
hm : (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
hm₀ : m > 0
⊢ (↑X : Set G) ^ (n - 1) = (↑X : Set G) ^ (n - m + (m - 1))
have e_a : n - 1 = n - m + (m - 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} n
m : ℕ
hmn : m ≤ n
hm : (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
hm₀ : m > 0
⊢ (↑X : Set G) ^ (n - m) * (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
have rw : (↑X : Set G) ^ (n - m) * (↑(closure (↑X : Set G)) : Set G) = (↑(closure (↑X : Set G)) : Set G)
Tactic: rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} n
m : ℕ
hmn : m ≤ n
hm : (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
hm₀ : m > 0
rw : (↑X : Set G) ^ (n - m) * (↑(closure (↑X : Set G)) : Set G) = (↑(closure (↑X : Set G)) : Set G)
⊢ (↑X : Set G) ^ (n - m) * (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
have rw₁ : (↑(closure (↑X : Set G)) : Set G) = (↑(closure (↑X : Set G)) : Set G)
Tactic: rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} n
m : ℕ
hmn : m ≤ n
hm : (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
hm₀ : m > 0
⊢ (↑X : Set G) ^ (n - 1) = (↑(closure (↑X : Set G)) : Set G)
have calc : (↑X : Set G) ^ (n - 1) = (↑X : Set G) ^ (n - m) * (↑X : Set G) ^ (m - 1)
Tactic: calc (X : Set G) ^ (n - 1)
    _ = X ^ (n - m) * X ^ (m - 1) := by rw [← pow_add]; congr 1; lia
    _ = closure (X : Set G) := by rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} n
m : ℕ
hmn : m ≤ n
hm : (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
hm₀ : m > 0
calc : (↑X : Set G) ^ (n - 1) = (↑X : Set G) ^ (n - m) * (↑X : Set G) ^ (m - 1)
⊢ (↑X : Set G) ^ (n - 1) = (↑(closure (↑X : Set G)) : Set G)
have calc₁ : (↑X : Set G) ^ (n - m) * (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
Tactic: calc (X : Set G) ^ (n - 1)
    _ = X ^ (n - m) * X ^ (m - 1) := by rw [← pow_add]; congr 1; lia
    _ = closure (X : Set G) := by rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure (↑X : Set G)) : Set G).Infinite
⊢ StrictMono.{0, u_1} (β := Finset G) fun (n : ℕ) ↦ X ^ n
have inl : ∀ (hX₁ : Membership.mem (γ := Finset G) {1} 1) (hXclosure : (↑(closure (↑{1} : Set G)) : Set G).Infinite),
  StrictMono.{0, u_1} (β := Finset G) fun (n : ℕ) ↦ HPow.hPow (α := Finset G) {1} n
Tactic: obtain rfl | hX := eq_singleton_or_nontrivial hX₁
Cleared hypotheses: X, hX₁, hXclosure
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure (↑X : Set G)) : Set G).Infinite
inl :
  ∀ (hX₁ : Membership.mem (γ := Finset G) {1} 1) (hXclosure : (↑(closure (↑{1} : Set G)) : Set G).Infinite),
    StrictMono.{0, u_1} (β := Finset G) fun (n : ℕ) ↦ HPow.hPow (α := Finset G) {1} n
⊢ StrictMono.{0, u_1} (β := Finset G) fun (n : ℕ) ↦ X ^ n
have inr : ∀ (hX : X.Nontrivial), StrictMono.{0, u_1} (β := Finset G) fun (n : ℕ) ↦ X ^ n
Tactic: obtain rfl | hX := eq_singleton_or_nontrivial hX₁
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure (↑X : Set G)) : Set G).Infinite
hX : X.Nontrivial
⊢ StrictMono.{0, u_1} (β := Finset G) fun (n : ℕ) ↦ X ^ n
have h : ∀ (n : ℕ), (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)
Tactic: have h n : (X ^ (n - 1) : Set G) ≠ closure (X : Set G) :=
    fun h ↦ by simp [← h, ← coe_pow] at hXclosure
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : (b : G ⧸ H) → G := invFunOn (⇑π : (a : G) → G ⧸ H) ((↑A : Set G) ^ m)
⊢ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))
have hφ : Set.InjOn φ ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m)
Tactic: have hφ : Set.InjOn φ (π '' (A ^ m)) := invFunOn_injOn_image ..
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : (b : G ⧸ H) → G := invFunOn (⇑π : (a : G) → G ⧸ H) ((↑A : Set G) ^ m)
hφ : Set.InjOn φ ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m)
a : G ⧸ H
ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a
⊢ φ a ∈ A ^ m
have this : invFunOn (⇑π : (a : G) → G ⧸ H) ((↑A : Set G) ^ m) a ∈ (↑A : Set G) ^ m
Tactic: have := invFunOn_mem (by simpa using ha)
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : (b : G ⧸ H) → G := invFunOn (⇑π : (a : G) → G ⧸ H) ((↑A : Set G) ^ m)
hφ : Set.InjOn φ ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m)
a : G ⧸ H
ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a
this : invFunOn (⇑π : (a : G) → G ⧸ H) ((↑A : Set G) ^ m) a ∈ (↑A : Set G) ^ m
⊢ φ a ∈ A ^ m
have this₁ : invFunOn (⇑π : (a : G) → G ⧸ H) (↑(A ^ m) : Set G) a ∈ A ^ m
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : (b : G ⧸ H) → G := invFunOn (⇑π : (a : G) → G ⧸ H) ((↑A : Set G) ^ m)
hφ : Set.InjOn φ ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m)
⊢ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))
have hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
Tactic: have hφA {a} (ha : a ∈ π '' (A ^ m)) : φ a ∈ A ^ m := by
    have := invFunOn_mem (by simpa using ha)
    norm_cast at this
    simpa using this