awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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))
⊢ 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) (⨅ b ∈ s, (↑b : 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)
⊢ 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) (↑(sSup s) : PointedCone R E) (⨆ S ∈ s, (↑S : PointedCone R E))
Tactic: rw [← sSup_eq_iSup, ofSubmodule_sSup, sSup_eq_iSup, iSup_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) (↑(sSup 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) (sSup (ofSubmodule '' s)) (⨆ S ∈ s, (↑S : PointedCone R E))
Tactic: rw [← sSup_eq_iSup, ofSubmodule_sSup, sSup_eq_iSup, iSup_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) (↑(sSup s) : PointedCone R E) (⨆ S ∈ s, (↑S : PointedCone R E))
rw₁ : Eq (α := PointedCone R E) (sSup (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 [← sSup_eq_iSup, ofSubmodule_sSup, sSup_eq_iSup, iSup_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) (↑(sSup s) : PointedCone R E) (⨆ S ∈ s, (↑S : PointedCone R E))
rw₁ : Eq (α := PointedCone R E) (sSup (ofSubmodule '' s)) (⨆ S ∈ s, (↑S : PointedCone R E))
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))
⊢ 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) (⨆ b ∈ s, (↑b : PointedCone R E)) (⨆ S ∈ s, (↑S : PointedCone R E))
Tactic: rw [← sSup_eq_iSup, ofSubmodule_sSup, sSup_eq_iSup, iSup_image]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : C.Pointed
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
⊢ Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C
have inl : ∀ (hzero : 0 = c), Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C
Tactic: rcases eq_or_lt_of_le hc with hzero | hpos
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : C.Pointed
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
inl : ∀ (hzero : 0 = c), Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C
⊢ Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C
have inr : ∀ (hpos : 0 < c), Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C
Tactic: rcases eq_or_lt_of_le hc with hzero | hpos
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : 0 ∈ C
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hzero : 0 = c
⊢ Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C
have h : Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x = 0
Tactic: convert! hC
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : C.Pointed
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C
have inr : 0 < (↑(Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc) : R)
Tactic: apply ConvexCone.smul_mem
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : C.Pointed
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hpos : 0 < c
inr : 0 < (↑(Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc) : R)
⊢ Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C
have inr₁ : x ∈ C
Tactic: apply ConvexCone.smul_mem
-- 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
x : E
s : Set E
⊢ Membership.mem (γ := PointedCone R E) (hull R s) x ↔
    ∃ (c : E →₀ R),
      (↑c.support : Set E) ⊆ s ∧
        (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x
have rw : (∃ (c : Finsupp.{u_2, u_1} E R≥0), (↑c.support : Set E) ⊆ s ∧ (c.sum fun (mi : E) (r : R≥0) ↦ r • mi) = x) ↔
  ∃ (c : E →₀ R),
    (↑c.support : Set E) ⊆ s ∧
      (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x
Tactic: rw [mem_span_set]
-- 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
x : E
s : Set E
⊢ (∃ (c : Finsupp.{u_2, u_1} E R≥0), (↑c.support : Set E) ⊆ s ∧ (c.sum fun (mi : E) (r : R≥0) ↦ r • mi) = x) ↔
    ∃ (c : E →₀ R),
      (↑c.support : Set E) ⊆ s ∧
        (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x
have mp : (∃ (c : Finsupp.{u_2, u_1} E R≥0), (↑c.support : Set E) ⊆ s ∧ (c.sum fun (mi : E) (r : R≥0) ↦ r • mi) = x) →
  ∃ (c : E →₀ R),
    (↑c.support : Set E) ⊆ s ∧
      (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x
Tactic: constructor
-- 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
x : E
s : Set E
mp :
  (∃ (c : Finsupp.{u_2, u_1} E R≥0), (↑c.support : Set E) ⊆ s ∧ (c.sum fun (mi : E) (r : R≥0) ↦ r • mi) = x) →
    ∃ (c : E →₀ R),
      (↑c.support : Set E) ⊆ s ∧
        (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x
⊢ (∃ (c : Finsupp.{u_2, u_1} E R≥0), (↑c.support : Set E) ⊆ s ∧ (c.sum fun (mi : E) (r : R≥0) ↦ r • mi) = x) ↔
    ∃ (c : E →₀ R),
      (↑c.support : Set E) ⊆ s ∧
        (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x
have mpr : (∃ (c : E →₀ R),
    (↑c.support : Set E) ⊆ s ∧
      (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x) →
  ∃ (c : Finsupp.{u_2, u_1} E R≥0), (↑c.support : Set E) ⊆ s ∧ (c.sum fun (mi : E) (r : R≥0) ↦ r • mi) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup E
inst_4 : Module R E
C : PointedCone R E
r : R
x : E
hx : x ∈ C.support.carrier
⊢ r • x ∈ C.support.carrier
have pos : ∀ (hr : 0 ≤ r), r • x ∈ C.support.carrier
Tactic: by_cases hr : 0 ≤ r
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup E
inst_4 : Module R E
C : PointedCone R E
r : R
x : E
hx : x ∈ C.support.carrier
pos : ∀ (hr : 0 ≤ r), r • x ∈ C.support.carrier
⊢ r • x ∈ C.support.carrier
have neg : ∀ (hr : ¬0 ≤ r), r • x ∈ C.support.carrier
Tactic: by_cases hr : 0 ≤ r
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (hypothesis)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup E
inst_4 : Module R E
C : PointedCone R E
r : R
x : E
hx : x ∈ C.support.carrier
hr : ¬0 ≤ r
⊢ r • x ∈ C.support.carrier
have hr₁ : 0 ≤ -r
Tactic: have hr := le_of_lt <| neg_pos_of_neg <| lt_of_not_ge hr
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup E
inst_4 : Module R E
C : PointedCone R E
⊢ C.lineal = sSup {S : Submodule R E | (↑S : PointedCone R E) ≤ C}
have simp_rw : C.lineal = sSup {S : Submodule R E | S ≤ C.lineal}
Tactic: simp_rw [gc_ofSubmodule_lineal.le_iff_le, Set.Iic_def, csSup_Iic]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Pointed (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup E
inst_4 : Module R E
C : PointedCone R E
simp_rw : C.lineal = sSup {S : Submodule R E | S ≤ C.lineal}
⊢ C.lineal = sSup {S : Submodule R E | (↑S : PointedCone R E) ≤ C}
have simp_rw₁ : C.lineal = sSup (Set.Iic C.lineal)
Tactic: simp_rw [gc_ofSubmodule_lineal.le_iff_le, Set.Iic_def, csSup_Iic]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.TensorProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
x : G
y : H
C₁ : PointedCone R G
C₂ : PointedCone R H
hx : x ∈ C₁
hy : y ∈ C₂
⊢ Membership.mem (γ := PointedCone R (G ⊗[R] H)) (C₁.maxTensorProduct C₂ : PointedCone R (G ⊗[R] H)) (x ⊗ₜ[R] y)
have simp : ∀ (φ : Dual R G),
  Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ →
    ∀ (ψ : Dual R H),
      Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ →
        0 ≤ HMul.hMul (α := R) (β := R) ((φ : (a : G) → R) x : R) ((ψ : (a : H) → R) y : R)
Tactic: simp only [mem_maxTensorProduct, dualDistrib_apply]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.TensorProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
⊢ Eq (α := PointedCone R (H ⊗[R] G))
    (map (↑(TensorProduct.comm R G H) : G ⊗[R] H →ₗ[R] H ⊗[R] G) (C₁.maxTensorProduct C₂) : PointedCone R (H ⊗[R] G))
    (C₂.maxTensorProduct C₁ : PointedCone R (H ⊗[R] G))
have h : ∀ (z : H ⊗[R] G),
  Membership.mem (γ := PointedCone R (H ⊗[R] G))
      (map (↑(TensorProduct.comm R G H) : G ⊗[R] H →ₗ[R] H ⊗[R] G) (C₁.maxTensorProduct C₂) : PointedCone R (H ⊗[R] G))
      z ↔
    Membership.mem (γ := PointedCone R (H ⊗[R] G)) (C₂.maxTensorProduct C₁ : PointedCone R (H ⊗[R] G)) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.TensorProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
z : H ⊗[R] G
⊢ Membership.mem (γ := PointedCone R (H ⊗[R] G))
      (map (↑(TensorProduct.comm R G H) : G ⊗[R] H →ₗ[R] H ⊗[R] G) (C₁.maxTensorProduct C₂) : PointedCone R (H ⊗[R] G))
      z ↔
    Membership.mem (γ := PointedCone R (H ⊗[R] G)) (C₂.maxTensorProduct C₁ : PointedCone R (H ⊗[R] G)) z
have h : (∃ (x : G ⊗[R] H),
    (∀ (φ : Dual R G),
        Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ →
          ∀ (ψ : Dual R H),
            Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ →
              LE.le.{u_1} (α := R) (0 : R)
                ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) (φ ⊗ₜ[R] ψ) :
                        Dual R (G ⊗[R] H)) :
                      (a : G ⊗[R] H) → R)
                    x :
                  R)) ∧
      ((↑(TensorProduct.comm R G H) : G ⊗[R] H →ₗ[R] H ⊗[R] G) : (a : G ⊗[R] H) → H ⊗[R] G) x = z) ↔
  ∀ (φ : Dual R H),
    Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) φ →
      ∀ (ψ : Dual R G),
        Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) ψ →
          LE.le.{u_1} (α := R) (0 : R)
            ((((dualDistrib R H G : (a : Dual R H ⊗[R] Dual R G) → Dual R (H ⊗[R] G)) (φ ⊗ₜ[R] ψ) : Dual R (H ⊗[R] G)) :
                  (a : H ⊗[R] G) → R)
                z :
              R)
Tactic: simp only [mem_map, mem_maxTensorProduct]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.TensorProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
z : H ⊗[R] G
⊢ (∃ (x : G ⊗[R] H),
      (∀ (φ : Dual R G),
          Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ →
            ∀ (ψ : Dual R H),
              Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ →
                LE.le.{u_1} (α := R) (0 : R)
                  ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) (φ ⊗ₜ[R] ψ) :
                          Dual R (G ⊗[R] H)) :
                        (a : G ⊗[R] H) → R)
                      x :
                    R)) ∧
        ((↑(TensorProduct.comm R G H) : G ⊗[R] H →ₗ[R] H ⊗[R] G) : (a : G ⊗[R] H) → H ⊗[R] G) x = z) ↔
    ∀ (φ : Dual R H),
      Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) φ →
        ∀ (ψ : Dual R G),
          Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) ψ →
            LE.le.{u_1} (α := R) (0 : R)
              ((((dualDistrib R H G : (a : Dual R H ⊗[R] Dual R G) → Dual R (H ⊗[R] G)) (φ ⊗ₜ[R] ψ) :
                      Dual R (H ⊗[R] G)) :
                    (a : H ⊗[R] G) → R)
                  z :
                R)
have h : (∃ (x : G ⊗[R] H),
    (∀ (φ : Dual R G),
        Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ →
          ∀ (ψ : Dual R H),
            Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ →
              LE.le.{u_1} (α := R) (0 : R)
                ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) (φ ⊗ₜ[R] ψ) :
                        Dual R (G ⊗[R] H)) :
                      (a : G ⊗[R] H) → R)
                    x :
                  R)) ∧
      ((↑(TensorProduct.comm R G H) : G ⊗[R] H →ₗ[R] H ⊗[R] G) : (a : G ⊗[R] H) → H ⊗[R] G) x = z) →
  ∀ (φ : Dual R H),
    Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) φ →
      ∀ (ψ : Dual R G),
        Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) ψ →
          LE.le.{u_1} (α := R) (0 : R)
            ((((dualDistrib R H G : (a : Dual R H ⊗[R] Dual R G) → Dual R (H ⊗[R] G)) (φ ⊗ₜ[R] ψ) : Dual R (H ⊗[R] G)) :
                  (a : H ⊗[R] G) → R)
                z :
              R)
Tactic: refine ⟨?_, fun hz ↦
    ⟨(TensorProduct.comm R H G) z, ?_, (TensorProduct.comm R H G).symm_apply_apply z⟩⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.TensorProduct (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
G' : Type u_4
H' : Type u_5
inst_7 : AddCommGroup G'
inst_8 : Module R G'
inst_9 : AddCommGroup H'
inst_10 : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw :
  ∀ (φ : Dual R G),
    Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ →
      ∀ (ψ : Dual R H),
        Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ →
          LE.le.{u_1} (α := R) (0 : R)
            ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) (φ ⊗ₜ[R] ψ) : Dual R (G ⊗[R] H)) :
                  (a : G ⊗[R] H) → R)
                w :
              R)
φ : Dual R G'
hφ : Membership.mem (γ := PointedCone R (Dual R G')) (dual (Dual.eval R G') (↑(map f C₁) : Set G')) φ
ψ : Dual R H'
hψ : Membership.mem (γ := PointedCone R (Dual R H')) (dual (Dual.eval R H') (↑(map g C₂) : Set H')) ψ
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((((dualDistrib R G' H' : (a : Dual R G' ⊗[R] Dual R H') → Dual R (G' ⊗[R] H')) (φ ⊗ₜ[R] ψ) : Dual R (G' ⊗[R] H')) :
          (a : G' ⊗[R] H') → R)
        (((↑{ c : R // 0 ≤ c } :
                  {S : Type u_1} →
                    {M : Type (max u_3 u_2)} →
                      {M₂ : Type (max u_5 u_4)} →
                        [inst_11 : Semiring { c : R // 0 ≤ c }] →
                          [inst_12 : Semiring S] →
                            [inst_13 : AddCommMonoid M] →
                              [inst_14 : AddCommMonoid M₂] →
                                [inst_15 : Module { c : R // 0 ≤ c } M] →
                                  [inst_16 : Module { c : R // 0 ≤ c } M₂] →
                                    [inst_17 : Module S M] →
                                      [inst_18 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ { c : R // 0 ≤ c } S] →
                                          (fₗ : M →ₗ[S] M₂) → M →ₗ[{ c : R // 0 ≤ c }] M₂)
                (TensorProduct.map f g) :
              (a : G ⊗[R] H) → G' ⊗[R] H')
            w :
          G' ⊗[R] H') :
      R)
have h_eq : Eq (α := G ⊗[R] H →ₗ[R] R)
  ((dualDistrib R G' H' : (a : Dual R G' ⊗[R] Dual R H') → Dual R (G' ⊗[R] H')) (φ ⊗ₜ[R] ψ) ∘ₗ TensorProduct.map f g)
  ((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g)))
Tactic: have h_eq : ((dualDistrib R G' H') (φ ⊗ₜ[R] ψ)).comp (TensorProduct.map f g) =
      ((dualDistrib R G H) ((φ.comp f) ⊗ₜ[R] (ψ.comp g))) :=
    TensorProduct.ext' fun x y ↦ by simp [map_tmul]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
x : P
⊢ convexCombination.{u_1, u_2, u_3} (R := R) (StdSimplex.single x) = x
have simp : (Finset.affineCombination R (Finsupp.support.{u_3, u_1} (M := R) (Finsupp.single x 1)) id : (a : P → R) → P)
    (⇑(Finsupp.single x 1) : (a : P) → R) =
  x
Tactic: simp only [convexCombination, StdSimplex.single]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
x : P
⊢ (Finset.affineCombination R (Finsupp.support.{u_3, u_1} (M := R) (Finsupp.single x 1)) id : (a : P → R) → P)
      (⇑(Finsupp.single x 1) : (a : P) → R) =
    x
have rw : (Finset.affineCombination R {x} id : (a : P → R) → P) (⇑(Finsupp.single x 1) : (a : P) → R) = x
Tactic: rw [Finsupp.support_single _ one_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
⊢ convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join
have obtain : ∀ (b : P), convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join
Tactic: obtain ⟨b⟩ : Nonempty P := inferInstance
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
⊢ convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join
have hL : (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id : (a : P → R) → P)
    (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
    (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
        (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
      V)
    b
Tactic: have hL := Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
    (f.map convexCombination).weights.support (f.map convexCombination).weights id
    (f.map convexCombination).total b
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id : (a : P → R) → P)
      (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
          (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
        V)
      b
⊢ convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join
have hR : (Finset.affineCombination R f.join.weights.support id : (a : P → R) → P) (⇑f.join.weights : (a : P) → R) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
    ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V) b
Tactic: have hR := Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
    f.join.weights.support f.join.weights id f.join.total b