Theorem: Finset.le_card_union_add_card_mulStab_union (LeanCamCombi/Kneser/KneserRuzsa.lean)

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
⊢ min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
State after:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
⊢ min (∅.card + ∅.mulStab.card) (t.card + t.mulStab.card) ≤ (∅ ∪ t).card + (∅ ∪ t).mulStab.card

case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
⊢ min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
⊢ min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
State after:
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ min (s.card + s.mulStab.card) (∅.card + ∅.mulStab.card) ≤ (s ∪ ∅).card + (s ∪ ∅).mulStab.card

case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
set Hs := s.mulStab with hHs
State after:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs : Hs = s.mulStab
⊢ min (s.card + Hs.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs : Hs = s.mulStab
⊢ min (s.card + Hs.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
set Ht := t.mulStab with hHt
State after:
case inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
set H := Hs * Ht with hH
State after:
case inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
have hHs : Hs.Nonempty := hs.mulStab
State after:
case inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
have hHt : Ht.Nonempty := ht.mulStab
State after:
case inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
have hH : H.Nonempty := hHs.mul hHt
State after:
case inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
wlog h1: Hs ∩ Ht = 1
State after:
case inr.inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

α✝ : Type u_1
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
s✝ t✝ : Finset α✝
α : 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
h1 : Hs ∩ Ht = 1
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
α✝ : Type u_1
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
s✝ t✝ : Finset α✝
α : 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
h1 : Hs ∩ Ht = 1
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
sorry
State after:
no goals

State before:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
⊢ min (∅.card + ∅.mulStab.card) (t.card + t.mulStab.card) ≤ (∅ ∪ t).card + (∅ ∪ t).mulStab.card
Tactic:
simp [-zero_le']
State after:
no goals

State before:
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ min (s.card + s.mulStab.card) (∅.card + ∅.mulStab.card) ≤ (s ∪ ∅).card + (s ∪ ∅).mulStab.card
Tactic:
simp [-zero_le']
State after:
no goals

State before:
case inr.inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
set N := stabilizer α s ⊓ stabilizer α t with hN
State after:
case inr.inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr.inr
α : 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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
have hNmulstab : (N : Set α) = ↑(Hs ∩ Ht) := by aesop
State after:
case inr.inr.inr
α : 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)
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr.inr
α : 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
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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
specialize this (α := α ⧸ N) (s := s.image (↑)) (t := t.image (↑))
State after:
case inr.inr.inr
α : 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 :
  (image QuotientGroup.mk s).Nonempty →
    (image QuotientGroup.mk t).Nonempty →
      let Hs := (image QuotientGroup.mk s).mulStab;
      Hs = (image QuotientGroup.mk s).mulStab →
        let Ht := (image QuotientGroup.mk t).mulStab;
        Ht = (image QuotientGroup.mk t).mulStab →
          let H := Hs * Ht;
          H = Hs * Ht →
            Hs.Nonempty →
              Ht.Nonempty →
                H.Nonempty →
                  Hs ∩ Ht = 1 →
                    min ((image QuotientGroup.mk s).card + Hs.card) ((image QuotientGroup.mk t).card + Ht.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) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr.inr
α : 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 :
  (image QuotientGroup.mk s).Nonempty →
    (image QuotientGroup.mk t).Nonempty →
      let Hs := (image QuotientGroup.mk s).mulStab;
      Hs = (image QuotientGroup.mk s).mulStab →
        let Ht := (image QuotientGroup.mk t).mulStab;
        Ht = (image QuotientGroup.mk t).mulStab →
          let H := Hs * Ht;
          H = Hs * Ht →
            Hs.Nonempty →
              Ht.Nonempty →
                H.Nonempty →
                  Hs ∩ Ht = 1 →
                    min ((image QuotientGroup.mk s).card + Hs.card) ((image QuotientGroup.mk t).card + Ht.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) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
simp only [image_nonempty, mulStab_nonempty, mul_nonempty, and_imp,
  forall_true_left, hs, ht, h1] at this
State after:
case inr.inr.inr
α : 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) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

State before:
case inr.inr.inr
α : 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) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
calc
min (card s + card Hs) (card t + card Ht) =
  min (Nat.card N * card (s.image (QuotientGroup.mk (s := N))) +
  Nat.card N * card (Hs.image (QuotientGroup.mk (s := N))))
  (Nat.card N * card (t.image (QuotientGroup.mk (s := N))) +
  Nat.card N * card (Ht.image (QuotientGroup.mk (s := N)))) := by
    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]
    all_goals { aesop }
_ = Nat.card N * min (card (s.image (QuotientGroup.mk (s := N))) +
  card (Hs.image (QuotientGroup.mk (s := N)))) (card (t.image (QuotientGroup.mk (s := N))) +
  card (Ht.image (QuotientGroup.mk (s := N)))) := by
    rw [← mul_add, ← mul_add, Nat.mul_min_mul_left]
_ = Nat.card N * min (card (image (QuotientGroup.mk (s := N)) s) +
  card (mulStab (image (QuotientGroup.mk (s := N)) s)))
  (card (image (QuotientGroup.mk (s := N)) t) +
  card (mulStab (image (QuotientGroup.mk (s := N)) t))) := by
    rw [mulStab_quotient_commute_subgroup N t, mulStab_quotient_commute_subgroup N s]
    all_goals simp [*]
_ ≤ Nat.card N * (card (image (QuotientGroup.mk (s := N)) s ∪
  image (QuotientGroup.mk (s := N)) t) +
  card (mulStab (image (QuotientGroup.mk (s := N)) s ∪
  image (QuotientGroup.mk (s := N)) t))) := Nat.mul_le_mul_left _ this
_ ≤ card (s ∪ t) + card (s ∪ t).mulStab := by
  rw [mul_add, ← image_union, subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t),
      ← mulStab_quotient_commute_subgroup N (s ∪ t),
      subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t).mulStab]
  all_goals
  { simp only [hNmulstab, mulStab_idem]; norm_cast; exact inter_mulStab_subset_mulStab_union }
State after:
no goals

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
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
⊢ ↑N = ↑(Hs ∩ Ht)
Tactic:
aesop
State after:
no goals

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
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)
⊢ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
Tactic:
ext x
State after:
case a
α : 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
⊢ x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab ↔ x ∈ 1

State before:
case a
α : 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
⊢ x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab ↔ x ∈ 1
Tactic:
constructor
State after:
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
⊢ x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab → x ∈ 1

case a.mpr
α : 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
⊢ x ∈ 1 → x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab

State before:
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
⊢ x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab → x ∈ 1
Tactic:
simp only [image_nonempty, mem_one, and_imp, ← QuotientGroup.mk_one]
State after:
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
⊢ x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab → x = ↑1

State before:
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
⊢ x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab → x = ↑1
Tactic:
intro hx
State after:
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
⊢ x = ↑1

State before:
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
⊢ x = ↑1
Tactic:
rw [← mulStab_quotient_commute_subgroup N s, ← mulStab_quotient_commute_subgroup N t] at hx
State after:
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
⊢ x = ↑1

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

State before:
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
⊢ x = ↑1

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 [mem_inter, mem_image] at hx
State after:
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 : (∃ a ∈ s.mulStab, ↑a = x) ∧ ∃ a ∈ t.mulStab, ↑a = x
⊢ x = ↑1

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

State before:
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 : (∃ a ∈ s.mulStab, ↑a = x) ∧ ∃ a ∈ t.mulStab, ↑a = x
⊢ x = ↑1

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:
obtain ⟨⟨y, hy, hyx⟩, ⟨z, hz, hzx⟩⟩ := hx
State after:
case a.mp.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
hyx : ↑y = x
z : α
hz : z ∈ t.mulStab
hzx : ↑z = x
⊢ x = ↑1

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

State before:
case a.mp.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
hyx : ↑y = x
z : α
hz : z ∈ t.mulStab
hzx : ↑z = x
⊢ x = ↑1

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:
obtain ⟨w, hwx⟩ := Quotient.exists_rep x
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
hyx : ↑y = x
z : α
hz : z ∈ t.mulStab
hzx : ↑z = x
w : α
hwx : ⟦w⟧ = x
⊢ x = ↑1

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

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
hyx : ↑y = x
z : α
hz : z ∈ t.mulStab
hzx : ↑z = x
w : α
hwx : ⟦w⟧ = x
⊢ x = ↑1

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:
have : ⟦w⟧ = QuotientGroup.mk (s := N) w := by exact rfl
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
hyx : ↑y = x
z : α
hz : z ∈ t.mulStab
hzx : ↑z = x
w : α
hwx : ⟦w⟧ = x
this : ⟦w⟧ = ↑w
⊢ x = ↑1

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

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
hyx : ↑y = x
z : α
hz : z ∈ t.mulStab
hzx : ↑z = x
w : α
hwx : ⟦w⟧ = x
this : ⟦w⟧ = ↑w
⊢ x = ↑1

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:
rw [← hwx, this, QuotientGroup.eq] at hyx hzx ⊢
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 : α
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

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 ⊢
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

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 : α
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
Tactic:
constructor
State after:
case a.mp.intro.intro.intro.intro.intro.intro.left
α : 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

case a.mp.intro.intro.intro.intro.intro.intro.right
α : 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 • 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

State before:
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:
all_goals { aesop }
State after:
no goals

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
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
hyx : ↑y = x
z : α
hz : z ∈ t.mulStab
hzx : ↑z = x
w : α
hwx : ⟦w⟧ = x
⊢ ⟦w⟧ = ↑w
Tactic:
exact rfl
State after:
no goals

State before:
case a.mp.intro.intro.intro.intro.intro.intro.left
α : 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
Tactic:
convert hyx.1 using 1
State after:
case h.e'_2
α : 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 = (y⁻¹ * w) • s

State before:
case h.e'_2
α : 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 = (y⁻¹ * w) • s
Tactic:
rw [mul_comm, mul_smul]
State after:
case h.e'_2
α : 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 = w • y⁻¹ • s

State before:
case h.e'_2
α : 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 = w • y⁻¹ • s
Tactic:
congr
State after:
case h.e'_2.e_a
α : 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
⊢ s = y⁻¹ • s

State before:
case h.e'_2.e_a
α : 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
⊢ s = y⁻¹ • s
Tactic:
simp only [← inv_smul_eq_iff, inv_inv, ← (mem_mulStab hs), hy]
State after:
no goals

State before:
case a.mp.intro.intro.intro.intro.intro.intro.right
α : 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 • t = t
Tactic:
convert hzx.2 using 1
State after:
case h.e'_2
α : 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 • t = (z⁻¹ * w) • t

State before:
case h.e'_2
α : 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 • t = (z⁻¹ * w) • t
Tactic:
rw [mul_comm, mul_smul]
State after:
case h.e'_2
α : 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 • t = w • z⁻¹ • t

State before:
case h.e'_2
α : 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 • t = w • z⁻¹ • t
Tactic:
congr
State after:
case h.e'_2.e_a
α : 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
⊢ t = z⁻¹ • t

State before:
case h.e'_2.e_a
α : 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
⊢ t = z⁻¹ • t
Tactic:
simp only [← inv_smul_eq_iff, inv_inv, ← (mem_mulStab ht), hz]
State after:
no goals

State before:
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:
aesop
State after:
no goals

State before:
case a.mpr
α : 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
⊢ x ∈ 1 → x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab
Tactic:
simp (config := { contextual := true }) [*]
State after:
no goals

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]
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

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
⊢ ↑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
Tactic:
all_goals { aesop }
State after:
no goals

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
⊢ ↑N ⊆ ↑s.mulStab
Tactic:
aesop
State after:
no goals

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 (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) =
    Nat.card ↥N *
      min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk Hs).card)
        ((image QuotientGroup.mk t).card + (image QuotientGroup.mk Ht).card)
Tactic:
rw [← mul_add, ← mul_add, Nat.mul_min_mul_left]
State after:
no goals

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
⊢ Nat.card ↥N *
      min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk Hs).card)
        ((image QuotientGroup.mk t).card + (image QuotientGroup.mk Ht).card) =
    Nat.card ↥N *
      min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
        ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card)
Tactic:
rw [mulStab_quotient_commute_subgroup N t, mulStab_quotient_commute_subgroup N s]
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 ⊆ ↑s.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

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
⊢ ↑N ⊆ ↑s.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
Tactic:
all_goals simp [*]
State after:
no goals

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
⊢ ↑N ⊆ ↑t.mulStab
Tactic:
simp [*]
State after:
no goals

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
⊢ Nat.card ↥N *
      ((image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
        (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card) ≤
    (s ∪ t).card + (s ∪ t).mulStab.card
Tactic:
rw [mul_add, ← image_union, subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t),
    ← mulStab_quotient_commute_subgroup N (s ∪ t),
    subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t).mulStab]
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 ⊆ ↑(s ∪ t).mulStab.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 ∪ 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 ∪ t).mulStab

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
⊢ ↑N ⊆ ↑(s ∪ t).mulStab.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 ∪ 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 ∪ t).mulStab
Tactic:
all_goals
{ simp only [hNmulstab, mulStab_idem]; norm_cast; exact inter_mulStab_subset_mulStab_union }
State after:
no goals

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
⊢ ↑N ⊆ ↑(s ∪ t).mulStab
Tactic:
simp only [hNmulstab, mulStab_idem]
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
⊢ ↑(Hs ∩ Ht) ⊆ ↑(s ∪ t).mulStab

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
⊢ ↑(Hs ∩ Ht) ⊆ ↑(s ∪ t).mulStab
Tactic:
norm_cast
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
⊢ Hs ∩ Ht ⊆ (s ∪ t).mulStab

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
⊢ Hs ∩ Ht ⊆ (s ∪ t).mulStab
Tactic:
exact inter_mulStab_subset_mulStab_union
State after:
no goals