internlm/Lean-Github huggingface dataset:
Theorem: Finset.mulImpact_map_of_infinite
Proof state before:
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n ≤ s.mulImpact n
Tactic:
refine' le_ciInf fun t => _
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
t : { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n ≤ (s * ↑t).card
Theorem: Finset.mulImpact_map_of_infinite
Proof state before:
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
t : { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n ≤ (s * ↑t).card
Tactic:
sorry
Proof state after:
no goals
Theorem: Finset.mulImpact_map_of_infinite
Proof state before:
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ s.mulImpact n ≤ (map { toFun := ⇑f, inj' := hf } s).mulImpact n
Tactic:
refine' le_ciInf fun t => _
Proof state after:
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
t : { t // t.card = n }
⊢ s.mulImpact n ≤ (map { toFun := ⇑f, inj' := hf } s * ↑t).card
Theorem: Finset.mulImpact_map_of_infinite
Proof state before:
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
t : { t // t.card = n }
⊢ s.mulImpact n ≤ (map { toFun := ⇑f, inj' := hf } s * ↑t).card
Tactic:
sorry
Proof state after:
no goals
Theorem: ZMod.min_le_card_add'
Proof state before:
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Tactic:
haveI : Fact p.Prime := ⟨hp⟩
Proof state after:
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Theorem: ZMod.min_le_card_add'
Proof state before:
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Tactic:
obtain h | h := eq_bot_or_eq_top (AddAction.stabilizer (ZMod p) (s + t))
Proof state after:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊥
⊢ min p (s.card + t.card - 1) ≤ (s + t).card

case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊤
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Theorem: ZMod.min_le_card_add'
Proof state before:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊥
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Tactic:
refine' min_le_of_right_le _
Proof state after:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊥
⊢ s.card + t.card - 1 ≤ (s + t).card
Theorem: ZMod.min_le_card_add'
Proof state before:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊥
⊢ s.card + t.card - 1 ≤ (s + t).card
Tactic:
rw [← AddSubgroup.coe_eq_zero, ← coe_addStab (hs.add ht), coe_eq_zero] at h
Proof state after:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = 0
⊢ s.card + t.card - 1 ≤ (s + t).card
Theorem: ZMod.min_le_card_add'
Proof state before:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = 0
⊢ s.card + t.card - 1 ≤ (s + t).card
Tactic:
simpa [*] using add_kneser s t
Proof state after:
no goals
Theorem: ZMod.min_le_card_add'
Proof state before:
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊤
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Tactic:
rw [← AddSubgroup.coe_eq_univ, ← coe_addStab (hs.add ht), coe_eq_univ] at h
Proof state after:
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = univ
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Theorem: ZMod.min_le_card_add'
Proof state before:
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = univ
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Tactic:
refine' card_addStab_le_card.trans' _
Proof state after:
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = univ
⊢ min p (s.card + t.card - 1) ≤ (s + t).addStab.card
Theorem: ZMod.min_le_card_add'
Proof state before:
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = univ
⊢ min p (s.card + t.card - 1) ≤ (s + t).addStab.card
Tactic:
simp [*, card_univ]
Proof state after:
no goals
Theorem: mul_tsub_one
Proof state before:
α : Type u_1
inst✝⁴ : CanonicallyOrderedCommSemiring α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b - 1) = a * b - a
Tactic:
rw [mul_tsub, mul_one]
Proof state after:
no goals
Theorem: tsub_one_mul
Proof state before:
α : Type u_1
inst✝⁴ : CanonicallyOrderedCommSemiring α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a - 1) * b = a * b - b
Tactic:
rw [tsub_mul, one_mul]
Proof state after:
no goals
Theorem: ProbabilityTheory.iIndep_comap_iff
Proof state before:
Ω : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝ : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
S : Finset ι
s : ι → Set Ω
f : (i : ι) → Ω → β i
⊢ iIndep (fun i => MeasurableSpace.comap (fun x => x ∈ s i) ⊤) μ ↔ iIndepSet s μ
Tactic:
simp_rw [← generateFrom_singleton]
Proof state after:
Ω : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝ : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
S : Finset ι
s : ι → Set Ω
f : (i : ι) → Ω → β i
⊢ iIndep (fun i => generateFrom {s i}) μ ↔ iIndepSet s μ
Theorem: ProbabilityTheory.iIndep_comap_iff
Proof state before:
Ω : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝ : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
S : Finset ι
s : ι → Set Ω
f : (i : ι) → Ω → β i
⊢ iIndep (fun i => generateFrom {s i}) μ ↔ iIndepSet s μ
Tactic:
rfl
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors
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
⊢ K₁.Subdivides K₂ ↔ K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
Tactic:
refine' ⟨fun h => ⟨h.1.superset, fun s hs => _⟩, fun h =>
  ⟨h.1.antisymm' fun x hx => _, fun s₁ hs₁ => _⟩⟩
Proof state after:
case refine'_1
𝕜 : 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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂

case refine'_2
𝕜 : 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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx : x ∈ K₁.space
⊢ x ∈ K₂.space

case refine'_3
𝕜 : 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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors
Proof state before:
case refine'_1
𝕜 : 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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂
Tactic:
obtain ⟨t, ht, hst⟩ := h.2 hs
Proof state after:
case refine'_1.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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
t : Finset E
ht : t ∈ K₂
hst : (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors
Proof state before:
case refine'_1.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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
t : Finset E
ht : t ∈ K₂
hst : (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂
Tactic:
obtain ⟨u, hut, hu, hsu⟩ :=
  simplex_combiInteriors_split_interiors_nonempty (K₁.nonempty hs) (K₂.indep ht) hst
Proof state after:
case refine'_1.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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
t : Finset E
ht : t ∈ K₂
hst : (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
u : Finset E
hut : u ⊆ t
hu : u.Nonempty
hsu : combiInterior ℝ s ⊆ combiInterior ℝ u
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors
Proof state before:
case refine'_1.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
h : K₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
t : Finset E
ht : t ∈ K₂
hst : (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
u : Finset E
hut : u ⊆ t
hu : u.Nonempty
hsu : combiInterior ℝ s ⊆ combiInterior ℝ u
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂
Tactic:
exact ⟨u, K₂.down_closed' ht hut hu, hsu⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors
Proof state before:
case refine'_2
𝕜 : 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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx : x ∈ K₁.space
⊢ x ∈ K₂.space
Tactic:
obtain ⟨s₁, hs₁, hx⟩ := mem_space_iff.1 hx
Proof state after:
case refine'_2.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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
⊢ x ∈ K₂.space
Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors
Proof state before:
case refine'_2.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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
⊢ x ∈ K₂.space
Tactic:
obtain ⟨s₂, hs₂, hs₁s₂⟩ := h.2 _ hs₁
Proof state after:
case refine'_2.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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ x ∈ K₂.space
Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors
Proof state before:
case refine'_2.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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ x ∈ K₂.space
Tactic:
rw [mem_space_iff]
Proof state after:
case refine'_2.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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ ∃ s ∈ K₂.faces, x ∈ (convexHull ℝ) ↑s
Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors
Proof state before:
case refine'_2.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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ ∃ s ∈ K₂.faces, x ∈ (convexHull ℝ) ↑s
Tactic:
exact ⟨s₂, hs₂, convexHull_subset_convexHull_of_combiInterior_subset_combiInterior
  (K₁.indep hs₁) (K₂.indep hs₂) hs₁s₂ hx⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors
Proof state before:
case refine'_3
𝕜 : 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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
Tactic:
obtain ⟨s₂, hs₂, hs₁s₂⟩ := h.2 _ hs₁
Proof state after:
case refine'_3.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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_combiInteriors_subset_combiInteriors
Proof state before:
case refine'_3.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
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
Tactic:
exact ⟨_, hs₂, convexHull_subset_convexHull_of_combiInterior_subset_combiInterior (K₁.indep hs₁)
  (K₂.indep hs₂) hs₁s₂⟩
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
⊢ K₁.Subdivides K₂ ↔
    (K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
      K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
Tactic:
constructor
Proof state after:
case mp
𝕜 : 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
⊢ K₁.Subdivides K₂ →
    (K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
      K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁

case mpr
𝕜 : 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
⊢ ((K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
      K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁) →
    K₁.Subdivides K₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp
𝕜 : 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
⊢ K₁.Subdivides K₂ →
    (K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
      K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
Tactic:
rintro ⟨hspace, hsubdiv⟩
Proof state after:
case mp.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
⊢ (K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
    K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
⊢ (K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
    K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
Tactic:
refine' ⟨_, hspace.le, fun s hs => _⟩
Proof state after:
case mp.intro.refine'_1
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
⊢ K₁.faces.Nonempty → K₂.faces.Nonempty

case mp.intro.refine'_2
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
⊢ ∃ F ⊆ K₁.faces, combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
⊢ ∃ F ⊆ K₁.faces, combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
Tactic:
refine' ⟨{t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, fun t ht => ht.1, _⟩
Proof state after:
case mp.intro.refine'_2
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
⊢ combiInterior ℝ s = ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
⊢ combiInterior ℝ s = ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
ext x
Proof state after:
case mp.intro.refine'_2.h
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ x ∈ combiInterior ℝ s ↔ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ x ∈ combiInterior ℝ s ↔ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
refine' ⟨fun hxs => _, _⟩
Proof state after:
case mp.intro.refine'_2.h.refine'_1
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁

case mp.intro.refine'_2.h.refine'_2
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁ → x ∈ combiInterior ℝ s