internlm/Lean-Github huggingface dataset:
Theorem: Finset.mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
⊢ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab = (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
obtain rfl | hCne := C.eq_empty_or_nonempty
Proof state after:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' : Finset α
a b : α
hs₁ : (s ∩ a • ∅.mulStab).Nonempty
ht₁ : (t ∩ b • ∅.mulStab).Nonempty
hab : ¬(a * b) • ∅.mulStab ⊆ s * t
hC : Disjoint ∅ (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab))
⊢ (∅ ∪ s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab = (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab

case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
⊢ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab = (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Theorem: Finset.mulStab_union
Proof state before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
⊢ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab = (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
refine'
  ((subset_inter (mulStab_mul_ssubset_mulStab hs₁ ht₁ hab).subset Subset.rfl).trans
        inter_mulStab_subset_mulStab_union).antisymm'
    fun x hx => _
Proof state after:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x ∈ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Theorem: Finset.mulStab_union
Proof state before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x ∈ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
replace hx := (mem_mulStab $ (hs₁.mul ht₁).mono subset_union_right).mp hx
Proof state after:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Theorem: Finset.mulStab_union
Proof state before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [smul_finset_union] at hx
Proof state after:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Theorem: Finset.mulStab_union
Proof state before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
suffices hxC : x ∈ C.mulStab by
  rw [(mem_mulStab hCne).mp hxC] at hx
  rw [mem_mulStab_iff_subset_smul_finset (hs₁.mul ht₁)]
  exact hC.symm.left_le_of_le_sup_left (le_sup_right.trans hx.ge)
Proof state after:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ C.mulStab
Theorem: Finset.mulStab_union
Proof state before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ C.mulStab
Tactic:
rw [mem_mulStab_iff_smul_finset_subset hCne]
Proof state after:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x • C ⊆ C
Theorem: Finset.mulStab_union
Proof state before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x • C ⊆ C
Tactic:
obtain h | h := disjoint_or_nonempty_inter (x • C) (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
Proof state after:
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : Disjoint (x • C) (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
⊢ x • C ⊆ C

case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Theorem: Finset.mulStab_union
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Tactic:
have hUn :
  ((C.biUnion fun y => x • y • C.mulStab) ∩
      (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty := by
  have : (x • C.biUnion fun y => y • C.mulStab) = C.biUnion fun y => x • y • C.mulStab :=
    biUnion_image
  simpa [← this]
Proof state after:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hUn : ((C.biUnion fun y => x • y • C.mulStab) ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Theorem: Finset.mulStab_union
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hUn : ((C.biUnion fun y => x • y • C.mulStab) ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Tactic:
simp_rw [biUnion_inter, biUnion_nonempty, ← smul_assoc, smul_eq_mul] at hUn
Proof state after:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hUn : ∃ x_1 ∈ C, ((x * x_1) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Theorem: Finset.mulStab_union
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hUn : ∃ x_1 ∈ C, ((x * x_1) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Tactic:
obtain ⟨y, hy, hyne⟩ := hUn
Proof state after:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Theorem: Finset.mulStab_union
Proof state before:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Tactic:
have hxyCsubC : (x * y) • C.mulStab ⊆ x • C := by
  rw [← smul_eq_mul, smul_assoc, smul_finset_subset_smul_finset_iff]
  exact smul_finset_mulStab_subset hy
Proof state after:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
⊢ x • C ⊆ C
Theorem: Finset.mulStab_union
Proof state before:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
⊢ x • C ⊆ C
Tactic:
have hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) :=
  hxyC.left_le_of_le_sup_left (hxyCsubC.trans $ subset_union_left.trans hx.subset')
Proof state after:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x • C ⊆ C
Theorem: Finset.mulStab_union
Proof state before:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x • C ⊆ C
Tactic:
suffices s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab by
  have := (card_le_card hxysub).not_lt ((card_lt_card this).trans_eq ?_)
  cases this
  simp_rw [card_smul_finset]
Proof state after:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
Theorem: Finset.mulStab_union
Proof state before:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
Tactic:
apply ssubset_of_subset_not_subset
Proof state after:
case inr.inr.intro.intro.h₁
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab

case inr.inr.intro.intro.h₂
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ ¬(a * b) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
Theorem: Finset.mulStab_union
Proof state before:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' : Finset α
a b : α
hs₁ : (s ∩ a • ∅.mulStab).Nonempty
ht₁ : (t ∩ b • ∅.mulStab).Nonempty
hab : ¬(a * b) • ∅.mulStab ⊆ s * t
hC : Disjoint ∅ (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab))
⊢ (∅ ∪ s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab = (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab
Tactic:
simp [hs₁]
Proof state after:
no goals
Theorem: Finset.mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [(mem_mulStab hCne).mp hxC] at hx
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Theorem: Finset.mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [mem_mulStab_iff_subset_smul_finset (hs₁.mul ht₁)]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
Theorem: Finset.mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
Tactic:
exact hC.symm.left_le_of_le_sup_left (le_sup_right.trans hx.ge)
Proof state after:
no goals
Theorem: Finset.mulStab_union
Proof state before:
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : Disjoint (x • C) (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
⊢ x • C ⊆ C
Tactic:
exact h.left_le_of_le_sup_right (le_sup_left.trans_eq hx)
Proof state after:
no goals
Theorem: Finset.mulStab_union
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ ((C.biUnion fun y => x • y • C.mulStab) ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
Tactic:
have : (x • C.biUnion fun y => y • C.mulStab) = C.biUnion fun y => x • y • C.mulStab :=
  biUnion_image
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
this : (x • C.biUnion fun y => y • C.mulStab) = C.biUnion fun y => x • y • C.mulStab
⊢ ((C.biUnion fun y => x • y • C.mulStab) ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty