mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ log ‖meromorphicTrailingCoeffAt (fun x ↦ -a + f x) 0‖ = 0

Tactic:
rw [(meromorphicAt_of_meromorphicOrderAt_ne_zero
    h.ne').meromorphicTrailingCoeffAt_fun_add_eq_left_of_lt]

Goal state after:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ log ‖meromorphicTrailingCoeffAt (fun x ↦ -a) 0‖ = 0

f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt (fun x ↦ -a) 0 < meromorphicOrderAt f 0
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ log⁺ ‖f θ‖ + log⁺ ‖a₀‖ = log⁺ ‖-f θ‖ + log⁺ ‖a₀‖

Tactic:
· simp

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
this : Measurable f
⊢ Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (uIoc 0 (2 * π))).prod (volume.restrict (uIoc 0 (2 * π))))

Tactic:
simpa [uIoc_of_le two_pi_pos.le] using (integrable_prod_iff' (by fun_prop)).2
    ⟨Eventually.of_forall (integrableOn_cartanKernel_left f R),
      integrable_integral_norm_cartanKernel h⟩

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ 1 ≤ 1 + ℓ

Tactic:
by grind

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
yz : y ≤ z
⊢ HasConstantSpeedOnWith f (Icc x z) l

Tactic:
rw [← Set.Icc_union_Icc_eq_Icc xy yz]

Goal state after:
case inl.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
yz : y ≤ z
⊢ HasConstantSpeedOnWith f (Icc x y ∪ Icc y z) l
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s l
hf : HasConstantSpeedOnWith f (φ '' s) l'
x : ℝ
xs : x ∈ s
⊢ EqOn φ (fun y ↦ ↑l / ↑l' * (y - x) + φ x) s

Tactic:
rintro y ys

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s l
hf : HasConstantSpeedOnWith f (φ '' s) l'
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ φ y = (fun y ↦ ↑l / ↑l' * (y - x) + φ x) y
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l : List α
p : α → α → α → Prop
⊢ Triplewise p l ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < l.length), p l[i] l[j] l[k]

Tactic:
induction l with
  | nil => simp
  | cons head tail ih =>
    simp only [triplewise_cons, length_cons, pairwise_iff_getElem, ih]
    refine ⟨fun ⟨hh, ht⟩ i j k hij hjk hk ↦ ?_,
            fun h ↦ ⟨fun i j hi hj hij ↦ ?_, fun i j k hij hjk hk ↦ ?_⟩⟩
    · grind
    · simpa using! h 0 (i + 1) (j + 1) (by lia) (by lia) (by lia)
    · simpa using! h (i + 1) (j + 1) (k + 1) (by lia) (by lia) (by lia)

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
cb : c ≤ b
⊢ eVariationOn (naturalParameterization f s a)
      (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) =
    ENNReal.ofReal (↑1 * (variationOnFromTo f s a c - variationOnFromTo f s a b))

Tactic:
rw [NNReal.coe_one, one_mul, le_antisymm h (variationOnFromTo.monotoneOn hf as cs bs cb),
      sub_self, ENNReal.ofReal_zero, Icc_self, eVariationOn.subsingleton]
    exact fun x hx y hy => hx.2.trans hy.2.symm

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
s' : Finset ↑{x' | x' ≠ x}
⊢ #s' ≤ #(s'.biUnion fun x' ↦ (t ↑x').erase a)

Tactic:
have := Classical.decEq ι
  specialize ha (s'.image fun z => z.1)
  rw [image_nonempty, Finset.card_image_of_injective s' Subtype.coe_injective] at ha
  by_cases! he : s'.Nonempty
  · have ha' : #s' < #(s'.biUnion fun x => t x) := by
      convert! ha he fun h => by simpa [← h] using mem_univ x using 2
      ext x
      simp only [mem_image, mem_biUnion, SetCoe.exists, exists_and_right,
        exists_eq_right]
    rw [← erase_biUnion]
    by_cases hb : a ∈ s'.biUnion fun x => t x
    · rw [card_erase_of_mem hb]
      exact Nat.le_sub_one_of_lt ha'
    · rw [erase_eq_of_notMem hb]
      exact Nat.le_of_lt ha'
  · subst s'
    simp

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

Goal state before:
pp: s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
l : ℝ →L[ℝ] ℝ
c' : ℝ
hlc'_le : s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c' ≤ s.domRestrict f
hlc'_eq : re (l x) + c' = a
⊢ ∃ c c', (∀ y ∈ s, c * y + c' ≤ f y) ∧ c * x + c' = a

Tactic:
have h1 y : l 1 * y = l y := by rw [mul_comm, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one]

Goal state after:
s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
l : ℝ →L[ℝ] ℝ
c' : ℝ
hlc'_le : s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c' ≤ s.domRestrict f
hlc'_eq : re (l x) + c' = a
h1 : ∀ (y : ℝ), l 1 * y = l y
⊢ ∃ c c', (∀ y ∈ s, c * y + c' ≤ f y) ∧ c * x + c' = a
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case inl
f : ℝ → ℝ
hsc : IsClosed ∅
hfc : LowerSemicontinuousOn f ∅
hf : ConvexOn ℝ ∅ f
⊢ ∃ c c', ∀ x ∈ ∅, c * x + c' ≤ f x

pp: case inr
s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
x : ℝ
hxs : x ∈ s
⊢ ∃ c c', ∀ x ∈ s, c * x + c' ≤ f x

Tactic:
· simp

Goal state after:
case inr
s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
x : ℝ
hxs : x ∈ s
⊢ ∃ c c', ∀ x ∈ s, c * x + c' ≤ f x
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
⊢ φ hs.some - 1 < φ ↑⟨hs.some, ⋯⟩

Tactic:
by 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✝¹¹ : Ring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddTorsor V P
inst✝⁶ : ZeroLEOneClass R
R' : Type u_6
inst✝⁵ : Ring R'
inst✝⁴ : PartialOrder R'
inst✝³ : Module R' V
inst✝² : Module R' R
inst✝¹ : IsScalarTower R' R V
inst✝ : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ a • 1 ≤ 1

Tactic:
← one_smul R' 1

Goal state after:
case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝¹¹ : Ring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddTorsor V P
inst✝⁶ : ZeroLEOneClass R
R' : Type u_6
inst✝⁵ : Ring R'
inst✝⁴ : PartialOrder R'
inst✝³ : Module R' V
inst✝² : Module R' R
inst✝¹ : IsScalarTower R' R V
inst✝ : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ a • 1 ≤ 1 • 1
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
X Y : J
f : X ⟶ Y
⊢ X ∈ {X, Y}

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
X Y : J
f : X ⟶ Y
⊢ Y ∈ {X, Y}

Tactic:
by grind

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
⊢ φ 0 - 1 < φ ↑⟨0, ⋯⟩

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x ↦ x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
hb : ¬b ∈ s
ha : ¬a ∈ s
⊢ False ↔ False

Tactic:
· simp

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
h : ∀ (j : J), ∃ i f, (range ⇑(ConcreteCategory.hom (F.map f))).Finite
j i✝ : J
hi : i✝ ⟶ j
hf : (range ⇑(ConcreteCategory.hom (F.map hi))).Finite
m : Finset (F.obj j)
hmin : ∀ x ∈ {s | ∃ i f, ↑s = range ⇑(ConcreteCategory.hom (F.map f))}, ¬x ⊂ m
i : J
f : i ⟶ j
hm : ↑m = range ⇑(ConcreteCategory.hom (F.map f))
k : J
g : k ⟶ j
k' : J
g' : k' ⟶ j
hl :
  (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k', g'⟩ ⊆
    (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, f⟩
this : ¬⋯.toFinset ⊂ m
⊢ ¬(fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k', g'⟩ ⊂
      (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, f⟩

Tactic:
← Finset.coe_ssubset,

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), ∃ i f, (range ⇑(ConcreteCategory.hom (F.map f))).Finite
j i✝ : J
hi : i✝ ⟶ j
hf : (range ⇑(ConcreteCategory.hom (F.map hi))).Finite
m : Finset (F.obj j)
hmin : ∀ x ∈ {s | ∃ i f, ↑s = range ⇑(ConcreteCategory.hom (F.map f))}, ¬x ⊂ m
i : J
f : i ⟶ j
hm : ↑m = range ⇑(ConcreteCategory.hom (F.map f))
k : J
g : k ⟶ j
k' : J
g' : k' ⟶ j
hl :
  (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k', g'⟩ ⊆
    (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, f⟩
this : ¬↑⋯.toFinset ⊂ ↑m
⊢ ¬(fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k', g'⟩ ⊂
      (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, f⟩
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h✝ : ¬x = a
⊢ False ↔ False

Tactic:
· simp

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case none
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
h : f i = none
⊢ ∑ j_1, (if j_1 ∈ none then 1 else 0) * M j_1 j = Option.rec 0 (fun val ↦ M val j) none

pp: case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
fi : m
h : f i = some fi
⊢ ∑ j_1, (if j_1 ∈ some fi then 1 else 0) * M j_1 j = Option.rec 0 (fun val ↦ M val j) (some fi)

Tactic:
· simp

Goal state after:
case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
fi : m
h : f i = some fi
⊢ ∑ j_1, (if j_1 ∈ some fi then 1 else 0) * M j_1 j = Option.rec 0 (fun val ↦ M val j) (some fi)
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case some.h₁
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ fj ∉ Finset.univ → (M i fj * if j ∈ f fj then 1 else 0) = 0

Tactic:
· simp

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✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
⊢ 1 ᵥ* (M * N) = 1

Tactic:
rw [← vecMul_vecMul, hM.2.2, hN.2.2]

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:
by 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:
by grind

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

Goal state before:
pp: case refine_1.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 z : P
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ x = (lineMap x z) 0 ∨ z ∈ ⇑(lineMap x ((lineMap x z) 0)) '' Set.Ici 1

Tactic:
· simp

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

Goal state before:
pp: case inl.inr.inl
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 : P
v : V
ty : R
hy0 : ty < 0
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = 0 • v +ᵥ x → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x (ty • v +ᵥ x) (0 • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (0 • v +ᵥ x) x ∨ Wbtw R (0 • v +ᵥ x) x (ty • v +ᵥ x)

pp: case inl.inr.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 : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
· simp

Goal state after:
case inl.inr.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 : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr.inl
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 : P
v : V
tz : R
h : ∀ (p : P), p = x ∨ p = 0 • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x (0 • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (0 • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (0 • v +ᵥ x)

pp: case inr.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 : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
· simp

Goal state after:
case inr.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 : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr.inr.inr.inl
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 : P
v : V
ty : R
hy0 : 0 < ty
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = 0 • v +ᵥ x → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x (ty • v +ᵥ x) (0 • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (0 • v +ᵥ x) x ∨ Wbtw R (0 • v +ᵥ x) x (ty • v +ᵥ x)

pp: case inr.inr.inr.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 : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
· simp

Goal state after:
case inr.inr.inr.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 : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s✝ t : Set M
y : N
s : Set M
u v : N
hu : u ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
hv : v ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
x : M
hx : x ∈ s
⊢ 0 ≤ (p x) (u + v)

Tactic:
by rw [map_add]; exact add_nonneg (hu hx) (hv hx)

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

Goal state before:
pp: case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
⊢ gaugeRescale s s 0 = 0

pp: case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
hx : x ≠ 0
⊢ gaugeRescale s s x = x

Tactic:
· simp

Goal state after:
case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
hx : x ≠ 0
⊢ gaugeRescale s s x = x
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
⊢ gauge t (gaugeRescale s t 0) = gauge s 0

pp: case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
· simp

Goal state after:
case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t (gaugeRescale s t x) = gauge s x
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
⊢ gaugeRescale t u (gaugeRescale s t 0) = gaugeRescale s u 0

pp: case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x

Tactic:
· simp

Goal state after:
case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x : E
hx hy : x ∈ ball x₀ (r - ε)
⊢ f x - f x ≤ K * ‖x - x‖

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hxy : x ≠ y
⊢ f x - f y ≤ K * ‖x - y‖

Tactic:
· simp

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hxy : x ≠ y
⊢ f x - f y ≤ K * ‖x - y‖
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✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
hAB : IsExposed 𝕜 A ∅
⊢ IsClosed ∅

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
hB : B.Nonempty
⊢ IsClosed B

Tactic:
· simp

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
hB : B.Nonempty
⊢ IsClosed B