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

Tactic:
rw [Finset.card_mul_iff.2]

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
⊢ Set.InjOn (fun p => p.1 * p.2) (↑(image φ (image (⇑π) (A ^ m))) ×ˢ ↑(filter (fun x => x ∈ H) (A ^ 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
⊢ #(image (⇑π) (A ^ m)) * #(filter (fun x => x ∈ H) (A ^ n)) ≤ #(A ^ (m + n))

Tactic:
let φ := invFunOn π (A ^ m)

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)
⊢ #(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)
this : invFunOn (⇑π) (↑(A ^ m)) a ∈ A ^ m
⊢ φ a ∈ A ^ m

Tactic:
simpa using this

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
⊢ φ (π 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
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)
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

Tactic:
rintro _ a₁ b₁ hb₁ rfl - ha₁ _ a₂ b₂ hb₂ rfl - ha₂ 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₂
⊢ φ (π b₁) = φ (π b₂) ∧ a₁ = a₂

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 ∈ A ^ m, ∀ y ∈ A ^ n, y ∈ H → φ (π a) * y ∈ A ^ m * A ^ n

Tactic:
rintro a ha b hb -

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
a : G
ha : a ∈ A ^ m
b : G
hb : b ∈ A ^ n
⊢ φ (π a) * b ∈ A ^ m * A ^ 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
⊢ image φ (image (⇑π) (A ^ m)) * filter (fun x => x ∈ H) (A ^ n) ⊆ 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]

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
⊢ ∀ a ∈ A ^ m, ∀ y ∈ A ^ n, y ∈ H → φ (π a) * y ∈ A ^ m * A ^ 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))
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' (↑A ^ m) → φ a ∈ A ^ m
⊢ #(image (⇑π) (A ^ m)) * #(filter (fun x => x ∈ H) (A ^ n)) ≤ #(A ^ (m + n))

Tactic:
have hπφ {a} (ha : a ∈ π '' (A ^ m)) : π (φ a) = a := invFunOn_eq (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))
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))