-- 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))
a : G ⧸ H
ha : a ∈ ⇑π '' (↑A ^ m)
this : invFunOn (⇑π) (↑A ^ m) a ∈ ↑A ^ m
⊢ φ a ∈ A ^ m

Tactic:
norm_cast at 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))
a : G ⧸ H
ha : a ∈ ⇑π '' (↑A ^ m)
this : invFunOn (⇑π) (↑(A ^ m)) a ∈ A ^ m
⊢ φ a ∈ A ^ m

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 φ (image (⇑π) (A ^ m)) * filter (fun x => x ∈ H) (A ^ n)) ≤ #(A ^ (m + n))

Tactic:
gcongr

Result:
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
⊢ image φ (image (⇑π) (A ^ m)) * filter (fun x => x ∈ H) (A ^ n) ⊆ 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 : ℕ
⊢ #(image (⇑(QuotientGroup.mk' H)) (A ^ m)) * #(filter (fun x => x ∈ H) (A ^ n)) ≤ #(A ^ (m + n))

Tactic:
set π := QuotientGroup.mk' H

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
⊢ #(image (⇑π) (A ^ m)) * #(filter (fun x => x ∈ H) (A ^ n)) ≤ #(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))
a : G ⧸ H
ha : a ∈ ⇑π '' (↑A ^ m)
⊢ ∃ a ∈ ?m.5680, ?m.5681 a = ?m.5682

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))
a : G ⧸ H
ha : a ∈ ⇑π '' (↑A ^ m)
⊢ φ a ∈ A ^ m

Tactic:
have := invFunOn_mem (by simpa using 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))
a : G ⧸ H
ha : a ∈ ⇑π '' (↑A ^ m)
this : invFunOn (⇑π) (↑A ^ m) a ∈ ↑A ^ m
⊢ φ a ∈ A ^ m

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₂) ∧ a₁ = a₂

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

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
hπa₂ : π a₂ = 1
hπb : π b₁ = π b₂
⊢ φ (π 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)
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
⊢ Set.InjOn (fun p => p.1 * p.2) (↑(image φ (image (⇑π) (A ^ m))) ×ˢ ↑(filter (fun x => x ∈ H) (A ^ n)))

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]

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 x : G),
    x ∈ ↑A ^ m →
      φ (π x) = a →
        b ∈ A ^ n →
          b ∈ H →
            ∀ (a_5 b_1 x : G),
              x ∈ ↑A ^ m → φ (π x) = a_5 → b_1 ∈ A ^ n → b_1 ∈ H → a * b = a_5 * b_1 → a = a_5 ∧ b = b_1