internlm/Lean-Github huggingface dataset:
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof state before:
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∉ K.space
⊢ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
Tactic:
convert finite_empty
Proof state after:
case h.e'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∉ K.space
⊢ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s} = ∅
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof state before:
case h.e'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∉ K.space
⊢ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s} = ∅
Tactic:
exact eq_empty_of_forall_not_mem fun s hX => hxspace <| mem_biUnion hX.1 hX.2
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof state before:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
⊢ (∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite) → K.LocallyFinite
Tactic:
rintro hS s - ⟨x, hx⟩
Proof state after:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
hS : ∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
s : Finset E
x : E
hx : x ∈ s
⊢ K.LocallyFiniteAt s
Theorem: Geometry.SimplicialComplex.locallyFinite_iff_mem_finitely_many_faces
Proof state before:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
hS : ∀ (x : E), {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
s : Finset E
x : E
hx : x ∈ s
⊢ K.LocallyFiniteAt s
Tactic:
exact (hS x).subset fun t => And.imp_right fun ht => subset_convexHull _ _ <| ht 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 : α
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]
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
hCne : C.Nonempty
⊢ (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 : α
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₁
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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₁
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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)
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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)
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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]
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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]
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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]
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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
Proof 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
Theorem: Finset.mulStab_mul_ssubset_mulStab
Proof 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
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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ 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
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
Tactic:
refine' (Finset.ssubset_iff_of_subset hsubset).mpr ⟨w, hw, _⟩
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 ∉ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).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 ∉ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [mem_mulStab' ⟨x * y, 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
⊢ ¬∀ ⦃b_1 : α⦄, b_1 ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) → w • b_1 ∈ 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
⊢ ¬∀ ⦃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
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
⊢ ∃ b_1 ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab), w • b_1 ∉ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)