awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
⊢ IsSplittingField K L p ↔
    Splits (map (algebraMap K L) p) ∧
      Eq (α := Subalgebra K L) (Algebra.adjoin K (p.rootSet L)) (IntermediateField.toSubalgebra ⊤)

Tactic:
⟨fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩, fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩⟩

Premises used: Algebra.algebraMap, Polynomial.rootSet, Algebra.adjoin, _private.0.isSplittingField_iff_intermediateField.match_1, Polynomial.IsSplittingField, _private.0.isSplittingField_iff_intermediateField.match_2, And, And.intro, Iff.intro, Polynomial.map, Polynomial.Splits, Polynomial.IsSplittingField.mk, Top.top, Eq, IntermediateField.toSubalgebra
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
⊢ IsSplittingField K L p ↔
    Splits (map (algebraMap K L) p) ∧
      Eq (α := Subalgebra K L) (Algebra.adjoin K (p.rootSet L)) (IntermediateField.toSubalgebra ⊤)

Tactic:
exact ⟨fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩, fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩⟩
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
this :
  Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
    (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔ F = adjoin K (p.rootSet L))
⊢ IsSplittingField.{v, w} K (↥F) p ↔
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) ∧ F = adjoin K (p.rootSet L)

Tactic:
⟨fun h ↦ ⟨h.1, (this h.1).mp h.2⟩, fun h ↦ ⟨h.1, (this h.1).mpr h.2⟩⟩

Premises used: Iff.mpr, Polynomial.IsSplittingField.splits', Polynomial.IsSplittingField.adjoin_rootSet', And.right, And.left, And.intro, Iff.intro, Iff.mp, Polynomial.IsSplittingField.mk
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
this :
  Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
    (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔ F = adjoin K (p.rootSet L))
⊢ IsSplittingField.{v, w} K (↥F) p ↔
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) ∧ F = adjoin K (p.rootSet L)

Tactic:
exact ⟨fun h ↦ ⟨h.1, (this h.1).mp h.2⟩, fun h ↦ ⟨h.1, (this h.1).mpr h.2⟩⟩
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
suffices :
  Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
    (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔ F = adjoin K (p.rootSet L))
⊢ IsSplittingField.{v, w} K (↥F) p ↔
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) ∧ F = adjoin K (p.rootSet L)

Tactic:
suffices _ → (Algebra.adjoin K (p.rootSet F) = ⊤ ↔ F = adjoin K (p.rootSet L)) by
    exact ⟨fun h ↦ ⟨h.1, (this h.1).mp h.2⟩, fun h ↦ ⟨h.1, (this h.1).mpr h.2⟩⟩
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
rw :
  Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
    (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔
      F.toSubalgebra = Algebra.adjoin K (p.rootSet L))
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
    (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔ F = adjoin K (p.rootSet L))

Tactic:
rw [← toSubalgebra_injective.eq_iff,
      adjoin_toSubalgebra_of_isAlgebraic fun x ↦ isAlgebraic_of_mem_rootSet]

Premises used: Function.Injective.eq_iff, IntermediateField.toSubalgebra_injective, isAlgebraic_of_mem_rootSet, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
    (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔
      F.toSubalgebra = Algebra.adjoin K (p.rootSet L))

Tactic:
fun hp ↦ (hp.adjoin_rootSet_eq_range F.val).symm.trans ?_

Premises used: Polynomial.Splits.adjoin_rootSet_eq_range, Iff.trans, IntermediateField.val, Iff.symm
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
refine :
  ∀ (hp : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)),
    Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L)
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
    (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔
      F.toSubalgebra = Algebra.adjoin K (p.rootSet L))

Tactic:
refine fun hp ↦ (hp.adjoin_rootSet_eq_range F.val).symm.trans ?_
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
hp : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
rw : Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.val.range = Algebra.adjoin K (p.rootSet L)
rw₁ rw₂ : F.val.range = Algebra.adjoin K (p.rootSet L) ↔ F.val.range = Algebra.adjoin K (p.rootSet L)
⊢ Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L)

Tactic:
rw [← F.range_val, eq_comm]

Premises used: IntermediateField.range_val, eq_comm
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
hp : Splits (Polynomial.map (algebraMap K L) p)
⊢ IsSplittingField.{v, w} K (↥(adjoin K (p.rootSet L))) p

Tactic:
isSplittingField_iff.mpr ⟨splits_of_splits hp fun _ hx ↦ subset_adjoin K (p.rootSet L) hx, rfl⟩

Premises used: Iff.mpr, Polynomial.rootSet, IntermediateField.subset_adjoin, IntermediateField.isSplittingField_iff, And.intro, rfl, IntermediateField.splits_of_splits
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
inst : Field K
a : K
⊢ Splits (map (algebraMap K K) ((C : (a : K) → K[X]) a))

Tactic:
simp
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
inst : Field K
a : K
⊢ Eq (α := Subalgebra K K) (Algebra.adjoin K (rootSet (T := K) ((C : (a : K) → K[X]) a) K)) ⊤

Tactic:
simp
-- Module: Mathlib.FieldTheory.Tower
Goal:
F : Type u
K : Type v
A : Type w
inst : Ring F
inst_1 : Ring K
inst_2 : Module F K
inst_3 : AddCommGroup A
inst_4 : Module K A
inst_5 : IsTorsionFree K A
inst_6 : Module F A
inst_7 : IsNoetherian F A
inst_8 : IsScalarTower F K A
inst_9 : IsDomain K
inst_10 : Nontrivial A
⊢ Module.Finite F K

Tactic:
let ⟨x, hx⟩ := exists_ne (0 : A)
  Module.Finite.of_injective
    (LinearMap.ringLmapEquivSelf K ℕ A |>.symm x |>.restrictScalars F) (smul_left_injective K hx)

Premises used: LinearEquiv.symm, LinearMap.restrictScalars, LinearMap.ringLmapEquivSelf, exists_ne, Module.Finite.of_injective, smul_left_injective, _private.0.Module.Finite.left.match_1, Nat, Module.Finite, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.FieldTheory.Tower
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : AddCommMonoid A
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : Eq (α := Submodule F A) (span F (↑b : Set A)) ⊤
rw : (↑b : Set A) ⊆ (↑(restrictScalars F (span K (↑b : Set A))) : Set A)
⊢ Eq (α := Submodule F A) (restrictScalars F (span K (↑b : Set A))) (restrictScalars.{u, v, w} F (R := K) ⊤)

Tactic:
rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]

Premises used: eq_top_iff, Submodule.restrictScalars_top, Submodule.span_le
-- Module: Mathlib.FieldTheory.Tower
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : AddCommMonoid A
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : Eq (α := Submodule F A) (span F (↑b : Set A)) ⊤
⊢ (↑b : Set A) ⊆ (↑(restrictScalars F (span K (↑b : Set A))) : Set A)

Tactic:
Submodule.subset_span

Premises used: iInf, Set.iInter, setOf, Submodule.subset_span
-- Module: Mathlib.FieldTheory.Tower
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : AddCommMonoid A
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : Eq (α := Submodule F A) (span F (↑b : Set A)) ⊤
⊢ (↑b : Set A) ⊆ (↑(restrictScalars F (span K (↑b : Set A))) : Set A)

Tactic:
exact Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.Geometry.Convex.Cone.Basic
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 : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C C₁_1 C₂_1 : ConvexCone R M
s : Set M
c : R
x : M
C₁ C₂ : ConvexCone R M
h : C₁.carrier = C₂.carrier
mk :
  ∀ (carrier : Set M) (smul_mem' : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier → c • x ∈ carrier)
    (add_mem' : ∀ ⦃x : M⦄, x ∈ carrier → ∀ ⦃y : M⦄, y ∈ carrier → x + y ∈ carrier)
    (h : { carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' : ConvexCone R M }.carrier = C₂.carrier),
    { carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' : ConvexCone R M } = C₂
⊢ C₁ = C₂

Tactic:
cases C₁
-- Module: Mathlib.Geometry.Convex.Cone.Basic
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 : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C C₁ C₂_1 : ConvexCone R M
s : Set M
c : R
x : M
C₂ : ConvexCone R M
carrier : Set M
smul_mem' : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier → c • x ∈ carrier
add_mem' : ∀ ⦃x : M⦄, x ∈ carrier → ∀ ⦃y : M⦄, y ∈ carrier → x + y ∈ carrier
h : { carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' : ConvexCone R M }.carrier = C₂.carrier
⊢ { carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' : ConvexCone R M } = C₂

Tactic:
congr!
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
s : Set M
h₁ : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ s → c • x ∈ s
h₂ : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → x + y ∈ s
⊢ (↑{ carrier := s, smul_mem' := h₁, add_mem' := h₂ : ConvexCone R M } : Set M) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
s : Set M
x : M
h₁ : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ s → c • x ∈ s
h₂ : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → x + y ∈ s
⊢ x ∈ { carrier := s, smul_mem' := h₁, add_mem' := h₂ : ConvexCone R M } ↔ x ∈ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C₁ C₂ : ConvexCone R M
h : ∀ (x : M), x ∈ C₁ ↔ x ∈ C₂
⊢ C₁ = C₂

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C : ConvexCone R M
c : R
x : M
hc : 0 < c
hx : x ∈ C
⊢ c • x ∈ C

Tactic:
C.smul_mem' hc hx

Premises used: Set.Mem, ConvexCone.smul_mem'
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C : ConvexCone R M
x : M
hx : x ∈ C
y : M
hy : y ∈ C
⊢ x + y ∈ C

Tactic:
C.add_mem' hx hy

Premises used: Set.Mem, ConvexCone.add_mem'
-- Module: Mathlib.Geometry.Convex.Cone.Basic
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 : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C_1 C₁ C₂ : ConvexCone R M
s_1 : Set M
c : R
x : M
C : ConvexCone R M
s : Set M
hs : s = (↑C : Set M)
⊢ ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ s → c • x ∈ s

Tactic:
simpa [hs] using C.smul_mem'

Premises used: ConvexCone.smul_mem'
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C : ConvexCone R M
s : Set M
hs : s = (↑C : Set M)
⊢ C.copy s hs = C

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
S : Set (ConvexCone R M)
⊢ (↑(sInf S) : Set M) = ⋂ C ∈ S, (↑C : Set M)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
x : M
S : Set (ConvexCone R M)
⊢ x ∈ sInf S ↔ ∀ C ∈ S, x ∈ C

Tactic:
mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
ι : Sort u_7
f : ι → ConvexCone R M
⊢ (↑(iInf f) : Set M) = ⋂ (i : ι), (↑(f i) : Set M)

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
x : M
ι : Sort u_7
f : ι → ConvexCone R M
⊢ (∀ (i : ConvexCone R M) (j : i ∈ Set.range f), x ∈ (↑i : Set M)) ↔ ∀ (i : ι), x ∈ f i

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
s : Set M
⊢ s ⊆ (↑(hull R s) : Set M)

Tactic:
simp [hull]

Premises used: ConvexCone.hull
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C : ConvexCone R M
s : Set M
hsC : s ⊆ (↑C : Set M)
⊢ hull R s ≤ C

Tactic:
sInf_le hsC

Premises used: Set.Mem, sInf_le
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C : ConvexCone R M
s : Set M
⊢ hull R s ≤ C ↔ s ⊆ (↑C : Set M)

Tactic:
⟨subset_hull.trans, hull_min⟩

Premises used: HasSubset.Subset.trans, ConvexCone.hull_min, ConvexCone.subset_hull, Iff.intro
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
⊢ GaloisConnection (β := ConvexCone R M) (hull R) SetLike.coe

Tactic:
fun _C _s ↦ hull_le_iff

Premises used: ConvexCone.hull_le_iff, GaloisConnection
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
x : M
⊢ x ∉ ⊥

Tactic:
id

Premises used: Set.Mem, id, Not
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
⊢ (↑⊥ : Set M) = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C : ConvexCone R M
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : C = ⊥ ↔ C = ⊥
⊢ (↑C : Set M) = (↑⊥ : Set M) ↔ C = ⊥

Tactic:
norm_cast
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C₁ C₂ : ConvexCone R M
⊢ (↑(C₁ ⊓ C₂) : Set M) = (↑C₁ : Set M) ∩ (↑C₂ : Set M)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C₁ C₂ : ConvexCone R M
x : M
⊢ x ∈ C₁ ⊓ C₂ ↔ x ∈ C₁ ∧ x ∈ C₂

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
x : M
⊢ Membership.mem (γ := ConvexCone R M) ⊤ x

Tactic:
mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
⊢ (↑⊤ : Set M) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : SMul R M
C₁ C₂ : ConvexCone R M
⊢ Disjoint (↑C₁ : Set M) (↑C₂ : Set M) ↔ Disjoint C₁ C₂

Tactic:
simp [disjoint_iff, ← coe_inf]

Premises used: ConvexCone.coe_inf, disjoint_iff
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C : ConvexCone R M
⊢ Convex R (↑C : Set M)

Tactic:
convex_iff_forall_pos.2 fun _ hx _ hy _ _ ha hb _ ↦ add_mem (C.smul_mem ha hx) (C.smul_mem hb hy)

Premises used: Iff.mpr, ConvexCone.smul_mem, AddMemClass.add_mem, convex_iff_forall_pos
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
C : ConvexCone R M
f : M →ₗ[R] N
⊢ (↑(map f C) : Set N) = (⇑f : (a : M) → N) '' (↑C : Set M)

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
f : M →ₗ[R] N
C : ConvexCone R M
y : N
⊢ y ∈ map f C ↔ ∃ x ∈ C, (f : (a : M) → N) x = y

Tactic:
Set.mem_image f C y

Premises used: Set.Mem, setOf, Set.mem_image, SetLike.coe, Set.image, DFunLike.coe
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid O
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R O
g : N →ₗ[R] O
f : M →ₗ[R] N
C : ConvexCone R M
⊢ map g (map f C) = map (g ∘ₗ f) C

Tactic:
SetLike.coe_injective <| image_image g f C

Premises used: Set.image_image, SetLike.coe_injective, SetLike.coe, DFunLike.coe
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C : ConvexCone R M
⊢ map LinearMap.id C = C

Tactic:
SetLike.coe_injective <| image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.Geometry.Convex.Cone.Basic
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 : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid O
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
c : R
hc : 0 < c
x : M
hx : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) x
rw : HSMul.hSMul (β := N) c ((f : (a : M) → N) x : N) ∈ (↑C : Set N)
⊢ Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) (c • x)

Tactic:
rw [mem_preimage, f.map_smul c]

Premises used: LinearMap.map_smul, Set.mem_preimage
-- Module: Mathlib.Geometry.Convex.Cone.Basic
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 : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid O
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
c : R
hc : 0 < c
x : M
hx : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) x
⊢ HSMul.hSMul (β := N) c ((f : (a : M) → N) x : N) ∈ (↑C : Set N)

Tactic:
C.smul_mem hc hx

Premises used: ConvexCone.smul_mem
-- Module: Mathlib.Geometry.Convex.Cone.Basic
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 : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid O
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
c : R
hc : 0 < c
x : M
hx : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) x
⊢ HSMul.hSMul (β := N) c ((f : (a : M) → N) x : N) ∈ (↑C : Set N)

Tactic:
exact C.smul_mem hc hx

Premises used: ConvexCone.smul_mem
-- Module: Mathlib.Geometry.Convex.Cone.Basic
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 : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid O
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
x : M
hx : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) x
y : M
hy : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) y
rw : HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ∈ (↑C : Set N)
⊢ Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) (x + y)

Tactic:
rw [mem_preimage, f.map_add]

Premises used: LinearMap.map_add, Set.mem_preimage
-- Module: Mathlib.Geometry.Convex.Cone.Basic
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 : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid O
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
x : M
hx : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) x
y : M
hy : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) y
⊢ HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ∈ (↑C : Set N)

Tactic:
add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Geometry.Convex.Cone.Basic
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 : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid O
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
x : M
hx : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) x
y : M
hy : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) y
⊢ HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ∈ (↑C : Set N)

Tactic:
exact add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
f : M →ₗ[R] N
C : ConvexCone R N
⊢ (↑(comap f C) : Set M) = (⇑f : (a : M) → N) ⁻¹' (↑C : Set N)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C : ConvexCone R M
⊢ comap LinearMap.id C = C

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, ConvexCone.comap, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid O
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R O
g : N →ₗ[R] O
f : M →ₗ[R] N
C : ConvexCone R O
⊢ comap f (comap g C) = comap (g ∘ₗ f) C

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, ConvexCone.comap, rfl