-- Mathlib/Geometry/Group/Growth/QuotientInter.lean
@[to_additive]
lemma le_card_quotient_mul_sq_inter_subgroup (hAsymm : A⁻¹ = A) :
    #A ≤ #(A.image <| QuotientGroup.mk' H) * #{x ∈ A ^ 2 | x ∈ H}

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
hAsymm : A⁻¹ = A
⊢ #A ≤ #(image (⇑(QuotientGroup.mk' H)) A) * #(filter (fun x => x ∈ H) (A ^ 2))

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]

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ #(filter (fun x => x ∈ H) (A⁻¹ * A)) = #(filter (fun x => x ∈ H) (A ^ 2))

Tactic:
simp [hAsymm, sq]

Result:
no goals

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
x : G
hx : x⁻¹ ∈ A
hxa : (π x)⁻¹ = π a
y : G
hy : y ∈ A
hya : π y = π a
⊢ x * y ∈ A⁻¹ * A ∧ x * y ∈ H

Tactic:
refine ⟨mul_mem_mul (by simpa) hy, (QuotientGroup.eq_one_iff _).1 (?_ : π _ = _)⟩

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
x : G
hx : x⁻¹ ∈ A
hxa : (π x)⁻¹ = π a
y : G
hy : y ∈ A
hya : π y = π a
⊢ π (x * y) = 1

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ a⁻¹ ∈ (filter (fun a' => π a' = π a) A)⁻¹

Tactic:
simpa

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
hAsymm : A⁻¹ = A
⊢ #A ≤ #(image (⇑(QuotientGroup.mk' H)) A) * #(filter (fun x => x ∈ H) (A ^ 2))

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
⊢ #A ≤ #(image (⇑π) A) * #(filter (fun x => x ∈ H) (A ^ 2))

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
x : G
hx : x⁻¹ ∈ A
hxa : (π x)⁻¹ = π a
y : G
hy : y ∈ A
hya : π y = π a
⊢ π (x * y) = 1

Tactic:
simp [hya, ← hxa]

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
x : G
hx : x⁻¹ ∈ A
hxa : (π x)⁻¹ = π a
y : G
hy : y ∈ A
hya : π y = π a
⊢ x ∈ A⁻¹

Tactic:
simpa

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ #((filter (fun a' => π a' = π a) A)⁻¹ * filter (fun a' => π a' = π a) A) ≤ #(filter (fun x => x ∈ H) (A⁻¹ * A))

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ (filter (fun a' => π a' = π a) A)⁻¹ * filter (fun a' => π a' = π a) A ⊆ filter (fun x => x ∈ H) (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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ #(filter (fun a_1 => π a_1 = π a) A) ≤ #(filter (fun x => x ∈ H) (A ^ 2))

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]

Result:
no goals

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ ∀ (x : G), x⁻¹ ∈ A → (π x)⁻¹ = π a → ∀ y ∈ A, π y = π a → x * y ∈ A⁻¹ * A ∧ x * y ∈ H

Tactic:
rintro x hx hxa y hy hya

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
x : G
hx : x⁻¹ ∈ A
hxa : (π x)⁻¹ = π a
y : G
hy : y ∈ A
hya : π y = π a
⊢ x * y ∈ A⁻¹ * A ∧ x * y ∈ H

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ (filter (fun a' => π a' = π a) A)⁻¹ * filter (fun a' => π a' = π a) A ⊆ filter (fun x => x ∈ H) (A⁻¹ * A)

Tactic:
simp only [mul_subset_iff, mem_inv', map_inv, mem_filter, and_imp]

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ ∀ (x : G), x⁻¹ ∈ A → (π x)⁻¹ = π a → ∀ y ∈ A, π y = π a → x * y ∈ A⁻¹ * A ∧ x * y ∈ H

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
⊢ #A ≤ #(image (⇑π) A) * #(filter (fun x => x ∈ H) (A ^ 2))

Tactic:
rw [card_eq_sum_card_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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
⊢ ∑ b ∈ image (⇑π) A, #(filter (fun a => π a = b) A) ≤ #(image (⇑π) A) * #(filter (fun x => x ∈ H) (A ^ 2))

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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
⊢ ∑ b ∈ image (⇑π) A, #(filter (fun a => π a = b) A) ≤ #(image (⇑π) A) * #(filter (fun x => x ∈ H) (A ^ 2))

Tactic:
refine sum_le_card_nsmul _ _ _ <| forall_mem_image.2 fun a 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
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ #(filter (fun a_1 => π a_1 = π a) A) ≤ #(filter (fun x => x ∈ H) (A ^ 2))