awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₄ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₅ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₆ :
  Finset.card.{u_5} (α := A) (Finset.image (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) Finset.univ) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₇ : InjOn (β := A) (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) (↑Finset.univ : Set (E →ₐ[F] A)) ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₄ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₅ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₆ :
  Finset.card.{u_5} (α := A) (Finset.image (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) Finset.univ) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₇ :
  InjOn (β := A) (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) (↑Finset.univ : Set (E →ₐ[F] A)) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₈ : InjOn (β := A) (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) univ ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
φ : E →ₐ[F] A
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔
    ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ
have refine : ∀ (h : ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ),
  finrank (↥F⟮α⟯) E = finrank (↥⊤) E
Tactic: refine ⟨fun h ψ hψ ↦ (Field.primitive_element_iff_algHom_eq_of_eval' F A hA α).mp h hψ,
    fun h ↦ eq_of_le_of_finrank_eq' le_top ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ
this : Algebra.{u_4, u_5} (↥F⟮α⟯) A := RingHom.toAlgebra (AlgHom.toRingHom (φ.comp (val F⟮α⟯)))
⊢ finrank (↥F⟮α⟯) E = finrank (↥⊤) E
have rw : ∃ (x : E →ₐ[↥F⟮α⟯] A), ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x
Tactic: rw [IntermediateField.finrank_top, ← AlgHom.card_of_splits _ _ A, Fintype.card_eq_one_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ
this : Algebra.{u_4, u_5} (↥F⟮α⟯) A := RingHom.toAlgebra (AlgHom.toRingHom (φ.comp (val F⟮α⟯)))
rw : ∃ (x : E →ₐ[↥F⟮α⟯] A), ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x
⊢ finrank (↥F⟮α⟯) E = finrank (↥⊤) E
have rw₁ : ∀ (x : E), Splits (Polynomial.map (R := ↥F⟮α⟯) (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x))
Tactic: rw [IntermediateField.finrank_top, ← AlgHom.card_of_splits _ _ A, Fintype.card_eq_one_iff]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s_1 t : Set M
y : N
s : Set M
u v : N
hu :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    u
hv :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    v
x : M
hx : x ∈ s
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) (u + v) : R)
have rw : 0 ≤
  HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) u : R)
    ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) v : R)
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s_1 t : Set M
y_1 : N
s : Set M
c : R≥0
y : N
hy :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    y
x : M
hx : x ∈ s
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) (c • y) : R)
have rw : 0 ≤ HSMul.hSMul (β := R) (↑c : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)
Tactic: rw [← Nonneg.coe_smul, map_smul]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
⊢ Eq (α := PointedCone R N) (dual p ∅) ⊤
have h : ∀ (x : N), Membership.mem (γ := PointedCone R N) (dual p ∅) x ↔ Membership.mem (γ := PointedCone R N) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
⊢ Eq (α := PointedCone R N) (dual p 0) ⊤
have h : ∀ (x : N), Membership.mem (γ := PointedCone R N) (dual p 0) x ↔ Membership.mem (γ := PointedCone R N) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
⊢ Eq (α := PointedCone R N) (dual p (↑p.ker : Set M)) ⊤
have h : ∀ (x : N), Membership.mem (γ := PointedCone R N) (dual p (↑p.ker : Set M)) x ↔ Membership.mem (γ := PointedCone R N) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : M
⊢ Eq (α := PointedCone R N) (dual p {x}) (comap ((p : (a : M) → N →ₗ[R] R) x) (positive R R))
have h : ∀ (x_1 : N),
  Membership.mem (γ := PointedCone R N) (dual p {x}) x_1 ↔
    Membership.mem (γ := PointedCone R N) (comap ((p : (a : M) → N →ₗ[R] R) x) (positive R R)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : M
s : Set M
⊢ Eq (α := PointedCone R N) (dual p (insert x s)) (dual p {x} ⊓ dual p s)
have rw : Eq (α := PointedCone R N) (dual p ({x} ∪ s)) (dual p {x} ⊓ dual p s)
Tactic: rw [insert_eq, dual_union]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : M
s : Set M
rw : Eq (α := PointedCone R N) (dual p ({x} ∪ s)) (dual p {x} ⊓ dual p s)
⊢ Eq (α := PointedCone R N) (dual p (insert x s)) (dual p {x} ⊓ dual p s)
have rw₁ : Eq (α := PointedCone R N) (dual p {x} ⊓ dual p s) (dual p {x} ⊓ dual p s)
Tactic: rw [insert_eq, dual_union]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
ι : Sort u_4
f : ι → Set M
⊢ Eq (α := PointedCone R N) (dual p (⋃ (i : ι), f i)) (⨅ (i : ι), dual p (f i))
have h : ∀ (x : N),
  Membership.mem (γ := PointedCone R N) (dual p (⋃ (i : ι), f i)) x ↔
    Membership.mem (γ := PointedCone R N) (⨅ (i : ι), dual p (f i)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
S : Set (Set M)
⊢ Eq (α := PointedCone R N) (dual p (⋃₀ S)) (sInf (dual p '' S))
have h : ∀ (x : N),
  Membership.mem (γ := PointedCone R N) (dual p (⋃₀ S)) x ↔ Membership.mem (γ := PointedCone R N) (sInf (dual p '' S)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
⊢ (↑(dual p s) : Set N) = ⋂ (i : (↑s : Type u_2)), (↑(dual p {(↑i : M)}) : Set N)
have h : ∀ (x : N),
  x ∈ (↑(dual p s) : Set N) ↔ Membership.mem (γ := Set N) (⋂ (i : (↑s : Type u_2)), (↑(dual p {(↑i : M)}) : Set N)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
t : Set N
⊢ s ⊆ (↑(dual p.flip t) : Set M) ↔ t ⊆ (↑(dual p s) : Set N)
have mp : s ⊆ (↑(dual p.flip t) : Set M) → t ⊆ (↑(dual p s) : Set N)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
t : Set N
mp : s ⊆ (↑(dual p.flip t) : Set M) → t ⊆ (↑(dual p s) : Set N)
⊢ s ⊆ (↑(dual p.flip t) : Set M) ↔ t ⊆ (↑(dual p s) : Set N)
have mpr : t ⊆ (↑(dual p s) : Set N) → s ⊆ (↑(dual p.flip t) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
⊢ Eq (α := PointedCone R N) (dual p (↑(hull R s) : Set M)) (dual p s)
have refine : ∀ (x : N) (hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x) (y : M) (hy : y ∈ (↑(hull R s) : Set M)),
  LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
Tactic: refine le_antisymm (dual_anti Submodule.subset_span) (fun x hx y hy => ?_)
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y_1 y z : M
_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y
_hz : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) z
hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
hz : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) (y + z) : N →ₗ[R] R) : (a : N) → R) x : R)
have add : 0 ≤
  HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
    ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)
Tactic: rw [map_add, add_apply]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y_1 : M
t : R≥0
y : M
_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y
hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) (t • y) : N →ₗ[R] R) : (a : N) → R) x : R)
have smul : 0 ≤ HSMul.hSMul (β := R) (↑t : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
Tactic: rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y : M
hy : y ∈ (↑(hull R s) : Set M)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
have mem : ∀ (_y : M) (h : _y ∈ s), LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) _y : N →ₗ[R] R) : (a : N) → R) x : R)
Tactic: induction hy using Submodule.span_induction with
  | mem _y h => exact hx h
  | zero => simp
  | add y z _hy _hz hy hz => rw [map_add, add_apply]; exact add_nonneg hy hz
  | smul t y _hy hy => rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y : M
hy : y ∈ (↑(hull R s) : Set M)
mem :
  ∀ (_y : M) (h : _y ∈ s),
    LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) _y : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
have zero : LE.le.{u_1} (α := R) (0 : R) (((p : (a : M) → N →ₗ[R] R) 0 : (a : N) → R) x : R)
Tactic: induction hy using Submodule.span_induction with
  | mem _y h => exact hx h
  | zero => simp
  | add y z _hy _hz hy hz => rw [map_add, add_apply]; exact add_nonneg hy hz
  | smul t y _hy hy => rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y : M
hy : y ∈ (↑(hull R s) : Set M)
mem :
  ∀ (_y : M) (h : _y ∈ s),
    LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) _y : N →ₗ[R] R) : (a : N) → R) x : R)
zero : LE.le.{u_1} (α := R) (0 : R) (((p : (a : M) → N →ₗ[R] R) 0 : (a : N) → R) x : R)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
have add : ∀ (y z : M) (_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y)
  (_hz : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) z)
  (hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R))
  (hz : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)),
  LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) (y + z) : N →ₗ[R] R) : (a : N) → R) x : R)
Tactic: induction hy using Submodule.span_induction with
  | mem _y h => exact hx h
  | zero => simp
  | add y z _hy _hz hy hz => rw [map_add, add_apply]; exact add_nonneg hy hz
  | smul t y _hy hy => rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y : M
hy : y ∈ (↑(hull R s) : Set M)
mem :
  ∀ (_y : M) (h : _y ∈ s),
    LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) _y : N →ₗ[R] R) : (a : N) → R) x : R)
zero : LE.le.{u_1} (α := R) (0 : R) (((p : (a : M) → N →ₗ[R] R) 0 : (a : N) → R) x : R)
add :
  ∀ (y z : M) (_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y)
    (_hz : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) z)
    (hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R))
    (hz : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)),
    LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) (y + z) : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
have smul : ∀ (t : R≥0) (y : M) (_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y)
  (hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)),
  LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) (t • y) : N →ₗ[R] R) : (a : N) → R) x : R)
Tactic: induction hy using Submodule.span_induction with
  | mem _y h => exact hx h
  | zero => simp
  | add y z _hy _hz hy hz => rw [map_add, add_apply]; exact add_nonneg hy hz
  | smul t y _hy hy => rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
M' : Type u_4
inst_7 : AddCommMonoid M'
inst_8 : Module R M'
s : Set M'
q : M' →ₗ[R] M
⊢ Eq (α := PointedCone R N) (dual p ((⇑q : (a : M') → M) '' s)) (dual (p ∘ₗ q) s)
have h : ∀ (x : N),
  Membership.mem (γ := PointedCone R N) (dual p ((⇑q : (a : M') → M) '' s)) x ↔
    Membership.mem (γ := PointedCone R N) (dual (p ∘ₗ q) s) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
⊢ Eq (α := PointedCone R N) (dual p s) (comap p.flip (dual (Module.Dual.eval R M) s))
have h : ∀ (x : N),
  Membership.mem (γ := PointedCone R N) (dual p s) x ↔
    Membership.mem (γ := PointedCone R N) (comap p.flip (dual (Module.Dual.eval R M) s)) x
Tactic: ext