awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →ₗ[R] F
C : PointedCone R E
y : F
⊢ y ∈ map f C ↔ ∃ x ∈ C, (f : (a : E) → F) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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
inst_5 : AddCommMonoid F
inst_6 : Module R F
inst_7 : AddCommMonoid G
inst_8 : Module R G
g : F →ₗ[R] G
f : E →ₗ[R] F
C : PointedCone R E
⊢ map g (map f C) = map (g ∘ₗ f) C

Tactic:
SetLike.coe_injective <| Set.image_image g f C

Premises used: Set.image_image, SetLike.coe_injective, SetLike.coe, DFunLike.coe
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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
C : PointedCone R E
⊢ map LinearMap.id C = C

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →ₗ[R] F
C : PointedCone 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.Geometry.Convex.Cone.Pointed
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
C : PointedCone R E
⊢ comap LinearMap.id C = C

Tactic:
rfl

Premises used: Set.Mem, setOf, PointedCone.comap, Submodule.comap, Set.preimage, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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
inst_5 : AddCommMonoid F
inst_6 : Module R F
inst_7 : AddCommMonoid G
inst_8 : Module R G
g : F →ₗ[R] G
f : E →ₗ[R] F
C : PointedCone R G
⊢ comap f (comap g C) = comap (g ∘ₗ f) C

Tactic:
rfl

Premises used: LinearMap.restrictScalars, Set.Mem, setOf, PointedCone.comap, Submodule.comap, Set.preimage, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →ₗ[R] F
C : PointedCone R F
x : E
⊢ x ∈ comap f C ↔ Membership.mem (α := F) C ((f : (a : E) → F) x : F)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module R E
inst_7 : PosSMulMono R E
x : E
⊢ Membership.mem (γ := PointedCone R E) (positive R E) x ↔ 0 ≤ x

Tactic:
Iff.rfl

Premises used: Set.Ici, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module R E
inst_7 : PosSMulMono R E
⊢ Eq (α := ConvexCone R E) (↑(positive R E) : ConvexCone R E) (ConvexCone.positive R E)

Tactic:
rfl

Premises used: Set.Ici, setOf, ConvexCone.positive, rfl, PointedCone.toConvexCone
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
E : Type u_2
R : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup E
inst_4 : Module R E
C D : PointedCone R E
S : Submodule R E
hCS : C ≤ (↑S : PointedCone R E)
⊢ -C ≤ (↑S : PointedCone R E)

Tactic:
simpa [Submodule.neg_le]

Premises used: Submodule.neg_le
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
E : Type u_2
R : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup E
inst_4 : Module R E
C D : PointedCone R E
S : Submodule R E
hSC : (↑S : PointedCone R E) ≤ C
⊢ -(↑S : PointedCone R E) ≤ C

Tactic:
simpa [Submodule.neg_le]

Premises used: Submodule.neg_le
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module R E
C : PointedCone R E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ C
⊢ ∀ (a : R), 0 ≤ a → ∀ (b : E), 0 ≤ b → 0 ≤ a • b

Tactic:
simp +contextual [h, C.smul_mem]

Premises used: PointedCone.smul_mem
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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
neg : ∀ (hr : ¬0 ≤ r), r • x ∈ C.support.carrier
⊢ r • x ∈ C.support.carrier

Tactic:
by_cases hr : 0 ≤ r
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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

Tactic:
simpa using And.intro (C.smul_mem hr hx.1) (C.smul_mem hr hx.2)

Premises used: And.right, And.left, And.intro, PointedCone.smul_mem
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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
⊢ 0 ≤ -r

Tactic:
have hr := le_of_lt <| neg_pos_of_neg <| lt_of_not_ge hr
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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_1 : ¬0 ≤ r
hr : 0 ≤ -r
⊢ r • x ∈ C.support.carrier

Tactic:
simpa using And.intro (C.smul_mem hr hx.2) (C.smul_mem hr hx.1)

Premises used: And.right, And.left, And.intro, PointedCone.smul_mem
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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 : PointedCone R E) = C ⊓ -C

Tactic:
rfl

Premises used: Set.Mem, Submodule.restrictScalars, setOf, Set.inter, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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
x : E
⊢ x ∈ C.lineal ↔ x ∈ C ∧ -x ∈ C

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, Set.preimage
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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.support = C.lineal.toAddSubgroup

Tactic:
rfl

Premises used: AddSubmonoid.support, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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
x : Submodule R E
x_1 : PointedCone R E
h : (↑x : PointedCone R E) ≤ x_1
x_2 : E
⊢ x_2 ∈ x → x_2 ∈ x_1.lineal

Tactic:
aesop
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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 : PointedCone R E) ≤ C

Tactic:
gc_ofSubmodule_lineal.l_u_le C

Premises used: PointedCone.gc_ofSubmodule_lineal, GaloisConnection.l_u_le
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
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}
simp_rw₁ : C.lineal = sSup (Set.Iic C.lineal)
⊢ C.lineal = sSup {S : Submodule R E | (↑S : PointedCone R E) ≤ C}

Tactic:
simp_rw [gc_ofSubmodule_lineal.le_iff_le, Set.Iic_def, csSup_Iic]

Premises used: GaloisConnection.le_iff_le, PointedCone.gc_ofSubmodule_lineal, csSup_Iic, Set.Iic_def
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup E
inst_4 : Module R E
C : PointedCone R E
⊢ (↑C : ConvexCone R E).Salient ↔ (↑C : Set E) ∩ -(↑C : Set E) = {0}

Tactic:
simp [ConvexCone.Salient, Set.eq_singleton_iff_unique_mem, not_imp_not]

Premises used: ConvexCone.Salient, Set.eq_singleton_iff_unique_mem, not_imp_not
-- Module: Mathlib.Geometry.Convex.Cone.Simplicial
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
s : Set M
hs : s.Finite
hli : LinearIndepOn R id s
⊢ IsSimplicial (hull R s)

Tactic:
⟨s, hs, hli, rfl⟩

Premises used: PointedCone.IsSimplicial, And.intro, Exists.intro, rfl
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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 : G ⊗[R] H
⊢ Membership.mem (γ := PointedCone R (G ⊗[R] H)) (C₁.maxTensorProduct C₂ : PointedCone R (G ⊗[R] H)) z ↔
    ∀ (φ : 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)
                  z :
                R)

Tactic:
simp only [maxTensorProduct, minTensorProduct, dual_hull, mem_dual, Set.forall_mem_image2,
    SetLike.mem_coe, mem_dual]

Premises used: Set.forall_mem_image2, PointedCone.dual_hull, PointedCone.minTensorProduct, PointedCone.mem_dual, SetLike.mem_coe, PointedCone.maxTensorProduct
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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₂
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)
⊢ Membership.mem (γ := PointedCone R (G ⊗[R] H)) (C₁.maxTensorProduct C₂ : PointedCone R (G ⊗[R] H)) (x ⊗ₜ[R] y)

Tactic:
simp only [mem_maxTensorProduct, dualDistrib_apply]

Premises used: TensorProduct.dualDistrib_apply, PointedCone.mem_maxTensorProduct
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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₂
⊢ ∀ (φ : 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:
fun φ hφ ψ hψ => mul_nonneg (hφ hx) (hψ hy)

Premises used: mul_nonneg
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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₂
⊢ ∀ (φ : 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:
exact fun φ hφ ψ hψ => mul_nonneg (hφ hx) (hψ hy)

Premises used: mul_nonneg
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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₁.minTensorProduct C₂ : PointedCone R (G ⊗[R] H)) (x ⊗ₜ[R] y)

Tactic:
Submodule.subset_span (Set.mem_image2_of_mem hx hy)

Premises used: Set.Mem, Set.mem_image2_of_mem, Submodule.subset_span
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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
⊢ Set.image2 (fun (x1 : G) (x2 : H) ↦ x1 ⊗ₜ[R] x2) (↑C₁ : Set G) (↑C₂ : Set H) ⊆
    (↑(C₁.maxTensorProduct C₂ : PointedCone R (G ⊗[R] H)) : Set (G ⊗[R] H))

Tactic:
fun _ ⟨_, hx, _, hy, hz⟩ => hz ▸ tmul_mem_maxTensorProduct hx hy

Premises used: PointedCone.tmul_mem_maxTensorProduct, Membership.mem, Eq.rec, Set.Subset, SetLike.coe, PointedCone.maxTensorProduct, _private.0.PointedCone.tmul_subset_maxTensorProduct.match_1
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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
⊢ Set.image2 (fun (x1 : G) (x2 : H) ↦ x1 ⊗ₜ[R] x2) (↑C₁ : Set G) (↑C₂ : Set H) ⊆
    (↑(C₁.minTensorProduct C₂ : PointedCone R (G ⊗[R] H)) : Set (G ⊗[R] H))

Tactic:
fun _ ⟨_, hx, _, hy, hz⟩ => hz ▸ tmul_mem_minTensorProduct hx hy

Premises used: PointedCone.minTensorProduct, Membership.mem, Eq.rec, Set.Subset, SetLike.coe, PointedCone.tmul_mem_minTensorProduct, _private.0.PointedCone.tmul_subset_maxTensorProduct.match_1
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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
⊢ LE.le (α := PointedCone R (G ⊗[R] H)) (C₁.minTensorProduct C₂ : PointedCone R (G ⊗[R] H))
    (C₁.maxTensorProduct C₂ : PointedCone R (G ⊗[R] H))

Tactic:
Submodule.span_le.mpr (tmul_subset_maxTensorProduct C₁ C₂)

Premises used: Iff.mpr, Set.Mem, PointedCone.tmul_subset_maxTensorProduct, Submodule.span_le
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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
⊢ LE.le (α := PointedCone R (G ⊗[R] H)) (C₁.minTensorProduct C₂ : PointedCone R (G ⊗[R] H))
    (C₁.maxTensorProduct C₂ : PointedCone R (G ⊗[R] H))

Tactic:
exact Submodule.span_le.mpr (tmul_subset_maxTensorProduct C₁ C₂)

Premises used: Iff.mpr, PointedCone.tmul_subset_maxTensorProduct, Submodule.span_le
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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₁.minTensorProduct C₂) : PointedCone R (H ⊗[R] G))
    (C₂.minTensorProduct C₁ : PointedCone R (H ⊗[R] G))

Tactic:
simp [minTensorProduct, map, hull, Submodule.map_span, Set.image_image2,
    Set.image2_swap (· ⊗ₜ[R] · : H → G → _)]

Premises used: PointedCone.map, PointedCone.minTensorProduct, Set.image_image2, PointedCone.hull, Set.image2_swap, TensorProduct.tmul, Submodule.map_span
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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
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
⊢ 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))

Tactic:
ext z
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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
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)
⊢ 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:
simp only [mem_map, mem_maxTensorProduct]

Premises used: PointedCone.mem_map, PointedCone.mem_maxTensorProduct
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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)

Tactic:
⟨?_, fun hz ↦
    ⟨(TensorProduct.comm R H G) z, ?_, (TensorProduct.comm R H G).symm_apply_apply z⟩⟩

Premises used: TensorProduct.comm, LinearEquiv.symm_apply_apply, And.intro, Iff.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
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
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 H
hψ : Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ
φ : Dual R G
hφ : 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)
        (((↑(TensorProduct.comm R G H) : G ⊗[R] H →ₗ[R] H ⊗[R] G) : (a : G ⊗[R] H) → H ⊗[R] G) w : H ⊗[R] G) :
      R)

Tactic:
simpa [dualDistrib_apply_comm] using hw φ hφ ψ hψ

Premises used: TensorProduct.dualDistrib_apply_comm