internlm/Lean-Github huggingface dataset:
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
⊢ 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]
Proof 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
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
⊢ x ∈ (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab → x = ↑1
Tactic:
intro hx
Proof 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
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 ⊆ ↑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 }
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)
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
Proof state after:
no goals
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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]
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
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
⊢ s = y⁻¹ • s
Tactic:
simp only [← inv_smul_eq_iff, inv_inv, ← (mem_mulStab hs), hy]
Proof state after:
no goals
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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]
Proof 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
Theorem: Finset.le_card_union_add_card_mulStab_union
Proof 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
Proof 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