internlm/Lean-Github huggingface dataset:
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof state after:
no goals
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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']
Proof state after:
no goals
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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']
Proof state after:
no goals
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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 (↑))
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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 }
Proof state after:
no goals
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
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
Proof state after:
no goals
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
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
Proof 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