awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : MetricSpace P
inst_6 : MeasurableSpace P
inst_7 : BorelSpace P
inst_8 : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) = 1
hrank' : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) :=
  ContinuousLinearEquiv.trans (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv)
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) ⋯)
hf :
  MeasurableEmbedding (α := ℝ) (β := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
    (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction)
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) :=
  Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) x) p ⋯
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) :=
  Function.comp (β := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
    (⇑(IsometryEquiv.vaddConst p') : (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
    (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction)
hadd :
  MeasurableEmbedding.{u_3, u_4} (α := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) (β :=
    ↥(AffineSubspace.mk' p (ℝ ∙ v)))
    (⇑(IsometryEquiv.vaddConst p') : (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
hg : MeasurableEmbedding g
⊢ μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v))) ‖v‖ₑ (map g volume)

Tactic:
have hm : μHE[finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).direction] =
      ‖v‖ₑ • (volume : Measure ℝ).map g := by
    unfold g
    rw [euclideanHausdorffMeasure_eq p', ← map_map hadd.measurable hf.measurable,
      ← Measure.map_smul]
    congr
    let v' : (AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, by simp⟩
    suffices volume = ‖v'‖ₑ • volume.map f by simpa [v']
    exact volume_eq_of_finrank_eq_one hrank (by simpa [v'] using hv)
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : MetricSpace P
inst_6 : MeasurableSpace P
inst_7 : BorelSpace P
inst_8 : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) = 1
hrank' : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) :=
  ContinuousLinearEquiv.trans (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv)
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) ⋯)
hf :
  MeasurableEmbedding (α := ℝ) (β := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
    (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction)
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) :=
  Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) x) p ⋯
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) :=
  Function.comp (β := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
    (⇑(IsometryEquiv.vaddConst p') : (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
    (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction)
hadd :
  MeasurableEmbedding.{u_3, u_4} (α := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) (β :=
    ↥(AffineSubspace.mk' p (ℝ ∙ v)))
    (⇑(IsometryEquiv.vaddConst p') : (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
hg : MeasurableEmbedding g
hm :
  μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v))) ‖v‖ₑ (map g volume)
x : ℝ
⊢ x • v +ᵥ p = (↑(g x) : P)

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : MetricSpace P
inst_6 : MeasurableSpace P
inst_7 : BorelSpace P
inst_8 : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) = 1
hrank' : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) :=
  ContinuousLinearEquiv.trans (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv)
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) ⋯)
hf :
  MeasurableEmbedding (α := ℝ) (β := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
    (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction)
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) :=
  Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) x) p ⋯
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) :=
  Function.comp (β := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
    (⇑(IsometryEquiv.vaddConst p') : (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
    (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction)
hadd :
  MeasurableEmbedding.{u_3, u_4} (α := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) (β :=
    ↥(AffineSubspace.mk' p (ℝ ∙ v)))
    (⇑(IsometryEquiv.vaddConst p') : (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
hg : MeasurableEmbedding g
hm :
  μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v))) ‖v‖ₑ (map g volume)
⊢ ∀ (x : ℝ), x • v +ᵥ p = (↑(g x) : P)

Tactic:
have hx (x : ℝ) : x • v +ᵥ p = g x := by rfl
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : (↑X : Set G) ^ n ≠ (↑(closure (↑X : Set G)) : Set G)
inl :
  ∀ (hXclosure : HPow.hPow (β := ℕ) (↑X : Set G) 0 ≠ (↑(closure (↑X : Set G)) : Set G)),
    HPow.hPow (β := ℕ) X 0 ⊂ X ^ HAdd.hAdd (α := ℕ) 0 1
inr : ∀ (hn : n ≠ 0), X ^ n ⊂ X ^ (n + 1)
⊢ X ^ n ⊂ X ^ (n + 1)

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : HPow.hPow (β := ℕ) (↑X : Set G) 0 ≠ (↑(closure (↑X : Set G)) : Set G)
⊢ HPow.hPow (β := ℕ) X 0 ⊂ X ^ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simpa [ssubset_iff_subset_not_subset, hX₁, -Finset.subset_singleton_iff]
      using hX.not_subset_singleton

Premises used: ssubset_iff_subset_not_subset, Finset.Nontrivial.not_subset_singleton, Finset.subset_singleton_iff
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : (↑X : Set G) ^ n ≠ (↑(closure (↑X : Set G)) : Set G)
hn : n ≠ 0
⊢ X ^ n ⊂ X ^ (n + 1)

Tactic:
(pow_subset_pow_right hX₁ <| n.le_add_right _).ssubset_of_ne ?_

Premises used: Finset.pow_subset_pow_right, Set.Mem, Nat.le_add_right, setOf, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : (↑X : Set G) ^ n ≠ (↑(closure (↑X : Set G)) : Set G)
hn : n ≠ 0
inr : X ^ n ≠ X ^ (n + 1)
⊢ X ^ n ⊂ X ^ (n + 1)

Tactic:
refine (pow_subset_pow_right hX₁ <| n.le_add_right _).ssubset_of_ne ?_

Premises used: Finset.pow_subset_pow_right, Nat.le_add_right, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : (↑X : Set G) ^ n ≠ (↑(closure (↑X : Set G)) : Set G)
hn : n ≠ 0
inr : ∀ (hXn : X ^ n = X ^ (n + 1)), (↑X : Set G) ^ n = (↑(closure (↑X : Set G)) : Set G)
⊢ X ^ n ≠ X ^ (n + 1)

Tactic:
contrapose hXclosure with hXn
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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)
inr : (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
⊢ (↑X : Set G) ^ n = (↑(closure (↑X : Set G)) : Set G)

Tactic:
rw [← closure_pow (mod_cast hX₁) hn]

Premises used: Subgroup.closure_pow
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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)
inr :
  ∀
    (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)
wlog :
  ∀ {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)
⊢ (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)

Tactic:
wlog hn₁ : n = 1
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
⊢ ∀ {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

Premises used: pow_one
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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)
zero zero₁ : X ^ n = X ^ n
⊢ X ^ (n + 0) = X ^ n

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
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
⊢ X ^ (n + (d + 1)) = X ^ n

Tactic:
rw [pow_add, pow_one] at hXn

Premises used: pow_add, pow_one
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
succ₄ succ₅ : X ^ n = X ^ n
⊢ X ^ (n + (d + 1)) = X ^ n

Tactic:
rw [← add_assoc, pow_add, pow_one, hd, ← hXn]

Premises used: add_assoc, pow_add, pow_one
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
succ : ∀ (d : ℕ) (hd : X ^ (n + d) = X ^ n), X ^ (n + (d + 1)) = X ^ n
⊢ X ^ (n + d) = 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]

Premises used: add_assoc, pow_add, pow_one, add_zero
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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

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]
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
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)
hXn : ∀ (d : ℕ), X ^ (n + d) = X ^ n
⊢ HPow.hPow (β := ℕ) (X ^ n) 1 = (X ^ n) ^ HAdd.hAdd (α := ℕ) 1 1

Tactic:
simp [hXn, ← pow_mul, mul_two]

Premises used: pow_mul, mul_two
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
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)
hXn : ∀ (d : ℕ), X ^ (n + d) = X ^ n
⊢ Eq (α := ℕ) 1 1

Tactic:
simp
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
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)
hXn : ∀ (d : ℕ), X ^ (n + d) = X ^ n
⊢ (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)

Tactic:
exact mod_cast this (one_mem_pow hX₁) (hX.pow hn) one_ne_zero
      (by simp [hXn, ← pow_mul, mul_two]) (by simp)

Premises used: Finset.one_mem_pow, Finset.Nontrivial.pow, one_ne_zero
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
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)
⊢ (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)

Tactic:
subst hn₁
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
simp : ∀ (hn : True) (hXn : X = HPow.hPow (β := ℕ) X 2), (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)
⊢ HPow.hPow (β := ℕ) (↑X : Set G) 1 = (↑(closure (HPow.hPow (β := ℕ) (↑X : Set G) 1)) : Set G)

Tactic:
simp only [ne_eq, one_ne_zero, not_false_eq_true, Nat.reduceAdd, pow_one] at *

Premises used: Nat.reduceAdd, ne_eq, pow_one, one_ne_zero, not_false_eq_true
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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 ∈ X

Tactic:
norm_cast at *
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
⊢ y ∈ X

Tactic:
norm_cast at *
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
hy : y ∈ X
⊢ x * y ∈ X

Tactic:
simpa [← hXn, ← sq] using mul_mem_mul hx hy

Premises used: sq, Finset.mul_mem_mul
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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

Tactic:
norm_cast at *
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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 ⊆ X

Tactic:
simpa [← hXn, add_assoc, ← sq] using smul_finset_subset_mul (t := X) hx

Premises used: add_assoc, sq, Finset.smul_finset_subset_mul
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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 ⊆ X

Tactic:
have : x • X ⊆ X := by
        simpa [← hXn, add_assoc, ← sq] using smul_finset_subset_mul (t := X) hx
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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 = X

Tactic:
have : x • X = X := eq_of_subset_of_card_le this (card_smul_finset ..).ge
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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⁻¹ • X

Tactic:
rw [← eq_inv_smul_iff] at this

Premises used: eq_inv_smul_iff
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
rw : x⁻¹ ∈ x⁻¹ • X
⊢ x⁻¹ ∈ X

Tactic:
rw [this]
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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⁻¹ • X

Tactic:
simpa [mem_inv_smul_finset_iff]

Premises used: Finset.mem_inv_smul_finset_iff
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
Xgp : Subgroup G := { carrier := (↑X : Set G), mul_mem' := ⋯, one_mem' := hX₁, inv_mem' := ⋯ }
⊢ (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)

Tactic:
subset_closure.antisymm <| (closure_le Xgp).2 subset_rfl

Premises used: Iff.mpr, Subgroup.closure_le, Subgroup.subset_closure, HasSubset.Subset.antisymm, subset_rfl
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
Xgp : Subgroup G := { carrier := (↑X : Set G), mul_mem' := ⋯, one_mem' := hX₁, inv_mem' := ⋯ }
⊢ (↑X : Set G) = (↑(closure (↑X : Set G)) : Set G)

Tactic:
exact subset_closure.antisymm <| (closure_le Xgp).2 subset_rfl

Premises used: Iff.mpr, Subgroup.closure_le, Subgroup.subset_closure, HasSubset.Subset.antisymm, subset_rfl
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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)}

Tactic:
strictMonoOn_of_lt_add_one ⟨?_⟩ fun n _ _ hn ↦
    pow_ssubset_pow_succ_of_pow_ne_closure hX₁ hX hn

Premises used: strictMonoOn_of_lt_add_one, Set.OrdConnected.mk, Finset.pow_ssubset_pow_succ_of_pow_ne_closure
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
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)}
⊢ StrictMonoOn.{0, u_1} (β := Finset G) (fun (n : ℕ) ↦ X ^ n)
    {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

Premises used: strictMonoOn_of_lt_add_one, Set.OrdConnected.mk