awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ Disjoint C (hull 𝕜 s) ↔ Disjoint (↑C : Set M) s
have rw : Disjoint (hull 𝕜 s) C ↔ Disjoint (↑C : Set M) s
Tactic: rw [disjoint_comm, disjoint_hull_left_of_convex hs, disjoint_comm]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
rw : Disjoint (hull 𝕜 s) C ↔ Disjoint (↑C : Set M) s
⊢ Disjoint C (hull 𝕜 s) ↔ Disjoint (↑C : Set M) s
have rw₁ : Disjoint s (↑C : Set M) ↔ Disjoint (↑C : Set M) s
Tactic: rw [disjoint_comm, disjoint_hull_left_of_convex hs, disjoint_comm]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
rw : Disjoint (hull 𝕜 s) C ↔ Disjoint (↑C : Set M) s
rw₁ : Disjoint s (↑C : Set M) ↔ Disjoint (↑C : Set M) s
⊢ Disjoint C (hull 𝕜 s) ↔ Disjoint (↑C : Set M) s
have rw₂ : Disjoint (↑C : Set M) s ↔ Disjoint (↑C : Set M) s
Tactic: rw [disjoint_comm, disjoint_hull_left_of_convex hs, disjoint_comm]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ConvexCone 𝕜 M
have smul_mem' : ∀ ⦃c : 𝕜⦄,
  0 < c →
    ∀ ⦃x : M⦄,
      Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) x →
        Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) (c • x)
Tactic: apply ConvexCone.mk (⋃ (c : 𝕜) (_ : 0 < c), c • s)
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
smul_mem' :
  ∀ ⦃c : 𝕜⦄,
    0 < c →
      ∀ ⦃x : M⦄,
        Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) x →
          Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) (c • x)
⊢ ConvexCone 𝕜 M
have add_mem' : ∀ ⦃x : M⦄,
  Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) x →
    ∀ ⦃y : M⦄,
      Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) y →
        Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) (x + y)
Tactic: apply ConvexCone.mk (⋃ (c : 𝕜) (_ : 0 < c), c • s)
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃c : 𝕜⦄,
    0 < c →
      ∀ ⦃x : M⦄,
        Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) x →
          Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) (c • x)
have smul_mem' : ∀ ⦃c : 𝕜⦄,
  0 < c → ∀ ⦃x : M⦄, (∃ (i : 𝕜) (_ : 0 < i), ∃ y ∈ s, i • y = x) → ∃ (i : 𝕜) (_ : 0 < i), ∃ y ∈ s, i • y = c • x
Tactic: simp only [mem_iUnion, mem_smul_set]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃x : M⦄,
    Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) x →
      ∀ ⦃y : M⦄,
        Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) y →
          Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) (x + y)
have add_mem' : ∀ ⦃x : M⦄,
  (∃ (i : 𝕜) (_ : 0 < i), ∃ y ∈ s, i • y = x) →
    ∀ ⦃y : M⦄, (∃ (i : 𝕜) (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = y) → ∃ (i : 𝕜) (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = x + y
Tactic: simp only [mem_iUnion, mem_smul_set]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (hypothesis)
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
cx : 𝕜
cx_pos : 0 < cx
x : M
hx : x ∈ s
cy : 𝕜
cy_pos : 0 < cy
y : M
hy : y ∈ s
⊢ ∃ (i : 𝕜) (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = cx • x + cy • y
have this : 0 < cx + cy
Tactic: have : 0 < cx + cy := add_pos cx_pos cy_pos
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
cx : 𝕜
cx_pos : 0 < cx
x : M
hx : x ∈ s
cy : 𝕜
cy_pos : 0 < cy
y : M
hy : y ∈ s
this : 0 < cx + cy
⊢ ∃ (i : 𝕜) (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = cx • x + cy • y
have add_mem' : (cx + cy) • ((cx / (cx + cy)) • x + (cy / (cx + cy)) • y) = cx • x + cy • y
Tactic: refine ⟨_, this, _, convex_iff_div.1 hs hx hy cx_pos.le cy_pos.le this, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
⊢ x ∈ toCone s hs ↔ ∃ (c : 𝕜), 0 < c ∧ c • x ∈ s
have refine_1 : (∃ (c : 𝕜), 0 < c ∧ ∃ y ∈ s, c • y = x) → ∃ (c : 𝕜), 0 < c ∧ c • x ∈ s
Tactic: refine hs.mem_toCone.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
refine_1 : (∃ (c : 𝕜), 0 < c ∧ ∃ y ∈ s, c • y = x) → ∃ (c : 𝕜), 0 < c ∧ c • x ∈ s
⊢ x ∈ toCone s hs ↔ ∃ (c : 𝕜), 0 < c ∧ c • x ∈ s
have refine_2 : (∃ (c : 𝕜), 0 < c ∧ c • x ∈ s) → ∃ (c : 𝕜), 0 < c ∧ ∃ y ∈ s, c • y = x
Tactic: refine hs.mem_toCone.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
c : 𝕜
hc : 0 < c
y : M
hy : y ∈ s
⊢ c⁻¹ • c • y ∈ s
have rwa : (c⁻¹ * c) • y ∈ s
Tactic: rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
c : 𝕜
hc : 0 < c
y : M
hy : y ∈ s
rwa : (c⁻¹ * c) • y ∈ s
⊢ c⁻¹ • c • y ∈ s
have rwa₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 y ∈ s
Tactic: rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
⊢ c⁻¹ • c • x = x
have rw : (c⁻¹ * c) • x = x
Tactic: rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
rw : (c⁻¹ * c) • x = x
⊢ c⁻¹ • c • x = x
have rw₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 x = x
Tactic: rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
rw : (c⁻¹ * c) • x = x
rw₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 x = x
⊢ c⁻¹ • c • x = x
have rw₂ : x = x
Tactic: rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ IsLeast {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} (toCone s hs)
have refine : ∀ (t : ConvexCone 𝕜 M) (ht : Membership.mem (γ := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} t)
  (x : M) (hx : x ∈ toCone s hs), x ∈ t
Tactic: refine ⟨hs.subset_toCone, fun t ht x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
t : ConvexCone 𝕜 M
ht : Membership.mem (γ := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} t
x : M
hx : x ∈ toCone s hs
⊢ x ∈ t
have rcases : ∀ (c : 𝕜) (hc : 0 < c) (y : M) (hy : y ∈ s) (hx : c • y ∈ toCone s hs), c • y ∈ t
Tactic: rcases hs.mem_toCone.1 hx with ⟨c, hc, y, hy, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
⊢ IsLeast (α := ConvexCone 𝕜 M) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)}
    (Convex.toCone ((convexHull 𝕜 : (a : Set M) → Set M) s) ⋯)
have h : Eq.{u_4 + 1} (α := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)}
  {t : ConvexCone 𝕜 M | (convexHull 𝕜 : (a : Set M) → Set M) s ⊆ (↑t : Set M)}
Tactic: convert! (convex_convexHull 𝕜 s).toCone_isLeast using 1
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
⊢ Eq.{u_4 + 1} (α := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)}
    {t : ConvexCone 𝕜 M | (convexHull 𝕜 : (a : Set M) → Set M) s ⊆ (↑t : Set M)}
have h : ∀ (t : ConvexCone 𝕜 M),
  Membership.mem (γ := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} t ↔
    Membership.mem (γ := Set (ConvexCone 𝕜 M))
      {t : ConvexCone 𝕜 M | (convexHull 𝕜 : (a : Set M) → Set M) s ⊆ (↑t : Set M)} t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
hC : DualFG p C
⊢ ∃ (D : PointedCone R M), Submodule.FG D ∧ dual p (↑D : Set M) = C
have obtain : ∀ (s : Finset M) (hs : dual p (↑s : Set M) = C), ∃ (D : PointedCone R M), Submodule.FG D ∧ dual p (↑D : Set M) = C
Tactic: obtain ⟨s, hs⟩ := hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
⊢ DualFG p (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))
have h : Eq (α := PointedCone R N) (dual p (↑s : Set M)) (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))
Tactic: use s
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
hC : DualFG p C
⊢ DualFG (M := N →ₗ[R] R) LinearMap.id C
have obtain : ∀ (s : Finset M), DualFG (M := N →ₗ[R] R) LinearMap.id (dual p (↑s : Set M))
Tactic: obtain ⟨s, rfl⟩ := hC
Cleared hypotheses: C, hC
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
⊢ DualFG (M := N →ₗ[R] R) LinearMap.id (dual p (↑s : Set M))
have h : Eq (α := PointedCone R N) (dual LinearMap.id (↑(Finset.image (⇑p : (a : M) → N →ₗ[R] R) s) : Set (N →ₗ[R] R)))
  (dual p (↑s : Set M))
Tactic: use Finset.image p s
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
hC : DualFG p C
⊢ DualFG (M := N →ₗ[R] R) LinearMap.id C
have obtain : ∀ (s : Finset M), DualFG (M := N →ₗ[R] R) LinearMap.id (dual p (↑s : Set M))
Tactic: classical
  obtain ⟨s, rfl⟩ := hC
  use Finset.image p s
  simp
Cleared hypotheses: C, hC
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
hC : DualFG p C
obtain : ∀ (s : Finset M), DualFG (M := N →ₗ[R] R) LinearMap.id (dual p (↑s : Set M))
⊢ DualFG (M := N →ₗ[R] R) LinearMap.id C
have h : ∀ (s : Finset M),
  Eq (α := PointedCone R N) (dual LinearMap.id (↑(Finset.image (⇑p : (a : M) → N →ₗ[R] R) s) : Set (N →ₗ[R] R)))
    (dual p (↑s : Set M))
Tactic: classical
  obtain ⟨s, rfl⟩ := hC
  use Finset.image p s
  simp
Cleared hypotheses: C, hC
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s w : Finset M
⊢ DualFG p (dual p (↑s : Set M))
have h : Eq (α := PointedCone R N) (dual p (↑s : Set M)) (dual p (↑s : Set M))
Tactic: use s
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hs : s.Finite
⊢ DualFG p (dual p s)
have h : Eq (α := PointedCone R N) (dual p (↑(hs.toFinset (s := s)) : Set M)) (dual p s)
Tactic: use hs.toFinset
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hs : s.Finite
⊢ Eq (α := PointedCone R N) (dual p (↑(hs.toFinset (s := s)) : Set M)) (dual p s)
have h : Eq (α := PointedCone R N) (dual p s) (dual p s)
Tactic: rw [Set.Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R M
hC : Submodule.FG C
⊢ DualFG p (dual p (↑C : Set M))
have obtain : ∀ (s : Finset M), DualFG p (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))
Tactic: obtain ⟨s, rfl⟩ := hC
Cleared hypotheses: C, hC
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
⊢ Eq (α := PointedCone R N) (dual p (↑s : Set M)) (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))
have h : Eq (α := PointedCone R N) (dual p (↑(hull R (↑s : Set M)) : Set M))
  (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))
Tactic: rw [← dual_hull]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C D : PointedCone R N
hC : DualFG p C
hD : DualFG p D
⊢ DualFG p (C ⊓ D)
have obtain : ∀ (S : Finset M), DualFG p (dual p (↑S : Set M) ⊓ D)
Tactic: obtain ⟨S, rfl⟩ := hC
Cleared hypotheses: C, hC
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
D : PointedCone R N
hD : DualFG p D
S : Finset M
⊢ DualFG p (dual p (↑S : Set M) ⊓ D)
have obtain : ∀ (T : Finset M), DualFG p (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
Tactic: obtain ⟨T, rfl⟩ := hD
Cleared hypotheses: D, hD
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
S T : Finset M
⊢ DualFG p (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
have h : Eq (α := PointedCone R N) (dual p (↑(S ∪ T) : Set M)) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
Tactic: use S ∪ T
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
S T : Finset M
⊢ Eq (α := PointedCone R N) (dual p (↑(S ∪ T) : Set M)) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
have h : Eq (α := PointedCone R N) (dual p ((↑S : Set M) ∪ (↑T : Set M))) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
Tactic: rw [Finset.coe_union, dual_union]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
S T : Finset M
h : Eq (α := PointedCone R N) (dual p ((↑S : Set M) ∪ (↑T : Set M))) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
⊢ Eq (α := PointedCone R N) (dual p (↑(S ∪ T) : Set M)) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
have h₁ : Eq (α := PointedCone R N) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M)) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
Tactic: rw [Finset.coe_union, dual_union]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C D : PointedCone R N
hC : DualFG p C
hD : DualFG p D
⊢ DualFG p (C ⊓ D)
have obtain : ∀ (S : Finset M), DualFG p (dual p (↑S : Set M) ⊓ D)
Tactic: classical
  obtain ⟨S, rfl⟩ := hC; obtain ⟨T, rfl⟩ := hD
  use S ∪ T; rw [Finset.coe_union, dual_union]
Cleared hypotheses: C, hC
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C D : PointedCone R N
hC : DualFG p C
hD : DualFG p D
obtain obtain₁ : ∀ (S : Finset M), DualFG p (dual p (↑S : Set M) ⊓ D)
⊢ DualFG p (C ⊓ D)
have obtain₂ : ∀ (S T : Finset M), DualFG p (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
Tactic: classical
  obtain ⟨S, rfl⟩ := hC; obtain ⟨T, rfl⟩ := hD
  use S ∪ T; rw [Finset.coe_union, dual_union]
Cleared hypotheses: C, D, hC, hD
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C D : PointedCone R N
hC : DualFG p C
hD : DualFG p D
obtain obtain₁ : ∀ (S : Finset M), DualFG p (dual p (↑S : Set M) ⊓ D)
obtain₂ : ∀ (S T : Finset M), DualFG p (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
⊢ DualFG p (C ⊓ D)
have h : ∀ (S T : Finset M), Eq (α := PointedCone R N) (dual p (↑(S ∪ T) : Set M)) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
Tactic: classical
  obtain ⟨S, rfl⟩ := hC; obtain ⟨T, rfl⟩ := hD
  use S ∪ T; rw [Finset.coe_union, dual_union]
Cleared hypotheses: C, D, hC, hD
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.DualFinite (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
hC : DualFG p C
⊢ dual p (↑(dual p.flip (↑C : Set N)) : Set M) = C
have obtain : ∀ (D : PointedCone R M) (hDualFG : Submodule.FG D) (hC : DualFG p (dual p (↑D : Set M))),
  Eq (α := PointedCone R N) (dual p (↑(dual p.flip (↑(dual p (↑D : Set M)) : Set N)) : Set M)) (dual p (↑D : Set M))
Tactic: obtain ⟨D, hDualFG, rfl⟩ := exists_fg_dual hC
Cleared hypotheses: C, hC
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set (Submodule R E)
⊢ Eq.{u_2 + 1} (α := PointedCone R E) (↑(⨅ S ∈ s, S) : PointedCone R E) (⨅ S ∈ s, (↑S : PointedCone R E))
have rw : Eq (α := PointedCone R E) (↑(sInf s) : PointedCone R E) (⨅ S ∈ s, (↑S : PointedCone R E))
Tactic: rw [← sInf_eq_iInf, ofSubmodule_sInf, sInf_eq_iInf, iInf_image]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set (Submodule R E)
rw : Eq (α := PointedCone R E) (↑(sInf s) : PointedCone R E) (⨅ S ∈ s, (↑S : PointedCone R E))
⊢ Eq.{u_2 + 1} (α := PointedCone R E) (↑(⨅ S ∈ s, S) : PointedCone R E) (⨅ S ∈ s, (↑S : PointedCone R E))
have rw₁ : Eq (α := PointedCone R E) (sInf (ofSubmodule '' s)) (⨅ S ∈ s, (↑S : PointedCone R E))
Tactic: rw [← sInf_eq_iInf, ofSubmodule_sInf, sInf_eq_iInf, iInf_image]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set (Submodule R E)
rw : Eq (α := PointedCone R E) (↑(sInf s) : PointedCone R E) (⨅ S ∈ s, (↑S : PointedCone R E))
rw₁ : Eq (α := PointedCone R E) (sInf (ofSubmodule '' s)) (⨅ S ∈ s, (↑S : PointedCone R E))
⊢ Eq.{u_2 + 1} (α := PointedCone R E) (↑(⨅ S ∈ s, S) : PointedCone R E) (⨅ S ∈ s, (↑S : PointedCone R E))
have rw₂ : Eq.{u_2 + 1} (α := PointedCone R E)
  (⨅ (a : PointedCone R E), ⨅ (_ : Membership.mem (γ := Set (PointedCone R E)) (ofSubmodule '' s) a), a)
  (⨅ S ∈ s, (↑S : PointedCone R E))
Tactic: rw [← sInf_eq_iInf, ofSubmodule_sInf, sInf_eq_iInf, iInf_image]