awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
h :
  ∃ (s_1 : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w = p
h₁ :
  ∀ (u : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜) (hw : ∀ i ∈ u, 0 ≤ w i) (hw1 : u.sum w = 1),
    Membership.mem (α := V) s.closedInterior ((Finset.affineCombination 𝕜 u s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)
⊢ p ∈ s.closedInterior

Tactic:
obtain ⟨u, w, hw, hw1, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
i : Fin (n + 1)
hi : i ∈ u
rw : w i ≤ u.sum w
⊢ w i ≤ 1

Tactic:
rw [← hw1]
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
i : Fin (n + 1)
hi : i ∈ u
⊢ w i ≤ u.sum w

Tactic:
apply Finset.single_le_sum (fun j hj ↦ hw j hj) hi

Premises used: Finset.single_le_sum
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
⊢ ∀ i ∈ u, w i ≤ 1

Tactic:
have hw' : ∀ i ∈ u, w i ≤ 1 := by
      intro i hi
      rw [← hw1]
      apply Finset.single_le_sum (fun j hj ↦ hw j hj) hi
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), (↑u : Set (Fin (n + 1))).indicator w i) 1

Tactic:
simpa [Finset.sum_indicator_subset _ u.subset_univ] using hw1

Premises used: Finset.sum_indicator_subset, Finset.subset_univ
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), (↑u : Set (Fin (n + 1))).indicator w i) 1

Tactic:
have hw1' : ∑ i, (u : Set (Fin (n + 1))).indicator w i = 1 := by
      simpa [Finset.sum_indicator_subset _ u.subset_univ] using hw1
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), (↑u : Set (Fin (n + 1))).indicator w i) 1
h : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)
⊢ Membership.mem (α := V) s.closedInterior ((Finset.affineCombination 𝕜 u s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)

Tactic:
rw [Finset.affineCombination_indicator_subset _ _ u.subset_univ,
      affineCombination_mem_closedInterior_iff hw1']

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_iff, Finset.affineCombination_indicator_subset, Finset.subset_univ
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), (↑u : Set (Fin (n + 1))).indicator w i) 1
i : Fin (n + 1)
pos :
  ∀ (hi : i ∈ (↑u : Set (Fin (n + 1)))), Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)
neg :
  ∀ (hi : i ∉ (↑u : Set (Fin (n + 1)))), Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)
⊢ Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)

Tactic:
by_cases hi : i ∈ (u : Set (Fin (n + 1)))

Premises used: SetLike.coe
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), (↑u : Set (Fin (n + 1))).indicator w i) 1
i : Fin (n + 1)
hi : i ∈ (↑u : Set (Fin (n + 1)))
⊢ Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)

Tactic:
aesop
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), (↑u : Set (Fin (n + 1))).indicator w i) 1
i : Fin (n + 1)
hi : i ∉ (↑u : Set (Fin (n + 1)))
⊢ Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)

Tactic:
aesop
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
h : p ∈ s.closedInterior
h₁ :
  ∀ (w : Fin (n + 1) → 𝕜) (hw1 : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), w i) 1)
    (h :
      Membership.mem (α := V) s.closedInterior
        ((Finset.affineCombination 𝕜 Finset.univ s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)),
    ∃ (s_1 : Finset (Fin (n + 1))) (w_1 : Fin (n + 1) → 𝕜),
      (∀ i ∈ s_1, 0 ≤ w_1 i) ∧
        s_1.sum w_1 = 1 ∧
          Eq.{u_2 + 1} (α := V) ((Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w_1 : V)
            ((Finset.affineCombination 𝕜 Finset.univ s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)
⊢ ∃ (s_1 : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w = p

Tactic:
obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype <|
      Set.mem_of_mem_of_subset h s.closedInterior_subset_affineSpan

Premises used: eq_affineCombination_of_mem_affineSpan_of_fintype, Set.mem_of_mem_of_subset, Affine.Simplex.closedInterior_subset_affineSpan, rfl
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
w : Fin (n + 1) → 𝕜
hw1 : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), w i) 1
h :
  Membership.mem (α := V) s.closedInterior
    ((Finset.affineCombination 𝕜 Finset.univ s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)
⊢ ∀ (i : Fin (n + 1)), Membership.mem (γ := Set 𝕜) (Icc 0 1) (w i)

Tactic:
rw [affineCombination_mem_closedInterior_iff hw1] at h

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_iff
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
w : Fin (n + 1) → 𝕜
hw1 : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), w i) 1
h : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set 𝕜) (Icc 0 1) (w i)
⊢ ∃ (s_1 : Finset (Fin (n + 1))) (w_1 : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w_1 i) ∧
      s_1.sum w_1 = 1 ∧
        Eq.{u_2 + 1} (α := V) ((Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w_1 : V)
          ((Finset.affineCombination 𝕜 Finset.univ s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)

Tactic:
⟨Finset.univ, w, fun i _ ↦ (h i).1, hw1, rfl⟩

Premises used: Finset.univ, And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
w : Fin (n + 1) → 𝕜
hw1 : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), w i) 1
h : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set 𝕜) (Icc 0 1) (w i)
⊢ ∃ (s_1 : Finset (Fin (n + 1))) (w_1 : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w_1 i) ∧
      s_1.sum w_1 = 1 ∧
        Eq.{u_2 + 1} (α := V) ((Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w_1 : V)
          ((Finset.affineCombination 𝕜 Finset.univ s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)

Tactic:
exact ⟨Finset.univ, w, fun i _ ↦ (h i).1, hw1, rfl⟩
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
⊢ Injective.{u_3 + 1, u_3 + 1} (α := ProperCone R E) toPointedCone

Tactic:
ClosedSubmodule.toSubmodule_injective

Premises used: ClosedSubmodule.toSubmodule_injective
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
C₁ C₂ : ProperCone R E
h : ∀ (x : E), x ∈ C₁ ↔ x ∈ C₂
⊢ C₁ = C₂

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
C : ProperCone R E
x : E
⊢ x ∈ (↑C : PointedCone R E) ↔ x ∈ C

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
C : ProperCone R E
⊢ (↑(↑C : PointedCone R E) : ConvexCone R E).Pointed

Tactic:
C.toPointedCone.pointed_toConvexCone

Premises used: PointedCone.pointed_toConvexCone, ProperCone.toPointedCone
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
C : ProperCone R E
⊢ (↑C : Set E).Nonempty

Tactic:
C.toSubmodule.nonempty

Premises used: ClosedSubmodule.toSubmodule, Submodule.nonempty
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
C : ProperCone R E
⊢ IsClosed (↑C : Set E)

Tactic:
C.isClosed'

Premises used: ClosedSubmodule.isClosed'
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
C : ProperCone R E
⊢ Convex R (↑C : Set E)

Tactic:
C.toPointedCone.convex

Premises used: PointedCone.convex, ProperCone.toPointedCone
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
r : R
x : E
C : ProperCone R E
hx : x ∈ C
hr : 0 ≤ r
⊢ r • x ∈ C

Tactic:
C.smul_mem ⟨r, hr⟩ hx

Premises used: Set.Mem, ClosedSubmodule.toSubmodule, Subtype.mk, Submodule.smul_mem
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
x : E
inst_6 : T1Space E
⊢ Membership.mem (γ := ProperCone R E) ⊥ x ↔ x = 0

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
inst_6 : T1Space E
⊢ (↑⊥ : Set E) = {0}

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
inst_6 : T1Space E
⊢ Eq.{u_3 + 1} (α := PointedCone R E) (↑⊥ : PointedCone R E) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
F : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid F
inst_4 : TopologicalSpace F
inst_5 : Module R F
C : ProperCone R F
⊢ comap (ContinuousLinearMap.id R F) C = C

Tactic:
rfl

Premises used: Set.Mem, setOf, ClosedSubmodule.comap, Submodule.comap, Set.preimage, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
inst_6 : AddCommMonoid F
inst_7 : TopologicalSpace F
inst_8 : Module R F
f : E →L[R] F
C : ProperCone R F
⊢ (↑(comap f C) : Set E) = (⇑f : (a : E) → F) ⁻¹' (↑C : Set F)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
inst_6 : AddCommMonoid F
inst_7 : TopologicalSpace F
inst_8 : Module R F
inst_9 : AddCommMonoid G
inst_10 : TopologicalSpace G
inst_11 : Module R G
g : F →L[R] G
f : E →L[R] F
C : ProperCone R G
⊢ comap f (comap g C) = comap (g ∘SL f) C

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, LinearMap.restrictScalars, ContinuousLinearMap.restrictScalars, Set.Mem, setOf, ClosedSubmodule.comap, Submodule.comap, Set.preimage, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
inst_6 : AddCommMonoid F
inst_7 : TopologicalSpace F
inst_8 : Module R F
x : E
C : ProperCone R F
f : E →L[R] F
⊢ x ∈ comap f C ↔ Membership.mem (α := F) C ((f : (a : E) → F) x : F)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
F : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid F
inst_4 : TopologicalSpace F
inst_5 : Module R F
inst_6 : ContinuousAdd F
inst_7 : ContinuousConstSMul R F
C : ProperCone R F
⊢ map (ContinuousLinearMap.id R F) C = C

Tactic:
ClosedSubmodule.map_id _

Premises used: LinearMap.restrictScalars, ContinuousLinearMap.restrictScalars, ContinuousLinearMap.id, ClosedSubmodule.map_id
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
inst_6 : AddCommMonoid F
inst_7 : TopologicalSpace F
inst_8 : Module R F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul R F
f : E →L[R] F
C : ProperCone R E
⊢ (↑(map f C) : PointedCone R F) = (PointedCone.map (↑f : E →ₗ[R] F) (↑C : PointedCone R E)).closure

Tactic:
rfl

Premises used: Set.Mem, setOf, ConvexCone.toPointedCone, closure, Set.image, Submodule.topologicalClosure, AddSubmonoid.topologicalClosure, Set.sInter, PointedCone.closure, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
inst_6 : AddCommMonoid F
inst_7 : TopologicalSpace F
inst_8 : Module R F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul R F
f : E →L[R] F
C : ProperCone R E
y : F
⊢ y ∈ map f C ↔ y ∈ (PointedCone.map (↑f : E →ₗ[R] F) (↑C : PointedCone R E)).closure

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, closure, Set.image, Set.sInter
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
inst_6 : PartialOrder E
inst_7 : IsOrderedAddMonoid E
inst_8 : PosSMulMono R E
inst_9 : OrderClosedTopology E
x : E
⊢ Membership.mem (γ := ProperCone R E) (positive R E) x ↔ 0 ≤ x

Tactic:
.rfl

Premises used: Set.Ici, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
R : Type u_2
E : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module R E
inst_6 : PartialOrder E
inst_7 : IsOrderedAddMonoid E
inst_8 : PosSMulMono R E
inst_9 : OrderClosedTopology E
⊢ Eq (α := PointedCone R E) (↑(positive R E) : PointedCone R E) (PointedCone.positive R E)

Tactic:
rfl

Premises used: PointedCone.positive, ConvexCone.toPointedCone, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hC : (↑C : Set E).Nonempty
hSclos : IsClosed (↑C : Set E)
obtain : ∀ (x : E) (hx : x ∈ (↑C : Set E)), C.Pointed
⊢ C.Pointed

Tactic:
obtain ⟨x, hx⟩ := hC
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed (↑C : Set E)
x : E
hx : x ∈ (↑C : Set E)
f : 𝕜 → E := fun (x_1 : 𝕜) ↦ x_1 • x
w : 𝕜
h : Membership.mem (γ := Set 𝕜) (Ioi 0) w
⊢ f w ∈ (↑C : Set E)

Tactic:
C.smul_mem h hx

Premises used: Set.Mem, ConvexCone.smul_mem
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed (↑C : Set E)
x : E
hx : x ∈ (↑C : Set E)
f : 𝕜 → E := fun (x_1 : 𝕜) ↦ x_1 • x
w : 𝕜
h : Membership.mem (γ := Set 𝕜) (Ioi 0) w
⊢ f w ∈ (↑C : Set E)

Tactic:
exact C.smul_mem h hx

Premises used: ConvexCone.smul_mem
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed (↑C : Set E)
x : E
hx : x ∈ (↑C : Set E)
f : 𝕜 → E := fun (x_1 : 𝕜) ↦ x_1 • x
⊢ closure (f '' Ioi 0) ⊆ (↑C : Set E)

Tactic:
have hfS : closure (f '' Set.Ioi 0) ⊆ C :=
    hSclos.closure_subset_iff.2 <| by rintro _ ⟨_, h, rfl⟩; exact C.smul_mem h hx
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed (↑C : Set E)
x : E
hx : x ∈ (↑C : Set E)
f : 𝕜 → E := fun (x_1 : 𝕜) ↦ x_1 • x
hfS : closure (f '' Ioi 0) ⊆ (↑C : Set E)
⊢ ContinuousWithinAt f (Ioi 0) 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed (↑C : Set E)
x : E
hx : x ∈ (↑C : Set E)
f : 𝕜 → E := fun (x_1 : 𝕜) ↦ x_1 • x
hfS : closure (f '' Ioi 0) ⊆ (↑C : Set E)
⊢ ContinuousWithinAt f (Ioi 0) 0

Tactic:
have fc : ContinuousWithinAt f (Set.Ioi (0 : 𝕜)) 0 := by fun_prop
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed (↑C : Set E)
x : E
hx : x ∈ (↑C : Set E)
f : 𝕜 → E := fun (x_1 : 𝕜) ↦ x_1 • x
hfS : closure (f '' Ioi 0) ⊆ (↑C : Set E)
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ Membership.mem (γ := Set 𝕜) (closure (Ioi 0)) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed (↑C : Set E)
x : E
hx : x ∈ (↑C : Set E)
f : 𝕜 → E := fun (x_1 : 𝕜) ↦ x_1 • x
hfS : closure (f '' Ioi 0) ⊆ (↑C : Set E)
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ C.Pointed

Tactic:
simpa [f, Pointed, ← SetLike.mem_coe] using hfS <| fc.mem_closure_image <| by simp

Premises used: ContinuousWithinAt.mem_closure_image, SetLike.mem_coe, ConvexCone.Pointed
-- Module: Mathlib.Analysis.Convex.Cone.Closure
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
E : Type u_2
inst_2 : AddCommMonoid E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : SMul 𝕜 E
inst_6 : ContinuousConstSMul 𝕜 E
K : ConvexCone 𝕜 E
c : 𝕜
hc : 0 < c
x : E
h₁ : x ∈ closure (↑K : Set E)
⊢ Continuous (X := E) (HSMul.hSMul c)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.Cone.Closure
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
E : Type u_2
inst_2 : AddCommMonoid E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : SMul 𝕜 E
inst_6 : ContinuousConstSMul 𝕜 E
K : ConvexCone 𝕜 E
⊢ (↑K.closure : Set E) = closure (↑K : Set E)

Tactic:
rfl

Premises used: setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Closure
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
E : Type u_2
inst_2 : AddCommMonoid E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : SMul 𝕜 E
inst_6 : ContinuousConstSMul 𝕜 E
K : ConvexCone 𝕜 E
a : E
⊢ a ∈ K.closure ↔ a ∈ closure (↑K : Set E)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, closure, Set.sInter
-- Module: Mathlib.Analysis.Convex.Cone.Closure
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
E : Type u_2
inst_2 : AddCommMonoid E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : SMul 𝕜 E
inst_6 : ContinuousConstSMul 𝕜 E
K L : ConvexCone 𝕜 E
⊢ K.closure = L ↔ closure (↑K : Set E) = (↑L : Set E)

Tactic:
SetLike.ext'_iff

Premises used: setOf, closure, SetLike.ext'_iff, Set.sInter