internlm/Lean-Github huggingface dataset:
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
hxs : x ∈ combiInterior ℝ s
F : Set (Finset E)
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Tactic:
rw [hsint, mem_iUnion₂] at hxs
Proof state after:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
F : Set (Finset E)
hxs : ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
F : Set (Finset E)
hxs : ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Tactic:
obtain ⟨t, ht, hxt⟩ := hxs
Proof state after:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
t : Finset E
ht : t ∈ F
hxt : x ∈ combiInterior ℝ t
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
t : Finset E
ht : t ∈ F
hxt : x ∈ combiInterior ℝ t
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Tactic:
exact ⟨t, hF ht, hxt⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
hs : ∅ ∈ K₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) ↑s₂
Tactic:
obtain ⟨t, ht⟩ := hempty ⟨_, hs⟩
Proof state after:
case mpr.intro.intro.inl.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
hs : ∅ ∈ K₁
t : Finset E
ht : t ∈ K₂.faces
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) ↑s₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr.intro.intro.inl.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
hs : ∅ ∈ K₁
t : Finset E
ht : t ∈ K₂.faces
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) ↑s₂
Tactic:
exact ⟨t, ht, by simp⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
hs : ∅ ∈ K₁
t : Finset E
ht : t ∈ K₂.faces
⊢ (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) ↑t
Tactic:
simp
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ x ∈ combiInterior ℝ t
Tactic:
rw [hinterior, mem_iUnion₂] at hxt ⊢
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hxt : ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hxt : ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
Tactic:
obtain ⟨u, hu, hxu⟩ := hxt
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F
hxu : x ∈ combiInterior ℝ u
⊢ ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F
hxu : x ∈ combiInterior ℝ u
⊢ ∃ i, ∃ (_ : i ∈ F), x ∈ combiInterior ℝ i
Tactic:
exact ⟨u, hu, hxu⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ x ∈ combiInterior ℝ t'
Tactic:
rw [hinterior', mem_iUnion₂] at hxt' ⊢
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hxt' : ∃ i, ∃ (_ : i ∈ F'), x' ∈ combiInterior ℝ i
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ F'), x ∈ combiInterior ℝ i
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hxt' : ∃ i, ∃ (_ : i ∈ F'), x' ∈ combiInterior ℝ i
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ F'), x ∈ combiInterior ℝ i
Tactic:
obtain ⟨u, hu, hxu⟩ := hxt'
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ ∃ i, ∃ (_ : i ∈ F'), x ∈ combiInterior ℝ i
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ ∃ i, ∃ (_ : i ∈ F'), x ∈ combiInterior ℝ i
Tactic:
refine' ⟨u, hu, _⟩
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ x ∈ combiInterior ℝ u
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ x ∈ combiInterior ℝ u
Tactic:
rw [← disjoint_interiors hs (hF' hu) hx' hxu]
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ x ∈ combiInterior ℝ s
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ x ∈ combiInterior ℝ s
Tactic:
exact hx
Proof state after:
no goals
Theorem: QuotientGroup.preimage_image_mk_eq_iUnion_smul
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
N : Subgroup α
inst✝ : N.Normal
s : Set α
⊢ mk ⁻¹' (mk '' s) = ⋃ x, x • s
Tactic:
simp_rw [QuotientGroup.preimage_image_mk_eq_iUnion_image N s, ← image_smul, Submonoid.smul_def,
  smul_eq_mul, mul_comm]
Proof state after:
no goals
Theorem: SimpleGraph.disjoint_edgeFinset
Proof state before:
α : Type u_1
G H : SimpleGraph α
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype ↑H.edgeSet
⊢ Disjoint G.edgeFinset H.edgeFinset ↔ Disjoint G H
Tactic:
simp_rw [← Finset.disjoint_coe, coe_edgeFinset, disjoint_edgeSet]
Proof state after:
no goals
Theorem: SimpleGraph.edgeFinset_eq_empty
Proof state before:
α : Type u_1
G H : SimpleGraph α
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset = ∅ ↔ G = ⊥
Tactic:
rw [← edgeFinset_bot, edgeFinset_inj]
Proof state after:
no goals
Theorem: SimpleGraph.edgeFinset_nonempty
Proof state before:
α : Type u_1
G H : SimpleGraph α
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset.Nonempty ↔ G ≠ ⊥
Tactic:
rw [Finset.nonempty_iff_ne_empty, edgeFinset_eq_empty.ne]
Proof state after:
no goals
Theorem: eqn_solvable_divides
Proof state before:
a b c : ℤ
⊢ (∃ x y, a * x + b * y = c) → ↑(Int.gcd a b) ∣ c
Tactic:
intro ⟨x, y, h⟩
Proof state after:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ c
Theorem: eqn_solvable_divides
Proof state before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ c
Tactic:
rw [← h]
Proof state after:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x + b * y
Theorem: eqn_solvable_divides
Proof state before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x + b * y
Tactic:
apply dvd_add
Proof state after:
case h₁
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x

case h₂
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b * y
Theorem: eqn_solvable_divides
Proof state before:
case h₁
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x
Tactic:
trans a
Proof state after:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a

a b c x y : ℤ
h : a * x + b * y = c
⊢ a ∣ a * x
Theorem: eqn_solvable_divides
Proof state before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a
Tactic:
apply Int.gcd_dvd_left
Proof state after:
no goals
Theorem: eqn_solvable_divides
Proof state before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ a ∣ a * x
Tactic:
apply Int.dvd_mul_right
Proof state after:
no goals
Theorem: eqn_solvable_divides
Proof state before:
case h₂
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b * y
Tactic:
trans b
Proof state after:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b

a b c x y : ℤ
h : a * x + b * y = c
⊢ b ∣ b * y
Theorem: eqn_solvable_divides
Proof state before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b
Tactic:
apply Int.gcd_dvd_right
Proof state after:
no goals
Theorem: eqn_solvable_divides
Proof state before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ b ∣ b * y
Tactic:
apply Int.dvd_mul_right
Proof state after:
no goals
Theorem: Nat.minus_add_cancel
Proof state before:
m n : ℕ
hyp : n ≤ m
⊢ minus m n hyp + n = m
Tactic:
match m, n, hyp with
| m, 0, _ => simp [minus]
| 0, _ +1, pf => contradiction
| m + 1, n + 1 , pf =>
  simp [minus]
  rw [← add_assoc]
  simp [minus_add_cancel]
Proof state after:
no goals
Theorem: Nat.minus_add_cancel
Proof state before:
m✝ n : ℕ
hyp : n ≤ m✝
m : ℕ
x✝ : 0 ≤ m
⊢ minus m 0 x✝ + 0 = m
Tactic:
simp [minus]
Proof state after:
no goals
Theorem: Nat.minus_add_cancel
Proof state before:
m n : ℕ
hyp : n ≤ m
n✝ : ℕ
pf : n✝ + 1 ≤ 0
⊢ minus 0 (n✝ + 1) pf + (n✝ + 1) = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.minus_add_cancel
Proof state before:
m✝ n✝ : ℕ
hyp : n✝ ≤ m✝
m n : ℕ
pf : n + 1 ≤ m + 1
⊢ minus (m + 1) (n + 1) pf + (n + 1) = m + 1
Tactic:
simp [minus]
Proof state after:
m✝ n✝ : ℕ
hyp : n✝ ≤ m✝
m n : ℕ
pf : n + 1 ≤ m + 1
⊢ minus m n ⋯ + (n + 1) = m + 1
Theorem: Nat.minus_add_cancel
Proof state before:
m✝ n✝ : ℕ
hyp : n✝ ≤ m✝
m n : ℕ
pf : n + 1 ≤ m + 1
⊢ minus m n ⋯ + (n + 1) = m + 1
Tactic:
rw [← add_assoc]
Proof state after:
m✝ n✝ : ℕ
hyp : n✝ ≤ m✝
m n : ℕ
pf : n + 1 ≤ m + 1
⊢ minus m n ⋯ + n + 1 = m + 1
Theorem: Nat.minus_add_cancel
Proof state before:
m✝ n✝ : ℕ
hyp : n✝ ≤ m✝
m n : ℕ
pf : n + 1 ≤ m + 1
⊢ minus m n ⋯ + n + 1 = m + 1
Tactic:
simp [minus_add_cancel]
Proof state after:
no goals
Theorem: four_le_seven
Proof state before:
⊢ 4 ≤ 7
Tactic:
apply Nat.le_step
Proof state after:
case h

⊢ 4 ≤ 6
Theorem: four_le_seven
Proof state before:
case h

⊢ 4 ≤ 6
Tactic:
apply Nat.le_step
Proof state after:
case h.h

⊢ 4 ≤ 5
Theorem: four_le_seven
Proof state before:
case h.h

⊢ 4 ≤ 5
Tactic:
apply Nat.le_step
Proof state after:
case h.h.h

⊢ 4 ≤ 4
Theorem: four_le_seven
Proof state before:
case h.h.h

⊢ 4 ≤ 4
Tactic:
apply Nat.le_refl
Proof state after:
no goals
Theorem: four_le_ten
Proof state before:
⊢ 4 ≤ 10
Tactic:
decide
Proof state after:
no goals
Theorem: Waffle.disagree_eq_maybe
Proof state before:
ans : Answer
⊢ disagree ans = ans → ans = Answer.maybe
Tactic:
cases ans <;> simp [disagree]
Proof state after:
no goals
Theorem: Waffle.le_trans
Proof state before:
a b c : Answer
⊢ a ≤ b → b ≤ c → a ≤ c
Tactic:
intro h₁ h₂
Proof state after:
a b c : Answer
h₁ : a ≤ b
h₂ : b ≤ c
⊢ a ≤ c
Theorem: Waffle.le_trans
Proof state before:
a b c : Answer
h₁ : a ≤ b
h₂ : b ≤ c
⊢ a ≤ c
Tactic:
cases c₁:h₁
Proof state after:
case no_le
b c : Answer
h₂ : b ≤ c
h₁ : Answer.no ≤ b
c₁ : h₁ = ⋯
⊢ Answer.no ≤ c

case le_yes
a c : Answer
h₁ : a ≤ Answer.yes
h₂ : Answer.yes ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c

case refl
a c : Answer
h₁ : a ≤ a
h₂ : a ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c
Theorem: Waffle.le_trans
Proof state before:
b c : Answer
h₂ : b ≤ c
h₁ : Answer.no ≤ b
c₁ : h₁ = ⋯
⊢ Answer.no ≤ c
Tactic:
case no_le => 
  apply Answer.le.no_le
Proof state after:
no goals