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))
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
Tactic:
simpa [← this]
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
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ (x * y) • C.mulStab ⊆ x • C
Tactic:
rw [← smul_eq_mul, smul_assoc, smul_finset_subset_smul_finset_iff]
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
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ y • C.mulStab ⊆ C
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
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ y • C.mulStab ⊆ C
Tactic:
exact smul_finset_mulStab_subset hy
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
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
⊢ Disjoint ((x * y) • C.mulStab) C
Tactic:
convert disjoint_smul_finset_mulStab_mul_mulStab fun hxyC => _
Proof state after:
case h.e'_5
α : 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
⊢ C = ?convert_5 * C.mulStab

case convert_5
α : 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
⊢ Finset α

case convert_7
α : 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 : (x * y) • C.mulStab ⊆ ?convert_5 * C.mulStab
⊢ False
Theorem: Finset.mulStab_union
Proof state before:
case convert_7
α : 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 : (x * y) • C.mulStab ⊆ C * C.mulStab
⊢ False
Tactic:
rw [mul_mulStab] at hxyC
Proof state after:
case convert_7
α : 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 : (x * y) • C.mulStab ⊆ C
⊢ False
Theorem: Finset.mulStab_union
Proof state before:
case convert_7
α : 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 : (x * y) • C.mulStab ⊆ C
⊢ False
Tactic:
exact hyne.not_disjoint (hC.mono_left $ le_iff_subset.2 hxyC)
Proof state after:
no goals
Theorem: Finset.mulStab_union
Proof state before:
case h.e'_5
α : 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
⊢ C = ?convert_5 * C.mulStab
Tactic:
exact C.mul_mulStab.symm
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
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)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
⊢ x • C ⊆ C
Tactic:
have := (card_le_card hxysub).not_lt ((card_lt_card this).trans_eq ?_)
Proof state after:
case refine_2
α : 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)
this✝ : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
this : False
⊢ x • C ⊆ C

case refine_1
α : 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)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
⊢ ((a * b) • C.mulStab).card = ((x * y) • C.mulStab).card
Theorem: Finset.mulStab_union
Proof state before:
case refine_2
α : 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)
this✝ : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
this : False
⊢ x • C ⊆ C

case refine_1
α : 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)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
⊢ ((a * b) • C.mulStab).card = ((x * y) • C.mulStab).card
Tactic:
cases this
Proof state after:
case refine_1
α : 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)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
⊢ ((a * b) • C.mulStab).card = ((x * y) • C.mulStab).card
Theorem: Finset.mulStab_union
Proof state before:
case refine_1
α : 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)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
⊢ ((a * b) • C.mulStab).card = ((x * y) • C.mulStab).card
Tactic:
simp_rw [card_smul_finset]
Proof state after:
no goals
Theorem: Finset.mulStab_union
Proof state before:
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
Tactic:
refine' (mul_subset_mul inter_subset_right inter_subset_right).trans _
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)
⊢ a • C.mulStab * b • C.mulStab ⊆ (a * b) • C.mulStab
Theorem: Finset.mulStab_union
Proof state before:
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 • C.mulStab * b • C.mulStab ⊆ (a * b) • C.mulStab
Tactic:
simp only [smul_mul_smul, mulStab_mul_mulStab, subset_refl]
Proof state after:
no goals
Theorem: Finset.mulStab_union
Proof state before:
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)
Tactic:
contrapose! hab
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
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)
hab : (a * b) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (a * b) • C.mulStab ⊆ s * t
Theorem: Finset.mulStab_union
Proof state before:
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
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)
hab : (a * b) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (a * b) • C.mulStab ⊆ s * t
Tactic:
exact hab.trans (mul_subset_mul inter_subset_left inter_subset_left)
Proof state after:
no goals
Theorem: Finset.mul_aux1
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
ih : (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hconv : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hCun : (C ∪ s' * t').mulStab = (s' * t').mulStab
hsub : (s' * t').mulStab ⊆ C.mulStab
hdisj : Disjoint C (s' * t')
⊢ ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s' * t').mulStab).card <
    ↑C.mulStab.card - ↑(s' * (s' * t').mulStab).card - ↑(t' * (s' * t').mulStab).card
Tactic:
set H := C.mulStab
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
ih : (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hCun : (C ∪ s' * t').mulStab = (s' * t').mulStab
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
hsub : (s' * t').mulStab ⊆ H
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * (s' * t').mulStab).card <
    ↑H.card - ↑(s' * (s' * t').mulStab).card - ↑(t' * (s' * t').mulStab).card
Theorem: Finset.mul_aux1
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
ih : (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hCun : (C ∪ s' * t').mulStab = (s' * t').mulStab
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
hsub : (s' * t').mulStab ⊆ H
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * (s' * t').mulStab).card <
    ↑H.card - ↑(s' * (s' * t').mulStab).card - ↑(t' * (s' * t').mulStab).card
Tactic:
set H' := (s' * t').mulStab
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
H' : Finset α := (s' * t').mulStab
ih : (s' * H').card + (t' * H').card ≤ (s' * t').card + H'.card
hCun : (C ∪ s' * t').mulStab = H'
hsub : H' ⊆ H
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card
Theorem: Finset.mul_aux1
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
H' : Finset α := (s' * t').mulStab
ih : (s' * H').card + (t' * H').card ≤ (s' * t').card + H'.card
hCun : (C ∪ s' * t').mulStab = H'
hsub : H' ⊆ H
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card
Tactic:
set C' := C ∪ s' * t'
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
H' : Finset α := (s' * t').mulStab
ih : (s' * H').card + (t' * H').card ≤ (s' * t').card + H'.card
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hnotconv : C'.card + C'.mulStab.card < (s ∩ t).card + ((s ∪ t) * C'.mulStab).card
hCun : C'.mulStab = H'
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card