internlm/Lean-Github huggingface dataset:
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hab : ¬(a * c * (b * d)) • C.mulStab ⊆ s * t
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * c * (b * d)) • C.mulStab
hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
z : α
hz : z ∈ (a * c * (b * d)) • C.mulStab
hzst : z ∉ s * t
w : α
hw : w ∈ C.mulStab
hwz : (a * c * (b * d)) • w = z
⊢ ∃ b_1 ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab), w • b_1 ∉ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
Tactic:
refine' ⟨a * c * (b * d), by convert hxy, _⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hab : ¬(a * c * (b * d)) • C.mulStab ⊆ s * t
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * c * (b * d)) • C.mulStab
hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
z : α
hz : z ∈ (a * c * (b * d)) • C.mulStab
hzst : z ∉ s * t
w : α
hw : w ∈ C.mulStab
hwz : (a * c * (b * d)) • w = z
⊢ w • (a * c * (b * d)) ∉ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hab : ¬(a * c * (b * d)) • C.mulStab ⊆ s * t
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * c * (b * d)) • C.mulStab
hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
z : α
hz : z ∈ (a * c * (b * d)) • C.mulStab
hzst : z ∉ s * t
w : α
hw : w ∈ C.mulStab
hwz : (a * c * (b * d)) • w = z
⊢ w • (a * c * (b * d)) ∉ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
Tactic:
rw [smul_eq_mul, mul_comm, ← smul_eq_mul, hwz]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hab : ¬(a * c * (b * d)) • C.mulStab ⊆ s * t
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * c * (b * d)) • C.mulStab
hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
z : α
hz : z ∈ (a * c * (b * d)) • C.mulStab
hzst : z ∉ s * t
w : α
hw : w ∈ C.mulStab
hwz : (a * c * (b * d)) • w = z
⊢ z ∉ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hab : ¬(a * c * (b * d)) • C.mulStab ⊆ s * t
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * c * (b * d)) • C.mulStab
hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
z : α
hz : z ∈ (a * c * (b * d)) • C.mulStab
hzst : z ∉ s * t
w : α
hw : w ∈ C.mulStab
hwz : (a * c * (b * d)) • w = z
⊢ z ∉ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
Tactic:
exact not_mem_mono (mul_subset_mul inter_subset_left inter_subset_left) hzst
Proof state after:
no goals
Theorem: Finset.mulStab_mul_ssubset_mulStab
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
⊢ C.Nonempty
Tactic:
contrapose! hab
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 : ¬C.Nonempty
⊢ (a * b) • C.mulStab ⊆ s * t
Theorem: Finset.mulStab_mul_ssubset_mulStab
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 : ¬C.Nonempty
⊢ (a * b) • C.mulStab ⊆ s * t
Tactic:
simp only [not_nonempty_iff_eq_empty] at hab
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 : C = ∅
⊢ (a * b) • C.mulStab ⊆ s * t
Theorem: Finset.mulStab_mul_ssubset_mulStab
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 : C = ∅
⊢ (a * b) • C.mulStab ⊆ s * t
Tactic:
simp only [hab, mulStab_empty, smul_finset_empty, empty_subset]
Proof state after:
no goals
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
Tactic:
have hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) := mul_mem_mul hx hy
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
Tactic:
apply subset_trans (mulStab_subset_div_right hxymem)
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) / {x * y} ⊆ C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) / {x * y} ⊆ C.mulStab
Tactic:
have : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab := by
  apply subset_trans (mul_subset_mul inter_subset_right inter_subset_right)
  rw [smul_mul_smul]
  rw [← hac, ← had, smul_mul_smul, smul_assoc]
  apply smul_finset_subset_smul_finset
  rw [← smul_smul]
  rw [mul_subset_iff]
  intro x hx y hy
  rw [smul_mulStab hd, smul_mulStab hc, mem_mulStab hCne, ← smul_smul,
    (mem_mulStab hCne).mp hy, (mem_mulStab hCne).mp hx]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) / {x * y} ⊆ C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) / {x * y} ⊆ C.mulStab
Tactic:
apply subset_trans (div_subset_div_right this) _
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
⊢ (x * y) • C.mulStab / {x * y} ⊆ C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
⊢ (x * y) • C.mulStab / {x * y} ⊆ C.mulStab
Tactic:
have hsing : (x * y) • C.mulStab = {x * y} * C.mulStab := by rw [singleton_mul]; rfl
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
hsing : (x * y) • C.mulStab = {x * y} * C.mulStab
⊢ (x * y) • C.mulStab / {x * y} ⊆ C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
hsing : (x * y) • C.mulStab = {x * y} * C.mulStab
⊢ (x * y) • C.mulStab / {x * y} ⊆ C.mulStab
Tactic:
simp_rw [hsing, singleton_mul, div_singleton, image_image, div_eq_mul_inv, mul_comm, comp,
  mul_inv_cancel_right, image_id', subset_refl]
Proof state after:
no goals
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
Tactic:
apply subset_trans (mul_subset_mul inter_subset_right inter_subset_right)
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ a • C.mulStab * b • C.mulStab ⊆ (x * y) • C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ a • C.mulStab * b • C.mulStab ⊆ (x * y) • C.mulStab
Tactic:
rw [smul_mul_smul]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (a * b) • (C.mulStab * C.mulStab) ⊆ (x * y) • C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (a * b) • (C.mulStab * C.mulStab) ⊆ (x * y) • C.mulStab
Tactic:
rw [← hac, ← had, smul_mul_smul, smul_assoc]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (a * b) • (C.mulStab * C.mulStab) ⊆ (a * b) • (c * d) • C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (a * b) • (C.mulStab * C.mulStab) ⊆ (a * b) • (c * d) • C.mulStab
Tactic:
apply smul_finset_subset_smul_finset
Proof state after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ C.mulStab * C.mulStab ⊆ (c * d) • C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ C.mulStab * C.mulStab ⊆ (c * d) • C.mulStab
Tactic:
rw [← smul_smul]
Proof state after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ C.mulStab * C.mulStab ⊆ c • d • C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ C.mulStab * C.mulStab ⊆ c • d • C.mulStab
Tactic:
rw [mul_subset_iff]
Proof state after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ ∀ x ∈ C.mulStab, ∀ y ∈ C.mulStab, x * y ∈ c • d • C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ ∀ x ∈ C.mulStab, ∀ y ∈ C.mulStab, x * y ∈ c • d • C.mulStab
Tactic:
intro x hx y hy
Proof state after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x✝ : α
hx✝ : x✝ ∈ s ∩ a • C.mulStab
y✝ : α
hy✝ : y✝ ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x✝
d : α
hd : d ∈ C.mulStab
had : b • d = y✝
hxymem : x✝ * y✝ ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
x : α
hx : x ∈ C.mulStab
y : α
hy : y ∈ C.mulStab
⊢ x * y ∈ c • d • C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x✝ : α
hx✝ : x✝ ∈ s ∩ a • C.mulStab
y✝ : α
hy✝ : y✝ ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x✝
d : α
hd : d ∈ C.mulStab
had : b • d = y✝
hxymem : x✝ * y✝ ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
x : α
hx : x ∈ C.mulStab
y : α
hy : y ∈ C.mulStab
⊢ x * y ∈ c • d • C.mulStab
Tactic:
rw [smul_mulStab hd, smul_mulStab hc, mem_mulStab hCne, ← smul_smul,
  (mem_mulStab hCne).mp hy, (mem_mulStab hCne).mp hx]
Proof state after:
no goals
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
⊢ (x * y) • C.mulStab = {x * y} * C.mulStab
Tactic:
rw [singleton_mul]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
⊢ (x * y) • C.mulStab = image (fun x_1 => x * y * x_1) C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
⊢ (x * y) • C.mulStab = image (fun x_1 => x * y * x_1) C.mulStab
Tactic:
rfl
Proof state after:
no goals
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
⊢ (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
Tactic:
rw [smul_eq_iff_eq_inv_smul, ← smul_assoc, smul_eq_mul, mul_assoc, mul_comm c _, ← mul_assoc, ←
  mul_assoc, ← mul_assoc, mul_assoc _ a b, inv_mul_self (a * b), one_mul, ← smul_eq_mul,
  smul_assoc, smul_mulStab hc, smul_mulStab hd]
Proof state after:
no goals
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab
Tactic:
apply subset_trans (mul_subset_mul inter_subset_right inter_subset_right)
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
⊢ a • C.mulStab * b • C.mulStab ⊆ (a * b) • C.mulStab
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • 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_mul_ssubset_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hab : ¬(a * c * (b * d)) • C.mulStab ⊆ s * t
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * c * (b * d)) • C.mulStab
hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
z : α
hz : z ∈ (a * c * (b * d)) • C.mulStab
hzst : z ∉ s * t
w : α
hw : w ∈ C.mulStab
hwz : (a * c * (b * d)) • w = z
⊢ a * c * (b * d) ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
Tactic:
convert hxy
Proof state after:
no goals