awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
apply : (↑X : Set G) ^ (n - 1) = (↑(closure (↑X : Set G)) : Set G)
⊢ False

Tactic:
apply hn
-- 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
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)
inr : ∀ (hm₀ : m > 0), (↑X : Set G) ^ (n - 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

Premises used: Nat.eq_zero_or_pos, 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
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)} n
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:
simp [eq_comm (a := (1 : Set _)), coe_set_eq_one, -Set.subset_singleton_iff,
      hX.coe.not_subset_singleton] at hm

Premises used: Set.subset_singleton_iff, eq_comm, Set.Nontrivial.not_subset_singleton, Finset.Nontrivial.coe, coe_set_eq_one
-- 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
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 - 1) = (↑X : Set G) ^ (n - m + (m - 1))
⊢ (↑X : Set G) ^ (n - 1) = (↑X : Set G) ^ (n - m) * (↑X : Set G) ^ (m - 1)

Tactic:
rw [← pow_add]

Premises used: pow_add
-- 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
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
e_a : n - 1 = n - m + (m - 1)
⊢ (↑X : Set G) ^ (n - 1) = (↑X : Set G) ^ (n - m + (m - 1))

Tactic:
congr 1
-- 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
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
⊢ n - 1 = n - m + (m - 1)

Tactic:
lia
-- 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
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)
rw₁ rw₂ : (↑(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)

Tactic:
rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set]

Premises used: Set.pow_mul_subgroupClosure, Finset.Nontrivial.nonempty, Finset.Nonempty.to_set
-- 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
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)
calc₁ : (↑X : Set G) ^ (n - m) * (↑X : Set G) ^ (m - 1) = (↑(closure (↑X : Set G)) : Set G)
⊢ (↑X : Set G) ^ (n - 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]

Premises used: Subgroup.closure, HSub.hSub, SetLike.coe, OfNat.ofNat
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
inr : ∀ (hX : X.Nontrivial), StrictMono.{0, u_1} (β := Finset G) fun (n : ℕ) ↦ X ^ n
⊢ StrictMono.{0, u_1} (β := Finset G) fun (n : ℕ) ↦ X ^ n

Tactic:
obtain rfl | hX := eq_singleton_or_nontrivial hX₁

Premises used: Finset.eq_singleton_or_nontrivial, rfl
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
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:
simp [closure_singleton_one] at hXclosure

Premises used: Subgroup.closure_singleton_one
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
n : ℕ
h : (↑X : Set G) ^ (n - 1) = (↑(closure (↑X : Set G)) : Set G)
⊢ False

Tactic:
simp [← h, ← coe_pow] at hXclosure

Premises used: Finset.coe_pow
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
⊢ ∀ (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
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
h : ∀ (n : ℕ), (↑X : Set G) ^ (n - 1) ≠ (↑(closure (↑X : Set G)) : Set G)
⊢ StrictMono.{0, u_1} (β := Finset G) fun (n : ℕ) ↦ X ^ n

Tactic:
simpa [h] using pow_right_strictMonoOn hX₁ hX

Premises used: Finset.pow_right_strictMonoOn
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
⊢ HAdd.hAdd (α := ℕ) 0 1 ≤ #(HPow.hPow (β := ℕ) X 0)

Tactic:
simp
-- Module: Mathlib.Geometry.Group.Growth.LinearLowerBound
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
n : ℕ
⊢ (↑(closure (↑X : Set G)) : Set G).Infinite

Tactic:
simp [hXclosure]
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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 : ℕ
set :
  let π : G →* G ⧸ H := QuotientGroup.mk' H;
  card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))
⊢ card (α := G ⧸ H) (image (⇑(QuotientGroup.mk' H) : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))

Tactic:
set π := QuotientGroup.mk' H

Premises used: QuotientGroup.mk'
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
⊢ Set.InjOn φ ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m)

Tactic:
have hφ : Set.InjOn φ (π '' (A ^ m)) := invFunOn_injOn_image ..
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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_1 ∈ (↑A : Set G) ^ m, (π : (a : G) → G ⧸ H) a_1 = a

Tactic:
simpa using ha
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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
⊢ invFunOn (⇑π : (a : G) → G ⧸ H) ((↑A : Set G) ^ m) a ∈ (↑A : Set G) ^ m

Tactic:
have := invFunOn_mem (by simpa using ha)
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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
⊢ invFunOn (⇑π : (a : G) → G ⧸ H) (↑(A ^ m) : Set G) a ∈ A ^ m

Tactic:
norm_cast at this
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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 ^ m) : Set G) a ∈ A ^ m
⊢ φ a ∈ A ^ m

Tactic:
simpa using this
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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

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
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
a : G ⧸ H
ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a
⊢ ∃ a_1 ∈ (↑A : Set G) ^ m, (π : (a : G) → G ⧸ H) a_1 = a

Tactic:
simpa using ha
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
⊢ ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a

Tactic:
have hπφ {a} (ha : a ∈ π '' (A ^ m)) : π (φ a) = a := invFunOn_eq (by simpa using ha)
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
rw rw₁ :
  card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) =
    card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H})
⊢ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) =
    #(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m))) * #({x ∈ A ^ n | x ∈ H})

Tactic:
rw [Finset.card_image_of_injOn (f := φ) (mod_cast hφ)]

Premises used: Finset.card_image_of_injOn
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
rw :
  Set.InjOn (β := G) (fun (p : G × G) ↦ p.1 * p.2)
    ((↑(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m))) : Set G) ×ˢ (↑({x ∈ A ^ n | x ∈ H}) : Set G))
⊢ #(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m))) * #({x ∈ A ^ n | x ∈ H}) ≤
    #(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * {x ∈ A ^ n | x ∈ H})

Tactic:
rw [Finset.card_mul_iff.2]

Premises used: Iff.mpr, Finset.card_mul_iff
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
simp :
  ∀ (a b x : G),
    x ∈ (↑A : Set G) ^ m →
      φ ((π : (a : G) → G ⧸ H) x) = a →
        b ∈ A ^ n →
          b ∈ H →
            ∀ (a_5 b_1 x : G),
              x ∈ (↑A : Set G) ^ m →
                φ ((π : (a : G) → G ⧸ H) x) = a_5 → b_1 ∈ A ^ n → b_1 ∈ H → a * b = a_5 * b_1 → a = a_5 ∧ b = b_1
⊢ Set.InjOn (β := G) (fun (p : G × G) ↦ p.1 * p.2)
    ((↑(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m))) : Set G) ×ˢ (↑({x ∈ A ^ n | x ∈ H}) : Set G))

Tactic:
simp only [Set.InjOn, coe_image, coe_pow, coe_filter, Set.mem_prod, Set.mem_image,
        exists_exists_and_eq_and, Set.mem_setOf_eq, and_imp, forall_exists_index, Prod.forall,
        Prod.mk.injEq]

Premises used: Finset.coe_filter, and_imp, Set.mem_image, forall_exists_index, Finset.coe_image, Set.mem_setOf_eq, Set.mem_prod, exists_exists_and_eq_and, Prod.mk.injEq, Prod.forall, Set.InjOn, Finset.coe_pow
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ (↑A : Set G) ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ (↑A : Set G) ^ m
ha₂ : a₂ ∈ H
hab : φ ((π : (a : G) → G ⧸ H) b₁) * a₁ = φ ((π : (a : G) → G ⧸ H) b₂) * a₂
⊢ Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a₁ : G ⧸ H) (1 : G ⧸ H)

Tactic:
have hπa₁ : π a₁ = 1 := (QuotientGroup.eq_one_iff _).2 ha₁
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ (↑A : Set G) ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ (↑A : Set G) ^ m
ha₂ : a₂ ∈ H
hab : φ ((π : (a : G) → G ⧸ H) b₁) * a₁ = φ ((π : (a : G) → G ⧸ H) b₂) * a₂
hπa₁ : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a₁ : G ⧸ H) (1 : G ⧸ H)
⊢ Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a₂ : G ⧸ H) (1 : G ⧸ H)

Tactic:
have hπa₂ : π a₂ = 1 := (QuotientGroup.eq_one_iff _).2 ha₂
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ (↑A : Set G) ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ (↑A : Set G) ^ m
ha₂ : a₂ ∈ H
hab : φ ((π : (a : G) → G ⧸ H) b₁) * a₁ = φ ((π : (a : G) → G ⧸ H) b₂) * a₂
hπa₁ : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a₁ : G ⧸ H) (1 : G ⧸ H)
hπa₂ : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a₂ : G ⧸ H) (1 : G ⧸ H)
⊢ Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) b₁ : G ⧸ H) ((π : (a : G) → G ⧸ H) b₂ : G ⧸ H)

Tactic:
simpa [hπφ, Set.mem_image_of_mem π, hb₁, hb₂, hπa₁, hπa₂] using congr(π $hab)

Premises used: Set.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ (↑A : Set G) ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ (↑A : Set G) ^ m
ha₂ : a₂ ∈ H
hab : φ ((π : (a : G) → G ⧸ H) b₁) * a₁ = φ ((π : (a : G) → G ⧸ H) b₂) * a₂
hπa₁ : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a₁ : G ⧸ H) (1 : G ⧸ H)
hπa₂ : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a₂ : G ⧸ H) (1 : G ⧸ H)
⊢ Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) b₁ : G ⧸ H) ((π : (a : G) → G ⧸ H) b₂ : G ⧸ H)

Tactic:
have hπb : π b₁ = π b₂ := by
        simpa [hπφ, Set.mem_image_of_mem π, hb₁, hb₂, hπa₁, hπa₂] using congr(π $hab)
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ (↑A : Set G) ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ (↑A : Set G) ^ m
ha₂ : a₂ ∈ H
hab : φ ((π : (a : G) → G ⧸ H) b₁) * a₁ = φ ((π : (a : G) → G ⧸ H) b₂) * a₂
hπa₁ : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a₁ : G ⧸ H) (1 : G ⧸ H)
hπa₂ : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a₂ : G ⧸ H) (1 : G ⧸ H)
hπb : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) b₁ : G ⧸ H) ((π : (a : G) → G ⧸ H) b₂ : G ⧸ H)
⊢ φ ((π : (a : G) → G ⧸ H) b₁) = φ ((π : (a : G) → G ⧸ H) b₂) ∧ a₁ = a₂

Tactic:
simp_all
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
a : image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * {x ∈ A ^ n | x ∈ H} ⊆ A ^ (m + n)
⊢ #(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * {x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))

Tactic:
gcongr
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
a : ∀ a ∈ A ^ m, ∀ y ∈ A ^ n, y ∈ H → φ ((π : (a : G) → G ⧸ H) a) * y ∈ A ^ m * A ^ n
⊢ image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * {x ∈ A ^ n | x ∈ H} ⊆ A ^ (m + n)

Tactic:
simp only [mul_subset_iff, mem_image, exists_exists_and_eq_and, Finset.mem_filter, and_imp,
        forall_exists_index, forall_apply_eq_imp_iff₂, pow_add]

Premises used: Finset.mem_image, and_imp, pow_add, forall_exists_index, exists_exists_and_eq_and, Finset.mul_subset_iff, Finset.mem_filter, forall_apply_eq_imp_iff₂