mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ { toFun := fun a ↦ f a, invFun := fun a ↦ (f.symm a).bind ⇑(PEquiv.refl α), inv := ⋯ } x✝ = some a✝ ↔ f x✝ = some a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (some x) = x

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
⊢ (a ∈ if b ∈ s then some b else none) ↔ a = b ∧ a ∈ s

Tactic:
grind

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | (f a).isSome = true}) ↔ ∀ (a : α), (f a).isSome = true

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(ConcreteCategory.hom (F.map f))
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
k m : J
mi : m ⟶ i
h : (ConcreteCategory.hom (F.map (mi ≫ f))) (↑s₀ m) = (ConcreteCategory.hom (F.map (mi ≫ f))) (↑s₁ m)
mk : m ⟶ k
h✝ : True
⊢ (ConcreteCategory.hom (F.map mk)) (↑s₀ m) = (ConcreteCategory.hom (F.map mk)) (↑s₁ m)

Tactic:
exact congr_arg _ (Finj m (mi ≫ f) h)

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f g : α ≃. β
a : α
b : β
hf : f.symm b = some a ↔ f a = some b
hg : g.symm b = some a ↔ g a = some b
⊢ (if f.symm b = g.symm b then f.symm b else none) = some a ↔ (if f a = g a then f a else none) = some b

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
⊢ (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1 ↔
    ((∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1) ∧ (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
σ : Equiv.Perm n
⊢ Equiv.Perm.permMatrix R σ ∈ doublyStochastic R n

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
⊢ Mᵀ ∈ doublyStochastic R n ↔ M ∈ doublyStochastic R n

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
hM : M ∈ doublyStochastic R n
⊢ (reindex e₁ e₂) M ∈ doublyStochastic R m

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
⊢ (reindex e₁ e₂) M ∈ doublyStochastic R m ↔ M ∈ doublyStochastic R n

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
x : n → R
hA : M ∈ doublyStochastic R n
⊢ M ∈ colStochastic R n

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ : Fin 3
h₁₂ : i₁ ≠ i₂
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
i : Fin 3
h₁₃ : i₁ ≠ i
h₂₃ : i₂ ≠ i
h3 : ∀ (i_1 : Fin 3), i_1 = i₁ ∨ i_1 = i₂ ∨ i_1 = i
hu : Finset.univ = {i₁, i₂, i}
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i)) r₁) (t.points i)
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i)) r₂) (t.points i)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i)
h₂s : SignType.sign (w i₁) = SignType.sign (w i)
⊢ SignType.sign (w i) = SignType.sign (w i)

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: case inl
V : Type u_1
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup V
inst✝¹ : Module ℝ V
inst✝ : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ 0 • ↑K ⊆ b • ↑K

pp: case inr
V : Type u_1
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup V
inst✝¹ : Module ℝ V
inst✝ : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
⊢ a • ↑K ⊆ b • ↑K

Tactic:
· rw [Set.zero_smul_set K.nonempty, Set.zero_subset]
    exact Set.mem_smul_set.mpr ⟨0, h_zero, smul_zero _⟩

Goal state after:
case inr
V : Type u_1
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup V
inst✝¹ : Module ℝ V
inst✝ : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
⊢ a • ↑K ⊆ b • ↑K
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : r ∈ Set.Ici 1
⊢ Wbtw R x y ((lineMap x y) r)

Tactic:
Set.mem_Ici

Goal state after:
case refine_2.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ Wbtw R x y ((lineMap x y) r)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : r ∈ Set.Ici 1
h : Sbtw R x y ((lineMap x y) r)
⊢ (lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioi 1

Tactic:
Set.mem_Ici

Goal state after:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y ((lineMap x y) r)
⊢ (lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioi 1
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ ∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i, w i = 1 ∧ ∑ i, w i • z i = x

Tactic:
by
  rw [convexHull_eq_union] at hx
  simp only [exists_prop, Set.mem_iUnion] at hx
  obtain ⟨t, ht₁, ht₂, ht₃⟩ := hx
  simp only [t.convexHull_eq, Set.mem_ofPred_eq] at ht₃
  obtain ⟨w, hw₁, hw₂, hw₃⟩ := ht₃
  let t' := {i ∈ t | w i ≠ 0}
  refine ⟨t', t'.fintypeCoeSort, ((↑) : t' → E), w ∘ ((↑) : t' → E), ?_, ?_, ?_, ?_, ?_⟩
  · rw [Subtype.range_coe_subtype]
    exact Subset.trans (Finset.filter_subset _ t) ht₁
  · exact ht₂.comp_embedding ⟨_, inclusion_injective (Finset.filter_subset (fun i => w i ≠ 0) t)⟩
  · exact fun i =>
      (hw₁ _ (Finset.mem_filter.mp i.2).1).lt_of_ne (Finset.mem_filter.mp i.property).2.symm
  · simp only [univ_eq_attach, Function.comp_apply]
    rw [Finset.sum_attach, Finset.sum_filter_ne_zero, hw₂]
  · change (∑ i ∈ t'.attach, (fun e => w e • e) ↑i) = x
    rw [Finset.sum_attach (f := fun e => w e • e), Finset.sum_filter_of_ne]
    · rw [t.centerMass_eq_of_sum_1 id hw₂] at hw₃
      exact hw₃
    · intro e _ hwe contra
      apply hwe
      rw [contra, zero_smul]

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_1.right.h
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
⊢ t₁ * t₂ ≤ 1 - t₁ + t₁ * t₂

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ (lineMap w z) (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) = x

Tactic:
rw [← hy, lineMap_apply, lineMap_apply, eq_comm, eq_vadd_iff_vsub_eq] at hx

Goal state after:
case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ (lineMap w z) (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) = x
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
x : E
hx : x ∈ B
⊢ x ∈ A

Tactic:
obtain ⟨_, rfl⟩ := hAB ⟨x, hx⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
w✝ : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, w✝ y ≤ w✝ x}
hx : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, w✝ y ≤ w✝ x}
⊢ x ∈ A
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}.Nonempty
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∧ a ≤ l_1 x}

Tactic:
obtain ⟨w, hw⟩ := hB

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
w : E
hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∧ a ≤ l_1 x}
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∃ l a, ∅ = {x | x ∈ A ∧ a ≤ l x}

Tactic:
refine ⟨0, 1, ?_⟩
    rw [eq_comm, eq_empty_iff_forall_notMem]
    rintro x ⟨-, h⟩
    rw [zero_apply] at h
    have : ¬(1 : 𝕜) ≤ 0 := not_le_of_gt zero_lt_one
    contradiction

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:

Tactic:
(fun a ↦ y + h (-x + a)) '' closure s = y +ᵥ h '' closure (-x +ᵥ s) := by
        simp_rw [closure_vadd, ← image_vadd, image_image, vadd_eq_add]
      _ = _ := by rw [image_gaugeRescaleHomeomorph_closure, closure_vadd, vadd_neg_vadd]

Goal state after:
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
x : E
hx : x ∈ C
this : ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
δ : ℝ
hδ₀ : 0 < δ
hδ₁ : δ < 1
y : E := ⋯
hy : y ∈ C
hr✝ : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
ε : ℝ
hε : ε > 0
hr : ∀ ⦃y : E⦄, dist y x₀ < ε → f y ≤ r ∧ y ∈ C
z : E
hz : dist z x < ε * δ
hx₀' : δ⁻¹ • (x - y) + y = x₀
w : E := ⋯
hwyz : δ • w + (1 - δ) • y = z
hw : dist w x₀ < ε
⊢ f w ≤ r

Tactic:
exact (hr hw).1

Goal state after:
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ f '' Subtype.val '' interior (Subtype.val ⁻¹' s) = f '' intrinsicInterior 𝕜 s

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ f '' Subtype.val '' frontier (Subtype.val ⁻¹' s) = f '' intrinsicFrontier 𝕜 s

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ f '' Subtype.val '' closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s) = f '' intrinsicClosure 𝕜 s

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
this : ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z)
hx : y ∈ Icc y z
⊢ Icc y z ⊆ Ici y

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y : ℝ
hfy : ContinuousWithinAt f (Ici y) y
x : ℝ
hyx : y < x
hf_cvx : ConvexOn ℝ (Icc y x) f
hyz : y < x
hfz : ContinuousWithinAt f (Iic x) x
this : ContinuousOn f (Ico y x) ∧ ContinuousOn f (Ioc y x)
hx : x ∈ Icc y x
⊢ Icc y x ⊆ Iic x

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
this : ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z)
x : ℝ
hx : x ∈ Icc y z
hyx : y < x
hxz : x < z
⊢ x ∈ Ico y z

Tactic:
grind

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
s : Set X
hs : IsStarConvexSet R x s
hs₀ : s.Nonempty
⊢ x ∈ s

Tactic:
obtain ⟨y, hy⟩ := hs₀; simpa using hs hy zero_le_one le_rfl (add_zero _)

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
x : X
s : Set Y
hf : IsAffineMap R f
hs : IsStarConvexSet R (f x) s
y : X
hy : y ∈ f ⁻¹' s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ convexCombPair a b ha hb hab x y ∈ f ⁻¹' s

Tactic:
simpa [mem_preimage, hf.map_convexCombPair] using hs hy _ ..

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s : StdSimplex R P
⊢ sConvexComb s = (Finset.affineCombination R s.weights.support id) ⇑s.weights

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ (s • (x -ᵥ y) + (Finsupp.single y t).sum fun p w ↦ w • (p -ᵥ y)) = s • (x -ᵥ y)

Tactic:
Finsupp.sum_single_index (by simp)

Goal state after:
case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ s • (x -ᵥ y) + t • (y -ᵥ y) = s • (x -ᵥ y)
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
⊢ IsConvexSet R (f '' s)

Tactic:
rintro w hw
  obtain ⟨u, hus, hfu, huw⟩ := Finset.exists_subset_injOn_image_eq_of_surjOn _ _ hw
  refine ⟨sConvexComb {
      weights := .onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) <| by simp +contextual
      nonneg x := by simp; split <;> simp
      total := by
        simp only [implies_true, sum_onFinset, Finset.sum_ite_mem, Finset.inter_self,
        ← Finset.sum_image hfu, huw]
        exact w.total
    }, hs.sConvexComb_mem <| by grw [support_onFinset_subset, hus], ?_⟩
  rw [hf.map_sConvexComb]
  congr
  ext y
  rw [StdSimplex.weights_map]
  by_cases hy : y ∈ w.weights.support
  · rw [← huw, Finset.mem_image] at hy
    obtain ⟨x, hx, rfl⟩ := hy
    convert mapDomain_apply' _ _ support_onFinset_subset hfu hx
    exact (if_pos hx).symm
  · rw [mapDomain_of_not_mem_image_support (by simp [← huw] at ⊢ hy; tauto)]
    simp_all

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t✝ : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄, ↑t ⊆ s → t = w.weights.support → sConvexComb w ∈ s
w : StdSimplex K X
hw : ↑(Finset.cons x t hx) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : w.weights x ≠ 0
hwx' : ∃ y, y ≠ x ∧ w.weights y ≠ 0
⊢ t = {x_1 ∈ insert x t | ¬x_1 = x}

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.Quasiconvex

Goal state before:
pp: case inr
𝕜 : Type u_4
E : Type u_5
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
this :
  ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
    [inst_3 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_4 : LinearOrder β] [inst_5 : Preorder γ] {s : Set E}
    {f : E → β} {g : β → γ},
    Monotone g →
      QuasiconvexOn 𝕜 s f →
        ∀ (c : γ) (x : E),
          x ∈ s ∧ g (f x) ≤ c →
            ∀ (y : E),
              y ∈ s ∧ g (f y) ≤ c →
                ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f x ≤ f y → a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
h : ¬f x ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.Piecewise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : LinearOrder E
inst✝⁷ : IsOrderedAddMonoid E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : PosSMulMono 𝕜 E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConcaveOn 𝕜 (Set.Iic e) f
hg : ConcaveOn 𝕜 (Set.Ici e) g
h_mono : MonotoneOn f (Set.Iic e)
h_anti : AntitoneOn g (Set.Ici e)
h_eq : f e = g e
⊢ ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (-f) (-g))

Tactic:
exact convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici
    hf.neg hg.neg h_mono.neg h_anti.neg (neg_inj.mpr h_eq)

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
a : X
⊢ t' = s - s' + t

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
D : ℝ
t : T
hx : ContinuousOn x (f ⁻¹' {0})ᶜ
hy : ContinuousOn y (f ⁻¹' {1})ᶜ
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
ht : 0 < f t ∧ f t < 1
⊢ ∀ (a : T), 0 < f a → f a < 1 → ¬f a = 0

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
D : ℝ
t : T
hx : ContinuousOn x (f ⁻¹' {0})ᶜ
hy : ContinuousOn y (f ⁻¹' {1})ᶜ
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
ht : 0 < f t ∧ f t < 1
⊢ ∀ (a : T), 0 < f a → f a < 1 → ¬f a = 1

Tactic:
grind

Goal state after: