Theorem: ex_1_2_4 (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ x_1 ∈ A ×ˢ B, ex124' x_1 = x} ≤ #↑A * #↑B
Tactic:
simp only [ex124', Set.mem_prod, exists_prop, Prod.exists]
State after:
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} ≤ #↑A * #↑B

State before:
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} ≤ #↑A * #↑B
Tactic:
calc
  (#{x | ∃ a b : G, (a ∈ A ∧ b ∈ B) ∧ a * b = x}) =
      (#(⋃ (a ∈ A) (b ∈ B), ({(a : G) * (b : G)} : Set G))) := ?_
  _ = (#(⋃ (a : A) (b : B), ({(a : G) * (b : G)} : Set G))) := ?_
  _ ≤ Cardinal.sum fun a : A => Cardinal.sum fun b : B => #({(a : G) * (b : G)} : Set G) := ?_
  _ = (#A) * (#B) := ?_
State after:
case calc_1
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} = #↑(⋃ a ∈ A, ⋃ b ∈ B, {a * b})

case calc_2
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑(⋃ a ∈ A, ⋃ b ∈ B, {a * b}) = #↑(⋃ a, ⋃ b, {↑a * ↑b})

case calc_3
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑(⋃ a, ⋃ b, {↑a * ↑b}) ≤ Cardinal.sum fun a => Cardinal.sum fun b => #↑{↑a * ↑b}

case calc_4
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ (Cardinal.sum fun a => Cardinal.sum fun b => #↑{↑a * ↑b}) = #↑A * #↑B

State before:
case calc_1
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} = #↑(⋃ a ∈ A, ⋃ b ∈ B, {a * b})
Tactic:
congr 2 with x
State after:
case calc_1.e_a.e_s.h
G : Type u_1
inst✝ : Group G
A B : Set G
x : G
⊢ x ∈ {x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} ↔ x ∈ ⋃ a ∈ A, ⋃ b ∈ B, {a * b}

State before:
case calc_1.e_a.e_s.h
G : Type u_1
inst✝ : Group G
A B : Set G
x : G
⊢ x ∈ {x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} ↔ x ∈ ⋃ a ∈ A, ⋃ b ∈ B, {a * b}
Tactic:
simp [Set.setOf_exists, Set.setOf_and, and_assoc]
State after:
no goals

State before:
case calc_2
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑(⋃ a ∈ A, ⋃ b ∈ B, {a * b}) = #↑(⋃ a, ⋃ b, {↑a * ↑b})
Tactic:
simp only [Set.iUnion_coe_set]
State after:
no goals

State before:
case calc_3
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑(⋃ a, ⋃ b, {↑a * ↑b}) ≤ Cardinal.sum fun a => Cardinal.sum fun b => #↑{↑a * ↑b}
Tactic:
exact
  Cardinal.mk_iUnion_le_sum_mk.trans
    (Cardinal.sum_le_sum _ _ fun a => Cardinal.mk_iUnion_le_sum_mk)
State after:
no goals

State before:
case calc_4
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ (Cardinal.sum fun a => Cardinal.sum fun b => #↑{↑a * ↑b}) = #↑A * #↑B
Tactic:
simp_rw [Cardinal.mk_singleton, Cardinal.sum_const', mul_one]
State after:
no goals