awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
⊢ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))
have 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
Tactic: have hπφ {a} (ha : a ∈ π '' (A ^ m)) : π (φ a) = a := invFunOn_eq (by simpa using ha)
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
⊢ 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})
have 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})
Tactic: rw [Finset.card_image_of_injOn (f := φ) (mod_cast hφ)]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
⊢ #(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})
have 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))
Tactic: rw [Finset.card_mul_iff.2]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
⊢ 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))
have 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
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]
-- 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)
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₂
⊢ φ ((π : (a : G) → G ⧸ H) b₁) = φ ((π : (a : G) → G ⧸ H) b₂) ∧ a₁ = a₂
have hπ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₁
-- 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)
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)
⊢ φ ((π : (a : G) → G ⧸ H) b₁) = φ ((π : (a : G) → G ⧸ H) b₂) ∧ a₁ = a₂
have hπ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₂
-- 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)
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)
⊢ φ ((π : (a : G) → G ⧸ H) b₁) = φ ((π : (a : G) → G ⧸ H) b₂) ∧ a₁ = a₂
have hπb : 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)
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
⊢ #(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * {x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))
have a : image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * {x ∈ A ^ n | x ∈ H} ⊆ A ^ (m + n)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
⊢ image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * {x ∈ A ^ n | x ∈ H} ⊆ A ^ (m + n)
have a : ∀ a ∈ A ^ m, ∀ y ∈ A ^ n, y ∈ H → φ ((π : (a : G) → G ⧸ H) a) * y ∈ A ^ m * A ^ 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]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
⊢ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))
have A₁ : 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: calc
    #((A ^ m).image π) * #{x ∈ A ^ n | x ∈ H}
    _ = #(((A ^ m).image π).image φ) * #{x ∈ A ^ n | x ∈ H} := by
      rw [Finset.card_image_of_injOn (f := φ) (mod_cast hφ)]
    _ ≤ #(((A ^ m).image π).image φ * {x ∈ A ^ n | x ∈ H}) := by
      rw [Finset.card_mul_iff.2]
      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]
      rintro _ a₁ b₁ hb₁ rfl - ha₁ _ a₂ b₂ hb₂ rfl - ha₂ hab
      have hπa₁ : π a₁ = 1 := (QuotientGroup.eq_one_iff _).2 ha₁
      have hπa₂ : π a₂ = 1 := (QuotientGroup.eq_one_iff _).2 ha₂
      have hπb : π b₁ = π b₂ := by
        simpa [hπφ, Set.mem_image_of_mem π, hb₁, hb₂, hπa₁, hπa₂] using congr(π $hab)
      simp_all
    _ ≤ #(A ^ (m + n)) := by
      gcongr
      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]
      rintro a ha b hb -
      exact mul_mem_mul (hφA <| Set.mem_image_of_mem _ <| mod_cast ha) hb
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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₁ :
  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})
⊢ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))
have A₂ : #(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: calc
    #((A ^ m).image π) * #{x ∈ A ^ n | x ∈ H}
    _ = #(((A ^ m).image π).image φ) * #{x ∈ A ^ n | x ∈ H} := by
      rw [Finset.card_image_of_injOn (f := φ) (mod_cast hφ)]
    _ ≤ #(((A ^ m).image π).image φ * {x ∈ A ^ n | x ∈ H}) := by
      rw [Finset.card_mul_iff.2]
      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]
      rintro _ a₁ b₁ hb₁ rfl - ha₁ _ a₂ b₂ hb₂ rfl - ha₂ hab
      have hπa₁ : π a₁ = 1 := (QuotientGroup.eq_one_iff _).2 ha₁
      have hπa₂ : π a₂ = 1 := (QuotientGroup.eq_one_iff _).2 ha₂
      have hπb : π b₁ = π b₂ := by
        simpa [hπφ, Set.mem_image_of_mem π, hb₁, hb₂, hπa₁, hπa₂] using congr(π $hab)
      simp_all
    _ ≤ #(A ^ (m + n)) := by
      gcongr
      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]
      rintro a ha b hb -
      exact mul_mem_mul (hφA <| Set.mem_image_of_mem _ <| mod_cast ha) hb
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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₁ :
  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})
A₂ :
  #(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})
⊢ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))
have A₃ : #(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * {x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))
Tactic: calc
    #((A ^ m).image π) * #{x ∈ A ^ n | x ∈ H}
    _ = #(((A ^ m).image π).image φ) * #{x ∈ A ^ n | x ∈ H} := by
      rw [Finset.card_image_of_injOn (f := φ) (mod_cast hφ)]
    _ ≤ #(((A ^ m).image π).image φ * {x ∈ A ^ n | x ∈ H}) := by
      rw [Finset.card_mul_iff.2]
      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]
      rintro _ a₁ b₁ hb₁ rfl - ha₁ _ a₂ b₂ hb₂ rfl - ha₂ hab
      have hπa₁ : π a₁ = 1 := (QuotientGroup.eq_one_iff _).2 ha₁
      have hπa₂ : π a₂ = 1 := (QuotientGroup.eq_one_iff _).2 ha₂
      have hπb : π b₁ = π b₂ := by
        simpa [hπφ, Set.mem_image_of_mem π, hb₁, hb₂, hπa₁, hπa₂] using congr(π $hab)
      simp_all
    _ ≤ #(A ^ (m + n)) := by
      gcongr
      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]
      rintro a ha b hb -
      exact mul_mem_mul (hφA <| Set.mem_image_of_mem _ <| mod_cast ha) hb
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
⊢ #A ≤ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
have rw : ∑ b ∈ image (⇑π : (a : G) → G ⧸ H) A, #({a ∈ A | (π : (a : G) → G ⧸ H) a = b}) ≤
  card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
Tactic: rw [card_eq_sum_card_image π]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
⊢ ∑ b ∈ image (⇑π : (a : G) → G ⧸ H) A, #({a ∈ A | (π : (a : G) → G ⧸ H) a = b}) ≤
    card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
have refine : ∀ (a : G) (ha : a ∈ A),
  #({a_1 ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a_1 : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
    #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
Tactic: refine sum_le_card_nsmul _ _ _ <| forall_mem_image.2 fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ #(({a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)})⁻¹ *
        {a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
    #({x ∈ A⁻¹ * A | x ∈ H})
have a₁ : ({a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)})⁻¹ *
    {a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)} ⊆
  {x ∈ A⁻¹ * A | x ∈ H}
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ ({a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)})⁻¹ *
      {a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)} ⊆
    {x ∈ A⁻¹ * A | x ∈ H}
have a₁ : ∀ (x : G),
  x⁻¹ ∈ A →
    Eq (α := G ⧸ H) (((π : (a : G) → G ⧸ H) x)⁻¹ : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H) →
      ∀ y ∈ A,
        Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) y : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H) →
          x * y ∈ A⁻¹ * A ∧ x * y ∈ H
Tactic: simp only [mul_subset_iff, mem_inv', map_inv, mem_filter, and_imp]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
x : G
hx : x⁻¹ ∈ A
hxa : Eq (α := G ⧸ H) (((π : (a : G) → G ⧸ H) x)⁻¹ : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)
y : G
hy : y ∈ A
hya : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) y : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)
⊢ x * y ∈ A⁻¹ * A ∧ x * y ∈ H
have a₁ : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) (x * y) : G ⧸ H) (1 : G ⧸ H)
Tactic: refine ⟨mul_mem_mul (by simpa) hy, (QuotientGroup.eq_one_iff _).1 (?_ : π _ = _)⟩
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ #({a_1 ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a_1 : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
    #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
have A₁ : #(({a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)})⁻¹ *
      {a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
  #({x ∈ A⁻¹ * A | x ∈ H})
Tactic: calc
    #{a' ∈ A | π a' = π a}
    _ ≤ #({a' ∈ A | π a' = π a}⁻¹ * {a' ∈ A | π a' = π a}) :=
      card_le_card_mul_left ⟨a⁻¹, by simpa⟩
    _ ≤ #{x ∈ A⁻¹ * A | x ∈ H} := by
      gcongr
      simp only [mul_subset_iff, mem_inv', map_inv, mem_filter, and_imp]
      rintro x hx hxa y hy hya
      refine ⟨mul_mem_mul (by simpa) hy, (QuotientGroup.eq_one_iff _).1 (?_ : π _ = _)⟩
      simp [hya, ← hxa]
    _ = #{x ∈ A ^ 2 | x ∈ H} := by simp [hAsymm, sq]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
A₁ :
  #(({a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)})⁻¹ *
        {a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
    #({x ∈ A⁻¹ * A | x ∈ H})
⊢ #({a_1 ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a_1 : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
    #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
have A₂ : #({x ∈ A⁻¹ * A | x ∈ H}) = #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
Tactic: calc
    #{a' ∈ A | π a' = π a}
    _ ≤ #({a' ∈ A | π a' = π a}⁻¹ * {a' ∈ A | π a' = π a}) :=
      card_le_card_mul_left ⟨a⁻¹, by simpa⟩
    _ ≤ #{x ∈ A⁻¹ * A | x ∈ H} := by
      gcongr
      simp only [mul_subset_iff, mem_inv', map_inv, mem_filter, and_imp]
      rintro x hx hxa y hy hya
      refine ⟨mul_mem_mul (by simpa) hy, (QuotientGroup.eq_one_iff _).1 (?_ : π _ = _)⟩
      simp [hya, ← hxa]
    _ = #{x ∈ A ^ 2 | x ∈ H} := by simp [hAsymm, sq]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
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
hAsymm : A⁻¹ = A
set :
  #A ≤ card (α := G ⧸ H) (image (⇑(QuotientGroup.mk' H) : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
set₁ :
  let π : G →* G ⧸ H := QuotientGroup.mk' H;
  #A ≤ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
⊢ #A ≤ card (α := G ⧸ H) (image (⇑(QuotientGroup.mk' H) : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
have set₂ : let π : G →* G ⧸ H := QuotientGroup.mk' H;
∑ b ∈ image (⇑π : (a : G) → G ⧸ H) A, #({a ∈ A | (π : (a : G) → G ⧸ H) a = b}) ≤
  card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
Tactic: classical
  set π := QuotientGroup.mk' H
  rw [card_eq_sum_card_image π]
  refine sum_le_card_nsmul _ _ _ <| forall_mem_image.2 fun a ha ↦ ?_
  calc
    #{a' ∈ A | π a' = π a}
    _ ≤ #({a' ∈ A | π a' = π a}⁻¹ * {a' ∈ A | π a' = π a}) :=
      card_le_card_mul_left ⟨a⁻¹, by simpa⟩
    _ ≤ #{x ∈ A⁻¹ * A | x ∈ H} := by
      gcongr
      simp only [mul_subset_iff, mem_inv', map_inv, mem_filter, and_imp]
      rintro x hx hxa y hy hya
      refine ⟨mul_mem_mul (by simpa) hy, (QuotientGroup.eq_one_iff _).1 (?_ : π _ = _)⟩
      simp [hya, ← hxa]
    _ = #{x ∈ A ^ 2 | x ∈ H} := by simp [hAsymm, sq]