-- Mathlib/Geometry/Group/Growth/QuotientInter.lean
@[to_additive]
lemma card_pow_quotient_mul_pow_inter_subgroup_le :
    #((A ^ m).image <| QuotientGroup.mk' H) * #{x ∈ A ^ n | x ∈ H} ≤ #(A ^ (m + n))

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
⊢ #(image (⇑π) (A ^ m)) * #(filter (fun x => x ∈ H) (A ^ n)) ≤ #(A ^ (m + n))

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

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → φ a ∈ A ^ m
⊢ #(image (⇑π) (A ^ m)) * #(filter (fun x => x ∈ H) (A ^ n)) ≤ #(A ^ (m + n))

Proof state:
case a
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → π (φ a) = a
a : G
ha : a ∈ A ^ m
b : G
hb : b ∈ A ^ n
⊢ φ (π a) * b ∈ A ^ m * A ^ n

Tactic:
exact mul_mem_mul (hφA <| Set.mem_image_of_mem _ <| mod_cast ha) hb

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → π (φ a) = a
⊢ #(image (⇑π) (A ^ m)) * #(filter (fun x => x ∈ H) (A ^ n)) ≤ #(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)
    aesop
  _ ≤ #(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

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → π (φ a) = a
⊢ #(image (⇑π) (A ^ m)) * #(filter (fun x => x ∈ H) (A ^ n)) =
    #(image φ (image (⇑π) (A ^ m))) * #(filter (fun x => x ∈ H) (A ^ n))

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

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → π (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ ↑A ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ ↑A ^ m
ha₂ : a₂ ∈ H
hab : φ (π b₁) * a₁ = φ (π b₂) * a₂
hπa₁ : π a₁ = 1
hπa₂ : π a₂ = 1
hπb : π b₁ = π b₂
⊢ φ (π b₁) = φ (π b₂) ∧ a₁ = a₂

Tactic:
aesop

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → φ a ∈ A ^ m
a : G ⧸ H
ha : a ∈ ⇑π '' (↑A ^ m)
⊢ ∃ a_1 ∈ ↑A ^ m, π a_1 = a

Tactic:
simpa using ha

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → π (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ ↑A ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ ↑A ^ m
ha₂ : a₂ ∈ H
hab : φ (π b₁) * a₁ = φ (π b₂) * a₂
hπa₁ : π a₁ = 1
hπa₂ : π a₂ = 1
⊢ π b₁ = π b₂

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

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → π (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ ↑A ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ ↑A ^ m
ha₂ : a₂ ∈ H
hab : φ (π b₁) * a₁ = φ (π b₂) * a₂
⊢ φ (π b₁) = φ (π b₂) ∧ a₁ = a₂

Tactic:
have hπa₁ : π a₁ = 1 := (QuotientGroup.eq_one_iff _).2 ha₁

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → π (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ ↑A ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ ↑A ^ m
ha₂ : a₂ ∈ H
hab : φ (π b₁) * a₁ = φ (π b₂) * a₂
hπa₁ : π a₁ = 1
⊢ φ (π b₁) = φ (π b₂) ∧ a₁ = a₂

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
⊢ #(image (⇑π) (A ^ m)) * #(filter (fun x => x ∈ H) (A ^ n)) ≤ #(A ^ (m + n))

Tactic:
have hφ : Set.InjOn φ (π '' (A ^ m)) := invFunOn_injOn_image ..

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x => x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' (↑A ^ m))
⊢ #(image (⇑π) (A ^ m)) * #(filter (fun x => x ∈ H) (A ^ n)) ≤ #(A ^ (m + n))