Theorem: Finset.mulStab_mul_ssubset_mulStab (LeanCamCombi/Kneser/Kneser.lean)

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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
have hCne : C.Nonempty := by
  contrapose! hab
  simp only [not_nonempty_iff_eq_empty] at hab
  simp only [hab, mulStab_empty, smul_finset_empty, empty_subset]
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
hCne : C.Nonempty
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

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
hCne : C.Nonempty
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
obtain ⟨x, hx⟩ := hs₁
State after:
case intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

State before:
case intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
obtain ⟨y, hy⟩ := ht₁
State after:
case intro.intro
α : 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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

State before:
case intro.intro
α : 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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
obtain ⟨c, hc, hac⟩ := mem_smul_finset.mp (mem_of_mem_inter_right hx)
State after:
case intro.intro.intro.intro
α : 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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

State before:
case intro.intro.intro.intro
α : 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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
obtain ⟨d, hd, had⟩ := mem_smul_finset.mp (mem_of_mem_inter_right hy)
State after:
case intro.intro.intro.intro.intro.intro
α : 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

State before:
case intro.intro.intro.intro.intro.intro
α : 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 hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab := by
  have hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) := mul_mem_mul hx hy
  apply subset_trans (mulStab_subset_div_right hxymem)
  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]
  apply subset_trans (div_subset_div_right this) _
  have hsing : (x * y) • C.mulStab = {x * y} * C.mulStab := by rw [singleton_mul]; rfl
  simp_rw [hsing, singleton_mul, div_singleton, image_image, div_eq_mul_inv, mul_comm, comp,
    mul_inv_cancel_right, image_id', subset_refl]
State after:
case intro.intro.intro.intro.intro.intro
α : 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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

State before:
case intro.intro.intro.intro.intro.intro
α : 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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
have : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab := by
  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]
State after:
case intro.intro.intro.intro.intro.intro
α : 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)).mulStab ⊂ C.mulStab

State before:
case intro.intro.intro.intro.intro.intro
α : 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)).mulStab ⊂ C.mulStab
Tactic:
have hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab := by
  apply subset_trans (mul_subset_mul inter_subset_right inter_subset_right)
  simp only [smul_mul_smul, mulStab_mul_mulStab, subset_refl]
State after:
case intro.intro.intro.intro.intro.intro
α : 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
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

State before:
case intro.intro.intro.intro.intro.intro
α : 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
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
have hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) := mul_mem_mul hx hy
State after:
case intro.intro.intro.intro.intro.intro
α : 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
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab
hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

State before:
case intro.intro.intro.intro.intro.intro
α : 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
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab
hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
rw [this] at hsub
State after:
case intro.intro.intro.intro.intro.intro
α : 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
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)
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

State before:
case intro.intro.intro.intro.intro.intro
α : 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
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)
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
rw [this] at hab
State after:
case 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)
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

State before:
case 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)
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
obtain ⟨z, hz, hzst⟩ := not_subset.1 hab
State after:
case 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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

State before:
case 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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
obtain ⟨w, hw, hwz⟩ := mem_smul_finset.mp hz
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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
refine' (Finset.ssubset_iff_of_subset hsubset).mpr ⟨w, hw, _⟩
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 ∉ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

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 ∉ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [mem_mulStab' ⟨x * y, hxy⟩]
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
⊢ ¬∀ ⦃b_1 : α⦄, b_1 ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) → w • b_1 ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)

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 : α⦄, b_1 ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) → w • b_1 ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
Tactic:
push_neg
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
⊢ ∃ b_1 ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab), w • b_1 ∉ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)

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, _⟩
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)

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]
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)

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
State after:
no goals

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
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

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
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

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]
State after:
no goals

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
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

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)
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

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]
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

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) _
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

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
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

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]
State after:
no goals

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)
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

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]
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

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]
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

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
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

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]
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

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]
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

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
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

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]
State after:
no goals

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]
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

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
State after:
no goals

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]
State after:
no goals

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)
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

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]
State after:
no goals

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
State after:
no goals