awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
simp_rw : ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ x⁻¹ ^ (n + 1)
⊢ ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ x ^ -[n+1]

Tactic:
simp_rw [zpow_negSucc, ← inv_pow]

Premises used: zpow_negSucc, inv_pow
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
⊢ 0 ≤ x⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
refine :
  ∀ ⦃x : 𝕜⦄,
    Membership.mem (γ := Set 𝕜) (Ioi 0) x →
      ∀ ⦃y : 𝕜⦄,
        Membership.mem (γ := Set 𝕜) (Ioi 0) y →
          ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → (a • x + b • y)⁻¹ ≤ a • x⁻¹ + b • y⁻¹
⊢ ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ x⁻¹ ^ (n + 1)

Tactic:
refine (convexOn_iff_forall_pos.2 ⟨convex_Ioi _, ?_⟩).pow (fun x (hx : 0 < x) ↦ by positivity) _

Premises used: Iff.mpr, convexOn_iff_forall_pos, And.intro, ConvexOn.pow, convex_Ioi
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
simp : (a * x + b * y)⁻¹ ≤ a * x⁻¹ + b * y⁻¹
⊢ (a • x + b • y)⁻¹ ≤ a • x⁻¹ + b • y⁻¹

Tactic:
simp only [smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
field_simp : x * y ≤ (a * x + b * y) * (a * y + x * b)
⊢ (a * x + b * y)⁻¹ ≤ a * x⁻¹ + b * y⁻¹

Tactic:
field_simp
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 ≤ a * b * HPow.hPow (β := ℕ) (x - y) 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 ≤ a * b * HPow.hPow (β := ℕ) (x - y) 2

Tactic:
have H : 0 ≤ a * b * (x - y) ^ 2 := by positivity
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
H : 0 ≤ a * b * HPow.hPow (β := ℕ) (x - y) 2
⊢ x * y ≤ (a * x + b * y) * (a * y + x * b)

Tactic:
linear_combination H - x * y * (a + b + 1) * hab

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.NNReal
Goal:
x y : ℝ≥0
⊢ Icc x y ⊆ segment ℝ≥0 x y

Tactic:
Nonneg.Icc_subset_segment

Premises used: NNReal.mk, NNReal, Nonneg.Icc_subset_segment
-- Module: Mathlib.Analysis.Convex.NNReal
Goal:
x y : ℝ≥0
hxy : x ≤ y
⊢ segment ℝ≥0 x y = Icc x y

Tactic:
Nonneg.segment_eq_Icc hxy

Premises used: NNReal.mk, NNReal, Nonneg.segment_eq_Icc
-- Module: Mathlib.Analysis.Convex.NNReal
Goal:
x y : ℝ≥0
⊢ segment ℝ≥0 x y = uIcc x y

Tactic:
Nonneg.segment_eq_uIcc

Premises used: Nonneg.segment_eq_uIcc, NNReal.mk, NNReal
-- Module: Mathlib.Analysis.Convex.NNReal
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : Module ℝ M
s : Set M
⊢ Convex ℝ≥0 s ↔ Convex ℝ s

Tactic:
⟨fun H ↦ ?_, Convex.lift ℝ≥0⟩

Premises used: NNReal, Iff.intro, Convex.lift
-- Module: Mathlib.Analysis.Convex.NNReal
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : Module ℝ M
s : Set M
refine : ∀ (H : Convex ℝ≥0 s), Convex ℝ s
⊢ Convex ℝ≥0 s ↔ Convex ℝ s

Tactic:
refine ⟨fun H ↦ ?_, Convex.lift ℝ≥0⟩
-- Module: Mathlib.Analysis.Convex.NNReal
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : Module ℝ M
s : Set M
H : Convex ℝ≥0 s
x : M
hx : x ∈ s
_ : ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
⊢ StarConvex ℝ x s

Tactic:
_
-- Module: Mathlib.Analysis.Convex.NNReal
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : Module ℝ M
s : Set M
H : Convex ℝ≥0 s
x : M
hx : x ∈ s
y : M
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
a₁ : (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) a ha + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) b hb) : ℝ) = (↑1 : ℝ)
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) a ha + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) b hb = 1

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.NNReal
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : Module ℝ M
s : Set M
H : Convex ℝ≥0 s
x : M
hx : x ∈ s
y : M
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) a ha + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) b hb) : ℝ) = (↑1 : ℝ)

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.NNReal
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : Module ℝ M
s : Set M
H : Convex ℝ≥0 s
x : M
hx : x ∈ s
y : M
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Tactic:
exact H hx hy (a := ⟨a, ha⟩) (b := ⟨b, hb⟩) zero_le zero_le (by ext; simpa)

Premises used: zero_le
-- Module: Mathlib.Analysis.Convex.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set X
f : PartitionOfUnity ι X s
g : ι → X → E
t : Set E
x : X
hx : x ∈ s
hg : ∀ (i : ι), Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ) → g i x ∈ t
ht : Convex ℝ t
⊢ ∑ᶠ (i : ι), HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (g i x) ∈ t

Tactic:
ht.finsum_mem (fun _ => f.nonneg _ _) (f.sum_eq_one hx) hg

Premises used: Set.Mem, PartitionOfUnity.sum_eq_one, PartitionOfUnity.nonneg, Convex.finsum_mem
-- Module: Mathlib.Analysis.Convex.PartitionOfUnity
Goal:
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : NormalSpace X
inst_4 : ParacompactSpace X
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
H : ∀ (x : X), ∃ U ∈ 𝓝 x, ∃ (g : X → E), ContinuousOn g U ∧ ∀ y ∈ U, g y ∈ t y
choose :
  ∀ (U : (x : X) → Set X) (hU : ∀ (x : X), U x ∈ 𝓝 x) (g : (x : X) → X → E) (hgc : ∀ (x : X), ContinuousOn (g x) (U x))
    (hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y),
    ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)
⊢ ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)

Tactic:
choose U hU g hgc hgt using H
-- Module: Mathlib.Analysis.Convex.PartitionOfUnity
Goal:
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : NormalSpace X
inst_4 : ParacompactSpace X
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : (x : X) → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
obtain :
  ∀ (f : PartitionOfUnity X X) (hf : f.IsSubordinate (s := univ) fun (x : X) ↦ interior (U x)),
    ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)
⊢ ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)

Tactic:
obtain ⟨f, hf⟩ := PartitionOfUnity.exists_isSubordinate isClosed_univ (fun x => interior (U x))
    (fun x => isOpen_interior) fun x _ => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩

Premises used: isClosed_univ, Iff.mpr, mem_interior_iff_mem_nhds, isOpen_interior, Set.mem_iUnion, PartitionOfUnity.exists_isSubordinate, interior, Exists.intro
-- Module: Mathlib.Analysis.Convex.PartitionOfUnity
Goal:
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : NormalSpace X
inst_4 : ParacompactSpace X
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : (x : X) → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X
hf : f.IsSubordinate (s := univ) fun (x : X) ↦ interior (U x)
⊢ ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)

Tactic:
⟨⟨fun x => ∑ᶠ i, f i x • g i x,
    hf.continuous_finsum_smul (fun i => isOpen_interior) fun i => (hgc i).mono interior_subset⟩,
    fun x => f.finsum_smul_mem_convex (mem_univ x) (fun i hi => hgt _ _ ?_) (ht _)⟩

Premises used: interior_subset, ContinuousMap.mk, isOpen_interior, finsum, PartitionOfUnity.IsSubordinate.continuous_finsum_smul, PartitionOfUnity.finsum_smul_mem_convex, Exists.intro, Set.mem_univ, ContinuousOn.mono, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.PartitionOfUnity
Goal:
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : NormalSpace X
inst_4 : ParacompactSpace X
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : (x : X) → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X
hf : f.IsSubordinate (s := univ) fun (x : X) ↦ interior (U x)
refine : ∀ (x i : X) (hi : Ne (α := ℝ) ((((f : (a : X) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)), x ∈ U i
⊢ ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)

Tactic:
refine ⟨⟨fun x => ∑ᶠ i, f i x • g i x,
    hf.continuous_finsum_smul (fun i => isOpen_interior) fun i => (hgc i).mono interior_subset⟩,
    fun x => f.finsum_smul_mem_convex (mem_univ x) (fun i hi => hgt _ _ ?_) (ht _)⟩
-- Module: Mathlib.Analysis.Convex.PartitionOfUnity
Goal:
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : NormalSpace X
inst_4 : ParacompactSpace X
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : (x : X) → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X
hf : f.IsSubordinate (s := univ) fun (x : X) ↦ interior (U x)
x i : X
hi : Ne (α := ℝ) ((((f : (a : X) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ x ∈ U i

Tactic:
interior_subset (hf _ <| subset_closure hi)

Premises used: interior_subset, subset_closure
-- Module: Mathlib.Analysis.Convex.PartitionOfUnity
Goal:
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : NormalSpace X
inst_4 : ParacompactSpace X
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : (x : X) → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X
hf : f.IsSubordinate (s := univ) fun (x : X) ↦ interior (U x)
x i : X
hi : Ne (α := ℝ) ((((f : (a : X) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ x ∈ U i

Tactic:
exact interior_subset (hf _ <| subset_closure hi)

Premises used: interior_subset, subset_closure
-- Module: Mathlib.Analysis.Convex.PartitionOfUnity
Goal:
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : NormalSpace X
inst_4 : ParacompactSpace X
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
H : ∀ (x : X), ∃ (c : E), ∀ᶠ (y : X) in 𝓝 x, c ∈ t y
⊢ ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)

Tactic:
exists_continuous_forall_mem_convex_of_local ht fun x =>
    let ⟨c, hc⟩ := H x
    ⟨_, hc, fun _ => c, continuousOn_const, fun _ => id⟩

Premises used: exists_continuous_forall_mem_convex_of_local, setOf, Membership.mem, Exists, continuousOn_const, nhds, id, And, _private.0.exists_continuous_forall_mem_convex_of_local_const.match_1, And.intro, Exists.intro, ContinuousOn
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
dsimp : Continuous.{0, u_1} (Y := E) fun (t : (↑I : Type)) ↦ (↑t : ℝ) • (b - a) + a
⊢ Continuous.{0, u_1} (Y := E) fun (t : (↑I : Type)) ↦ (lineMap a b : (a : ℝ) → E) (↑t : ℝ)

Tactic:
dsimp [lineMap]

Premises used: AffineMap.lineMap
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
⊢ Continuous.{0, u_1} (Y := E) fun (t : (↑I : Type)) ↦ (↑t : ℝ) • (b - a) + a

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
⊢ (lineMap a b : (a : ℝ) → E) (↑0 : ℝ) = a

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
⊢ (lineMap a b : (a : ℝ) → E) (↑1 : ℝ) = b

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
rw :
  Eq (α := Set E) (range (ι := (↑I : Type)) (⇑(Path.segment a b) : (a : (↑I : Type)) → E))
    (range fun (x : (↑(Icc 0 1) : Type)) ↦ (lineMap a b : (a : ℝ) → E) (↑x : ℝ))
⊢ range (ι := (↑I : Type)) (⇑(Path.segment a b) : (a : (↑I : Type)) → E) = [a -[ℝ] b]

Tactic:
rw [segment_eq_image_lineMap, image_eq_range]

Premises used: Set.image_eq_range, segment_eq_image_lineMap
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
⊢ Eq (α := Set E) (range (ι := (↑I : Type)) (⇑(Path.segment a b) : (a : (↑I : Type)) → E))
    (range fun (x : (↑(Icc 0 1) : Type)) ↦ (lineMap a b : (a : ℝ) → E) (↑x : ℝ))

Tactic:
simp only [← segment_apply]

Premises used: Path.segment_apply
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a : E
a₁ :
  ∀ (x : (↑I : Type)),
    Eq (α := E) ((Path.segment a a : (a : (↑I : Type)) → E) x : E) ((refl a : (a : (↑I : Type)) → E) x : E)
⊢ Eq (α := Path a a) (Path.segment a a) (refl a)

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a : E
x : (↑I : Type)
⊢ Eq (α := E) ((Path.segment a a : (a : (↑I : Type)) → E) x : E) ((refl a : (a : (↑I : Type)) → E) x : E)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
a₁ :
  ∀ (x : (↑I : Type)),
    Eq (α := E) ((symm (Path.segment a b) : (a : (↑I : Type)) → E) x : E)
      ((Path.segment b a : (a : (↑I : Type)) → E) x : E)
⊢ Eq (α := Path b a) (symm (Path.segment a b)) (Path.segment b a)

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
x : (↑I : Type)
⊢ Eq (α := E) ((symm (Path.segment a b) : (a : (↑I : Type)) → E) x : E)
    ((Path.segment b a : (a : (↑I : Type)) → E) x : E)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b c d : E
a₁ :
  ∀ (x : (↑I : Type)),
    Eq (α := E) ((Path.add (Path.segment a b) (Path.segment c d) : (a : (↑I : Type)) → E) x : E)
      ((Path.segment (a + c) (b + d) : (a : (↑I : Type)) → E) x : E)
⊢ Eq (α := Path (a + c) (b + d)) (Path.add (Path.segment a b) (Path.segment c d)) (Path.segment (a + c) (b + d))

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b c d : E
x : (↑I : Type)
⊢ Eq (α := E) ((Path.add (Path.segment a b) (Path.segment c d) : (a : (↑I : Type)) → E) x : E)
    ((Path.segment (a + c) (b + d) : (a : (↑I : Type)) → E) x : E)

Tactic:
simp [lineMap_apply_module, add_add_add_comm]

Premises used: AffineMap.lineMap_apply_module, add_add_add_comm
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b c d : E
hac : c = a
hbd : d = b
subst_vars : Eq (α := Path c d) (cast (Path.segment c d) ⋯ ⋯) (Path.segment c d)
⊢ Eq (α := Path c d) (cast (Path.segment a b) hac hbd) (Path.segment c d)

Tactic:
subst_vars
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
c d : E
⊢ Eq (α := Path c d) (cast (Path.segment c d) ⋯ ⋯) (Path.segment c d)

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
t : ℝ
ht : t ∈ I
⊢ Eq (α := E) ((extend (Path.segment a b) : (a : ℝ) → E) t : E) ((lineMap a b : (a : ℝ) → E) t : E)

Tactic:
simp [ht]
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
hne : a ≠ b
⊢ Function.Injective (α := (↑I : Type)) (β := E) (⇑(Path.segment a b) : (a : (↑I : Type)) → E)

Tactic:
(lineMap_injective _ hne).comp Subtype.coe_injective

Premises used: AffineMap.lineMap_injective, Subtype.coe_injective, Function.Injective.comp
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x -[ℝ] y] ⊆ s
h₁ : ∀ (t : (↑I : Type)), Membership.mem (α := E) s ((Path.segment x y : (a : (↑I : Type)) → E) t : E)
⊢ JoinedIn s x y

Tactic:
use .segment x y
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x -[ℝ] y] ⊆ s
h₁ : range (ι := (↑I : Type)) (⇑(Path.segment x y) : (a : (↑I : Type)) → E) ⊆ s
h₂ h₃ h₄ h₅ : [x -[ℝ] y] ⊆ s
⊢ ∀ (t : (↑I : Type)), Membership.mem (α := E) s ((Path.segment x y : (a : (↑I : Type)) → E) t : E)

Tactic:
rwa [← range_subset_iff, Path.range_segment]

Premises used: Path.range_segment, Set.range_subset_iff
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
s : Set E
a : E
h : StarConvex ℝ a s
ha : a ∈ s
⊢ IsPathConnected s

Tactic:
⟨a, ha, fun _y hy ↦ .of_segment_subset <| h.segment_subset hy⟩

Premises used: IsPathConnected, StarConvex.segment_subset, And.intro, Exists.intro, JoinedIn.of_segment_subset
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : s.Nonempty
⊢ IsPathConnected s

Tactic:
let ⟨_a, ha⟩ := hne; (hconv ha).isPathConnected ha

Premises used: IsPathConnected, StarConvex.isPathConnected, _private.0.Convex.isPathConnected.match_1
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
s : Set E
h : Convex ℝ s
hne : s.Nonempty
⊢ IsConnected s

Tactic:
(h.isPathConnected hne).isConnected

Premises used: IsPathConnected.isConnected, Convex.isPathConnected
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
s : Set E
h : Convex ℝ s
⊢ IsPreconnected s

Tactic:
s.eq_empty_or_nonempty.elim (fun h => h.symm ▸ isPreconnected_empty) fun hne =>
    (h.isConnected hne).isPreconnected

Premises used: Convex.isConnected, Eq.rec, Set.eq_empty_or_nonempty, IsConnected.isPreconnected, isPreconnected_empty, Or.elim, Eq.symm
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
s : Submodule ℝ E
⊢ IsPathConnected (↑s : Set E)

Tactic:
s.convex.isPathConnected s.nonempty

Premises used: Convex.isPathConnected, Submodule.convex, Submodule.nonempty
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
⊢ PathConnectedSpace E

Tactic:
pathConnectedSpace_iff_univ.mpr <| convex_univ.isPathConnected ⟨(0 : E), trivial⟩

Premises used: Iff.mpr, trivial, Convex.isPathConnected, convex_univ, pathConnectedSpace_iff_univ, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected (X := ↥p) {0}ᶜ
⊢ IsPathConnected (image (α := ↥p) (Subtype.val (p := fun (x : E) ↦ x ∈ p)) {0}ᶜ + (↑q : Set E))

Tactic:
(hpc.image continuous_subtype_val).add q.isPathConnected

Premises used: IsPathConnected.add, continuous_subtype_val, IsPathConnected.image, Submodule.isPathConnected
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected (X := ↥p) {0}ᶜ
h : (↑q : Set E)ᶜ = image (α := ↥p) (Subtype.val (p := fun (x : E) ↦ x ∈ p)) {0}ᶜ + (↑q : Set E)
⊢ IsPathConnected (↑q : Set E)ᶜ

Tactic:
convert! (hpc.image continuous_subtype_val).add q.isPathConnected using 1

Premises used: IsPathConnected.add, continuous_subtype_val, IsPathConnected.image, Submodule.isPathConnected
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected (X := ↥p) {0}ᶜ
trans :
  (↑q : Set E)ᶜ =
    (⇑(p.prodEquivOfIsCompl q hpq) : (a : ↥p × ↥q) → E) '' SProd.sprod (α := Set ↥p) (β := Set ↥q) {0}ᶜ univ
trans₁ :
  (⇑(p.prodEquivOfIsCompl q hpq) : (a : ↥p × ↥q) → E) '' SProd.sprod (α := Set ↥p) (β := Set ↥q) {0}ᶜ univ =
    image (α := ↥p) (Subtype.val (p := fun (x : E) ↦ x ∈ p)) {0}ᶜ + (↑q : Set E)
⊢ (↑q : Set E)ᶜ = image (α := ↥p) (Subtype.val (p := fun (x : E) ↦ x ∈ p)) {0}ᶜ + (↑q : Set E)

Tactic:
trans Submodule.prodEquivOfIsCompl p q hpq '' ({0}ᶜ ×ˢ univ)

Premises used: Submodule.prodEquivOfIsCompl, SProd.sprod, Compl.compl, Set.univ, Singleton.singleton, OfNat.ofNat