awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
rw : ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ
| f y * ∫⁻ (y_1 : G), g y_1 * k (y_1⁻¹ * (y⁻¹ * x)) ∂μ

Tactic:
rw [← lintegral_const_mul'' _ (by fun_prop), ← lintegral_mul_left_eq_self _ y⁻¹]

Premises used: Inv.inv, MeasureTheory.lintegral_const_mul'', MeasureTheory.lintegral_mul_left_eq_self
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
h :
  ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x) ∂μ
⊢ ∫⁻ (y : G), f y * ∫⁻ (y_1 : G), g y_1 * k (y_1⁻¹ * (y⁻¹ * x)) ∂μ ∂μ =
    ∫⁻ (y : G), (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x) ∂μ

Tactic:
conv in f _ * (∫⁻ _, _ ∂μ) =>
    rw [← lintegral_const_mul'' _ (by fun_prop), ← lintegral_mul_left_eq_self _ y⁻¹]

Premises used: MeasureTheory.lintegral_const_mul'', MeasureTheory.lintegral
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₂ : map (fun (a : G) ↦ a⁻¹ * y) μ ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y_1 : G) ↦ f y_1 * g (y_1⁻¹ * y)) μ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
rw : ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ
| (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x)

Tactic:
rw [← lintegral_mul_const'' _ (by fun_prop)]

Premises used: MeasureTheory.lintegral_mul_const''
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
h :
  ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ
⊢ ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x) ∂μ

Tactic:
conv in (∫⁻ _, _ ∂μ) * k _ =>
    rw [← lintegral_mul_const'' _ (by fun_prop)]

Premises used: MeasureTheory.lintegral_mul_const'', MeasureTheory.lintegral
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
h :
  ∫⁻ (y : G), ∫⁻ (x_1 : G), f x_1 * (g (x_1⁻¹ * y) * k ((x_1⁻¹ * y)⁻¹ * (x_1⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ
h₁ :
  AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))))
    (μ.prod μ)
⊢ ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ

Tactic:
rw [lintegral_lintegral_swap]

Premises used: MeasureTheory.lintegral_lintegral_swap
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ ∫⁻ (y : G), ∫⁻ (x_1 : G), f x_1 * (g (x_1⁻¹ * y) * k ((x_1⁻¹ * y)⁻¹ * (x_1⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₅ : map (fun (a : G × G) ↦ a.1⁻¹ * a.2) (μ.prod μ) ≪ μ
funProp₆ : mG ≤ mG
funProp₇ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ k a0
funProp₈ : map (fun (a : G × G) ↦ a.2⁻¹ * x) (μ.prod μ) ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
simpa : AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))))
    (μ.prod μ)

Tactic:
simpa [mul_assoc] using by fun_prop

Premises used: mul_assoc
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hk : Measurable k
⊢ f ⋆ₘₗ[μ] g ⋆ₘₗ[μ] k = (f ⋆ₘₗ[μ] g) ⋆ₘₗ[μ] k

Tactic:
mlconvolution_assoc₀ hf.aemeasurable hg.aemeasurable hk.aemeasurable

Premises used: MeasureTheory.mlconvolution_assoc₀, Measurable.aemeasurable
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : CommGroup G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : μ.IsInvInvariant
f g : G → ℝ≥0∞
h : ∀ (x : G), (f ⋆ₘₗ[μ] g) x = (g ⋆ₘₗ[μ] f) x
⊢ f ⋆ₘₗ[μ] g = g ⋆ₘₗ[μ] f

Tactic:
ext x
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : CommGroup G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : μ.IsInvInvariant
f g : G → ℝ≥0∞
x : G
h : ∫⁻ (x_1 : G), f (x * x_1⁻¹) * g ((x * x_1⁻¹)⁻¹ * x) ∂μ = ∫⁻ (y : G), g y * f (y⁻¹ * x) ∂μ
⊢ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ = ∫⁻ (y : G), g y * f (y⁻¹ * x) ∂μ

Tactic:
rw [← lintegral_mul_left_eq_self _ x, ← lintegral_inv_eq_self]

Premises used: MeasureTheory.lintegral_inv_eq_self, MeasureTheory.lintegral_mul_left_eq_self
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : CommGroup G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : μ.IsInvInvariant
f g : G → ℝ≥0∞
x : G
⊢ ∫⁻ (x_1 : G), f (x * x_1⁻¹) * g ((x * x_1⁻¹)⁻¹ * x) ∂μ = ∫⁻ (y : G), g y * f (y⁻¹ * x) ∂μ

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
⊢ AbsConvex.{u_1, u_2} 𝕜 (E := E) ∅

Tactic:
⟨balanced_empty, convex_empty⟩

Premises used: balanced_empty, AbsConvex, convex_empty, And.intro
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
⊢ AbsConvex.{u_1, u_2} 𝕜 (E := E) Set.univ

Tactic:
⟨balanced_univ, convex_univ⟩

Premises used: AbsConvex, convex_univ, And.intro, balanced_univ
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s t : Set E
hs : AbsConvex 𝕜 s
ht : AbsConvex 𝕜 t
⊢ AbsConvex 𝕜 (s ∩ t)

Tactic:
⟨hs.1.inter ht.1, hs.2.inter ht.2⟩

Premises used: AbsConvex, Convex.inter, Balanced.inter, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
S : Set (Set E)
h : ∀ s ∈ S, AbsConvex 𝕜 s
⊢ AbsConvex 𝕜 (⋂₀ S)

Tactic:
⟨.sInter fun s hs => (h s hs).1, convex_sInter fun s hs => (h s hs).2⟩

Premises used: AbsConvex, Balanced.sInter, And.right, And.left, And.intro, convex_sInter
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
ι : Sort u_3
κ : ι → Sort u_4
f : (i : ι) → κ i → Set E
h : ∀ (i : ι) (j : κ i), AbsConvex 𝕜 (f i j)
⊢ AbsConvex.{u_1, u_2} 𝕜 (E := E) (⋂ (i : ι), ⋂ (j : κ i), f i j)

Tactic:
AbsConvex.iInter fun _ => (AbsConvex.iInter fun _ => h _ _)

Premises used: AbsConvex.iInter
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
⊢ s ⊆ (absConvexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
(absConvexHull 𝕜).le_closure s

Premises used: absConvexHull, ClosureOperator.le_closure
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
⊢ AbsConvex.{u_1, u_2} 𝕜 (E := E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
(absConvexHull 𝕜).isClosed_closure s

Premises used: absConvexHull, AbsConvex, ClosureOperator.isClosed_closure
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
⊢ Balanced.{u_1, u_2} 𝕜 (E := E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
absConvex_absConvexHull.1

Premises used: absConvex_absConvexHull, And.left
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
⊢ Convex.{u_1, u_2} 𝕜 (E := E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
absConvex_absConvexHull.2

Premises used: absConvex_absConvexHull, And.right
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
⊢ Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    (⋂ (t : Set E), ⋂ (_ : s ⊆ t), ⋂ (_ : AbsConvex 𝕜 t), t : Set E)

Tactic:
simp [absConvexHull, iInter_subtype, iInter_and]

Premises used: absConvexHull, Set.iInter_subtype, Set.iInter_and
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
x : E
simp_rw :
  Membership.mem (γ := Set E) (⋂ (t : Set E), ⋂ (_ : s ⊆ t), ⋂ (_ : AbsConvex 𝕜 t), t) x ↔
    ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t
⊢ Membership.mem (γ := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) x ↔
    ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t

Tactic:
simp_rw [absConvexHull_eq_iInter, mem_iInter]

Premises used: Set.mem_iInter, absConvexHull_eq_iInter
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s t : Set E
⊢ s ⊆ t → AbsConvex 𝕜 t → (absConvexHull 𝕜 : (a : Set E) → Set E) s ⊆ t

Tactic:
(absConvexHull 𝕜).closure_min

Premises used: AbsConvex, ClosureOperator.closure_min
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s t : Set E
ht : AbsConvex 𝕜 t
⊢ (absConvexHull 𝕜 : (a : Set E) → Set E) s ⊆ t ↔ s ⊆ t

Tactic:
(show (absConvexHull 𝕜).IsClosed t from ht).closure_le_iff

Premises used: ClosureOperator.IsClosed.closure_le_iff
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s t : Set E
hst : s ⊆ t
⊢ Subset (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    ((absConvexHull 𝕜 : (a : Set E) → Set E) t : Set E)

Tactic:
(absConvexHull 𝕜).monotone hst

Premises used: absConvexHull, ClosureOperator.monotone
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
⊢ (absConvexHull 𝕜 : (a : Set E) → Set E) s = s ↔ AbsConvex 𝕜 s

Tactic:
(absConvexHull 𝕜).isClosed_iff.symm

Premises used: absConvexHull, AbsConvex, ClosureOperator.isClosed_iff, Iff.symm
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
⊢ Eq.{u_2 + 1} (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) univ : Set E) (univ : Set E)

Tactic:
ClosureOperator.closure_top (absConvexHull 𝕜)

Premises used: absConvexHull, ClosureOperator.closure_top
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
⊢ Eq.{u_2 + 1} (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) ∅ : Set E) (∅ : Set E)

Tactic:
AbsConvex.empty.absConvexHull_eq

Premises used: AbsConvex.empty, AbsConvex.absConvexHull_eq
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
mp : Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) → s = ∅
mpr : s = ∅ → Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
⊢ Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ s = ∅

Tactic:
constructor
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
h : Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
mp : s ⊆ (absConvexHull 𝕜 : (a : Set E) → Set E) s
⊢ s = ∅

Tactic:
rw [← Set.subset_empty_iff, ← h]

Premises used: Set.subset_empty_iff
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
h : Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
⊢ s ⊆ (absConvexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
subset_absConvexHull

Premises used: subset_absConvexHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
h : Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
⊢ s ⊆ (absConvexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
exact subset_absConvexHull

Premises used: subset_absConvexHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
⊢ Eq.{u_2 + 1} (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) ∅ : Set E) (∅ : Set E)

Tactic:
absConvexHull_empty

Premises used: absConvexHull_empty
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
⊢ Eq.{u_2 + 1} (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) ∅ : Set E) (∅ : Set E)

Tactic:
exact absConvexHull_empty

Premises used: absConvexHull_empty
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
rw : ¬Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ ¬s = ∅
⊢ Set.Nonempty.{u_2} (α := E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s) ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]

Premises used: Ne, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
⊢ ¬Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ ¬s = ∅

Tactic:
not_congr absConvexHull_eq_empty

Premises used: absConvexHull_eq_empty, not_congr
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
⊢ ¬Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ ¬s = ∅

Tactic:
exact not_congr absConvexHull_eq_empty

Premises used: absConvexHull_eq_empty, not_congr
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
inst_4 : TopologicalSpace E
S : Set (Set E)
h : ∀ s ∈ S, AbsConvex 𝕜 s ∧ IsClosed[inst_4] s
⊢ AbsConvex 𝕜 (⋂₀ S) ∧ IsClosed[inst_4] (⋂₀ S)

Tactic:
⟨AbsConvex.sInter (fun s hs => (h s hs).1), isClosed_sInter fun _ hs => (h _ hs).2⟩

Premises used: AbsConvex.sInter, And.right, And.left, And.intro, isClosed_sInter
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
inst_4 : TopologicalSpace E
s : Set E
⊢ AbsConvex.{u_1, u_2} 𝕜 (E := E) ((closedAbsConvexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
((closedAbsConvexHull 𝕜).isClosed_closure s).1

Premises used: closedAbsConvexHull, And.left, ClosureOperator.isClosed_closure
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
inst_4 : TopologicalSpace E
s : Set E
⊢ IsClosed[inst_4] ((closedAbsConvexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
((closedAbsConvexHull 𝕜).isClosed_closure s).2

Premises used: closedAbsConvexHull, And.right, ClosureOperator.isClosed_closure
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
inst_4 : TopologicalSpace E
s : Set E
⊢ s ⊆ (closedAbsConvexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
(closedAbsConvexHull 𝕜).le_closure s

Premises used: closedAbsConvexHull, ClosureOperator.le_closure
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
inst_4 : TopologicalSpace E
s : Set E
⊢ closure[inst_4] s ⊆ (closedAbsConvexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
closure_minimal subset_closedAbsConvexHull isClosed_closedAbsConvexHull

Premises used: closure_minimal, subset_closedAbsConvexHull, isClosed_closedAbsConvexHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
inst_4 : TopologicalSpace E
s t : Set E
hst : s ⊆ t
h_conv : AbsConvex 𝕜 t
h_closed : IsClosed[inst_4] t
⊢ (closedAbsConvexHull 𝕜 : (a : Set E) → Set E) s ⊆ t

Tactic:
(closedAbsConvexHull 𝕜).closure_min hst ⟨h_conv, h_closed⟩

Premises used: ClosureOperator.closure_min, And.intro
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
inst_4 : TopologicalSpace E
s : Set E
⊢ Subset (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    ((closedAbsConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)

Tactic:
absConvexHull_min subset_closedAbsConvexHull absConvex_convexClosedHull

Premises used: subset_closedAbsConvexHull, absConvex_convexClosedHull, absConvexHull_min
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
inst_4 : TopologicalSpace E
s : Set E
⊢ Subset (α := Set E) ((closedAbsConvexHull 𝕜 : (a : Set E) → Set E) (closure[inst_4] s) : Set E)
    ((closedAbsConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)

Tactic:
simpa using ((closedAbsConvexHull 𝕜).monotone
      (closure_subset_closedAbsConvexHull (𝕜 := 𝕜) (E := E)))

Premises used: closedAbsConvexHull, ClosureOperator.monotone, closure_subset_closedAbsConvexHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : AbsConvex 𝕜 s
⊢ AbsConvex 𝕜 (closure[inst_4] s)

Tactic:
⟨Balanced.closure hs.1, Convex.closure hs.2⟩

Premises used: AbsConvex, Balanced.closure, Convex.closure, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
⊢ Eq (α := Set E) ((closedAbsConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    (closure[inst_4] ((absConvexHull 𝕜 : (a : Set E) → Set E) s) : Set E)

Tactic:
subset_antisymm
  (closedAbsConvexHull_min (subset_trans (subset_absConvexHull) subset_closure)
    (AbsConvex.closure absConvex_absConvexHull) isClosed_closure)
  (closure_minimal absConvexHull_subset_closedAbsConvexHull isClosed_closedAbsConvexHull)

Premises used: subset_closure, subset_absConvexHull, closure_minimal, subset_trans, closedAbsConvexHull_min, subset_antisymm, absConvexHull_subset_closedAbsConvexHull, AbsConvex.closure, absConvex_absConvexHull, isClosed_closure, isClosed_closedAbsConvexHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
⊢ Filter.HasBasis (𝓝 0) (fun (s : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) s ∧ AbsConvex 𝕜 s) id

Tactic:
(LocallyConvexSpace.convex_basis_zero 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs =>
      ⟨s, ⟨hs.1, hs.2.2⟩, rfl.subset⟩

Premises used: LocallyConvexSpace.convex_basis_zero, Eq.subset, And.right, And.left, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis, rfl