Theorem: Finset.le_card_union_add_card_mulStab_union
Proof state before:
case a.mp.intro.intro.intro.intro.intro.intro
α : 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
this✝ :
  ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
    s.Nonempty →
      t.Nonempty →
        let Hs := s.mulStab;
        Hs = s.mulStab →
          let Ht := t.mulStab;
          Ht = t.mulStab →
            let H := Hs * Ht;
            H = Hs * Ht →
              Hs.Nonempty →
                Ht.Nonempty →
                  H.Nonempty →
                    Hs ∩ Ht = 1 → min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
h1 : ¬Hs ∩ Ht = 1
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
x : α ⧸ N
y : α
hy : y ∈ s.mulStab
z : α
hz : z ∈ t.mulStab
w : α
hzx : z⁻¹ * w ∈ N
hyx : y⁻¹ * w ∈ N
hwx : ⟦w⟧ = x
this : ⟦w⟧ = ↑w
⊢ w⁻¹ * 1 ∈ N

case a.mp
α : 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
this :
  ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
    s.Nonempty →
      t.Nonempty →
        let Hs := s.mulStab;
        Hs = s.mulStab →
          let Ht := t.mulStab;
          Ht = t.mulStab →
            let H := Hs * Ht;
            H = Hs * Ht →
              Hs.Nonempty →
                Ht.Nonempty →
                  H.Nonempty →
                    Hs ∩ Ht = 1 → min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
h1 : ¬Hs ∩ Ht = 1
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
x : α ⧸ N
hx : x ∈ image QuotientGroup.mk s.mulStab ∩ (image QuotientGroup.mk t).mulStab
⊢ ↑N ⊆ ↑t.mulStab

case a.mp
α : 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
this :
  ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
    s.Nonempty →
      t.Nonempty →
        let Hs := s.mulStab;
        Hs = s.mulStab →
          let Ht := t.mulStab;
          Ht = t.mulStab →
            let H := Hs * Ht;
            H = Hs * Ht →
              Hs.Nonempty →
                Ht.Nonempty →
                  H.Nonempty →
                    Hs ∩ Ht = 1 → min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
h1 : ¬Hs ∩ Ht = 1
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
x : α ⧸ N
hx : x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab
⊢ ↑N ⊆ ↑s.mulStab
Tactic:
simp only [mul_one, inv_mem_iff, Subgroup.mem_inf, mem_stabilizer_iff, N] at hyx hzx ⊢
Proof state after:
case a.mp.intro.intro.intro.intro.intro.intro
α : 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
this✝ :
  ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
    s.Nonempty →
      t.Nonempty →
        let Hs := s.mulStab;
        Hs = s.mulStab →
          let Ht := t.mulStab;
          Ht = t.mulStab →
            let H := Hs * Ht;
            H = Hs * Ht →
              Hs.Nonempty →
                Ht.Nonempty →
                  H.Nonempty →
                    Hs ∩ Ht = 1 → min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
h1 : ¬Hs ∩ Ht = 1
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
x : α ⧸ N
y : α
hy : y ∈ s.mulStab
z : α
hz : z ∈ t.mulStab
w : α
hwx : ⟦w⟧ = x
this : ⟦w⟧ = ↑w
hyx : (y⁻¹ * w) • s = s ∧ (y⁻¹ * w) • t = t
hzx : (z⁻¹ * w) • s = s ∧ (z⁻¹ * w) • t = t
⊢ w • s = s ∧ w • t = t

case a.mp
α : 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
this :
  ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
    s.Nonempty →
      t.Nonempty →
        let Hs := s.mulStab;
        Hs = s.mulStab →
          let Ht := t.mulStab;
          Ht = t.mulStab →
            let H := Hs * Ht;
            H = Hs * Ht →
              Hs.Nonempty →
                Ht.Nonempty →
                  H.Nonempty →
                    Hs ∩ Ht = 1 → min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
h1 : ¬Hs ∩ Ht = 1
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
x : α ⧸ N
hx : x ∈ image QuotientGroup.mk s.mulStab ∩ (image QuotientGroup.mk t).mulStab
⊢ ↑N ⊆ ↑t.mulStab

case a.mp
α : 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
this :
  ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
    s.Nonempty →
      t.Nonempty →
        let Hs := s.mulStab;
        Hs = s.mulStab →
          let Ht := t.mulStab;
          Ht = t.mulStab →
            let H := Hs * Ht;
            H = Hs * Ht →
              Hs.Nonempty →
                Ht.Nonempty →
                  H.Nonempty →
                    Hs ∩ Ht = 1 → min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
h1 : ¬Hs ∩ Ht = 1
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
x : α ⧸ N
hx : x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab
⊢ ↑N ⊆ ↑s.mulStab