Theorem: Finset.le_card_union_add_card_mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ min (s.card + Hs.card) (t.card + Ht.card) =
    min (Nat.card ↥N * (image QuotientGroup.mk s).card + Nat.card ↥N * (image QuotientGroup.mk Hs).card)
      (Nat.card ↥N * (image QuotientGroup.mk t).card + Nat.card ↥N * (image QuotientGroup.mk Ht).card)
Tactic:
rw [← subgroup_mul_card_eq_mul_of_mul_stab_subset N s,
← subgroup_mul_card_eq_mul_of_mul_stab_subset N t,
← subgroup_mul_card_eq_mul_of_mul_stab_subset N Hs,
← subgroup_mul_card_eq_mul_of_mul_stab_subset N Ht]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ ↑N ⊆ ↑Ht.mulStab

α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ ↑N ⊆ ↑Hs.mulStab

α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ ↑N ⊆ ↑t.mulStab

α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ ↑N ⊆ ↑s.mulStab