internlm/Lean-Github huggingface dataset:
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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]
Proof state after:
no goals
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof state after:
no goals
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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 }) [*]
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
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
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
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]
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
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]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ ↑N ⊆ ↑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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ ↑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 [*]
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
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 [*]
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
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 }
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
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]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ ↑(Hs ∩ Ht) ⊆ ↑(s ∪ t).mulStab
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ ↑(Hs ∩ Ht) ⊆ ↑(s ∪ t).mulStab
Tactic:
norm_cast
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ Hs ∩ Ht ⊆ (s ∪ t).mulStab
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs✝ : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt✝ : Ht = t.mulStab
H : Finset α := Hs * Ht
hH✝ : H = Hs * Ht
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (image QuotientGroup.mk t).mulStab.card) ≤
    (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s ∪ image QuotientGroup.mk t).mulStab.card
⊢ Hs ∩ Ht ⊆ (s ∪ t).mulStab
Tactic:
exact inter_mulStab_subset_mulStab_union
Proof state after:
no goals
Theorem: Finset.le_card_sup_add_card_mulStab_sup
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
s : Finset ι
f : ι → Finset α
hs : s.Nonempty
⊢ (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
Tactic:
induction' s using Finset.cons_induction with i s hi ih
Proof state after:
case empty
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ι : Type u_2
f : ι → Finset α
hs : ∅.Nonempty
⊢ (∅.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (∅.sup f).card + (∅.sup f).mulStab.card

case cons
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs : (cons i s hi).Nonempty
⊢ ((cons i s hi).inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i s hi).sup f).card + ((cons i s hi).sup f).mulStab.card
Theorem: Finset.le_card_sup_add_card_mulStab_sup
Proof state before:
case cons
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs : (cons i s hi).Nonempty
⊢ ((cons i s hi).inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i s hi).sup f).card + ((cons i s hi).sup f).mulStab.card
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
Proof state after:
case cons.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
hi : i ∉ ∅
ih : ∀ (hs : ∅.Nonempty), (∅.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (∅.sup f).card + (∅.sup f).mulStab.card
hs : (cons i ∅ hi).Nonempty
⊢ ((cons i ∅ hi).inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i ∅ hi).sup f).card + ((cons i ∅ hi).sup f).mulStab.card

case cons.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs✝ : (cons i s hi).Nonempty
hs : s.Nonempty
⊢ ((cons i s hi).inf' hs✝ fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i s hi).sup f).card + ((cons i s hi).sup f).mulStab.card
Theorem: Finset.le_card_sup_add_card_mulStab_sup
Proof state before:
case cons.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs✝ : (cons i s hi).Nonempty
hs : s.Nonempty
⊢ ((cons i s hi).inf' hs✝ fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i s hi).sup f).card + ((cons i s hi).sup f).mulStab.card
Tactic:
simp only [hs, inf'_cons, sup_cons, sup_eq_union]
Proof state after:
case cons.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs✝ : (cons i s hi).Nonempty
hs : s.Nonempty
⊢ (((f i).card + (f i).mulStab.card) ⊓ s.inf' ⋯ fun i => (f i).card + (f i).mulStab.card) ≤
    (f i ∪ s.sup f).card + (f i ∪ s.sup f).mulStab.card
Theorem: Finset.le_card_sup_add_card_mulStab_sup
Proof state before:
case cons.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs✝ : (cons i s hi).Nonempty
hs : s.Nonempty
⊢ (((f i).card + (f i).mulStab.card) ⊓ s.inf' ⋯ fun i => (f i).card + (f i).mulStab.card) ≤
    (f i ∪ s.sup f).card + (f i ∪ s.sup f).mulStab.card
Tactic:
exact (inf_le_inf_left _ $ ih hs).trans le_card_union_add_card_mulStab_union
Proof state after:
no goals
Theorem: Finset.le_card_sup_add_card_mulStab_sup
Proof state before:
case empty
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ι : Type u_2
f : ι → Finset α
hs : ∅.Nonempty
⊢ (∅.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (∅.sup f).card + (∅.sup f).mulStab.card
Tactic:
cases not_nonempty_empty hs
Proof state after:
no goals
Theorem: Finset.le_card_sup_add_card_mulStab_sup
Proof state before:
case cons.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
hi : i ∉ ∅
ih : ∀ (hs : ∅.Nonempty), (∅.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (∅.sup f).card + (∅.sup f).mulStab.card
hs : (cons i ∅ hi).Nonempty
⊢ ((cons i ∅ hi).inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i ∅ hi).sup f).card + ((cons i ∅ hi).sup f).mulStab.card
Tactic:
simp
Proof state after:
no goals