mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map f ↑b

Tactic:
exact le_rfl

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

Goal state before:
pp: case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
⊢ circleAverage (fun x ↦ log⁺ ‖f x‖) 0 r = circleAverage (fun x ↦ log⁺ ‖g x‖) 0 r

Tactic:
apply circleAverage_congr_codiscreteWithin _ hr

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
⊢ (fun x ↦ log⁺ ‖f x‖) =ᶠ[codiscreteWithin (sphere 0 |r|)] fun x ↦ log⁺ ‖g x‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
⊢ circleAverage (fun x ↦ log⁺ ‖f x - a.untop₀‖⁻¹) 0 r = circleAverage (fun x ↦ log⁺ ‖g x - a.untop₀‖⁻¹) 0 r

Tactic:
apply circleAverage_congr_codiscreteWithin _ hr

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
⊢ (fun x ↦ log⁺ ‖f x - a.untop₀‖⁻¹) =ᶠ[codiscreteWithin (sphere 0 |r|)] fun x ↦ log⁺ ‖g x - a.untop₀‖⁻¹
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 ↦ f x - a) 0‖ = 0

Tactic:
sub_eq_neg_add

Goal state after:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ log ‖meromorphicTrailingCoeffAt (fun x ↦ -a + f x) 0‖ = 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case pos
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R = 0
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) R) 0 1

pp: case neg
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : ¬R = 0
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) R) 0 1

Tactic:
· simp [hR, ValueDistribution.logCounting_eval_zero]

Goal state after:
case neg
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : ¬R = 0
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) R) 0 1
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l ↔
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))

Tactic:
by
  refine ⟨fun h x xs y ys _ => h xs ys, fun h x xs y ys => ?_⟩
  rcases le_total x y with (xy | yx)
  · exact h xs ys xy
  · rw [eVariationOn.subsingleton, ENNReal.ofReal_of_nonpos]
    · exact mul_nonpos_of_nonneg_of_nonpos l.prop (sub_nonpos_of_le yx)
    · rintro z ⟨zs, xz, zy⟩ w ⟨ws, xw, wy⟩
      cases le_antisymm (zy.trans yx) xz
      cases le_antisymm (wy.trans yx) xw
      rfl

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
⊢ logCounting D 0 = 0

Tactic:
by
  simp [logCounting]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
h : f₁ ≤ f₂
⊢ logCounting f₁ ≤ᶠ[atTop] logCounting f₂

Tactic:
filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ logCounting_le h hr

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a₀ : E
⊢ logCounting f ↑a₀ = locallyFinsuppWithin.logCounting (divisor (fun x ↦ f x - a₀) univ)⁺

Tactic:
by
  simp [logCounting]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a₀ : E
⊢ logCounting f ↑a₀ = logCounting (f - fun x ↦ a₀) 0

Tactic:
by
  simp [logCounting]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ logCounting f 0 = locallyFinsuppWithin.logCounting (divisor f univ)⁺

Tactic:
by
  simp [logCounting]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ logCounting f ⊤ = locallyFinsuppWithin.logCounting (divisor f univ)⁻

Tactic:
by
  simp [logCounting]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : E
e : WithTop E
⊢ logCounting (fun x ↦ c) e = 0

Tactic:
by
  simp [logCounting]

Goal state after:
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
y : ℝ
ys : y ∈ s
⊢ (φ y - φ x) * ↑l' = (y - x) * ↑l

Tactic:
hasConstantSpeedOnWith_iff_variationOnFromTo_eq

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 :
  LocallyBoundedVariationOn f (φ '' s) ∧
    ∀ ⦃x : ℝ⦄, x ∈ φ '' s → ∀ ⦃y : ℝ⦄, y ∈ φ '' s → variationOnFromTo f (φ '' s) x y = ↑l' * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ (φ y - φ x) * ↑l' = (y - x) * ↑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 :
  LocallyBoundedVariationOn f (φ '' s) ∧
    ∀ ⦃x : ℝ⦄, x ∈ φ '' s → ∀ ⦃y : ℝ⦄, y ∈ φ '' s → variationOnFromTo f (φ '' s) x y = ↑l' * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ (φ y - φ x) * ↑l' = (y - x) * ↑l

Tactic:
hasConstantSpeedOnWith_iff_variationOnFromTo_eq

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ :
  LocallyBoundedVariationOn (f ∘ φ) s ∧
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo (f ∘ φ) s x y = ↑l * (y - x)
hf :
  LocallyBoundedVariationOn f (φ '' s) ∧
    ∀ ⦃x : ℝ⦄, x ∈ φ '' s → ∀ ⦃y : ℝ⦄, y ∈ φ '' s → variationOnFromTo f (φ '' s) x y = ↑l' * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ (φ y - φ x) * ↑l' = (y - x) * ↑l
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
⊢ ∃ z,
    (fun G ↦ partialSections F G.snd) A ⊇ (fun G ↦ partialSections F G.snd) z ∧
      (fun G ↦ partialSections F G.snd) B ⊇ (fun G ↦ partialSections F G.snd) z

Tactic:
refine ⟨⟨A.1 ⊔ B.1, A.2.image ιA ⊔ B.2.image ιB⟩, ?_, ?_⟩

Goal state after:
case refine_1
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
⊢ (fun G ↦ partialSections F G.snd) A ⊇
    (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩

case refine_2
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
⊢ (fun G ↦ partialSections F G.snd) B ⊇
    (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case a
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range ⇑(ConcreteCategory.hom (F.map g))
⊢ F.eventualRange k ⊆ range ⇑(ConcreteCategory.hom (F.map (f ≫ g)))

Tactic:
apply iInter₂_subset

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

Goal state before:
pp: case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
⊢ (fun i ↦ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i = (fun i ↦ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i' → i = i'

Tactic:
have subi : ({i} : Finset ι) ⊆ {i, i'} := by simp

Goal state after:
case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : {i} ⊆ {i, i'}
⊢ (fun i ↦ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i = (fun i ↦ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i' → i = i'
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: case h₁
𝕜 : 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 ∈ ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t

Tactic:
simp only [exists_prop, Set.mem_iUnion]

Goal state after:
case h₁
𝕜 : 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
⊢ ∃ i, ↑i ⊆ s ∧ AffineIndependent 𝕜 Subtype.val ∧ x ∈ (convexHull 𝕜) ↑i
Module: Mathlib.Analysis.Convex.Extrema

Goal state before:
pp: case inl
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
hc : a ∈ Icc a b
⊢ f a ≤ f a

Tactic:
exact le_rfl

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)
⊢ p (f x) ∈ (convexHull 𝕜) (p '' ⇑f '' s)

Tactic:
Set.image_image

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)
⊢ p (f x) ∈ (convexHull 𝕜) ((fun x ↦ p (f x)) '' s)
Module: Mathlib.Analysis.Convex.KreinMilman

Goal state before:
pp: E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
⊢ (extremePoints ℝ s).Nonempty

Tactic:
let S : Set (Set E) := { t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t }

Goal state after:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
⊢ (extremePoints ℝ s).Nonempty
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬μ t = 0
h₀' : μ tᶜ = 0
⊢ ∫ (x : α) in t, f x ∂μ = μ.real t • ⨍ (x : α), f x ∂μ

Tactic:
rw [← ae_eq_univ] at h₀'
    rw [restrict_congr_set h₀', restrict_univ, measureReal_congr h₀', measure_smul_average]

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s = ⊤
⊢ μ (frontier s) = 0

Tactic:
rw [← hs.interior_nonempty_iff_affineSpan_eq_top] at hspan

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : (interior s).Nonempty
⊢ μ (frontier s) = 0
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : IsDomain K
w : StdSimplex K X
x : X
hx : ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0
a✝ : X
⊢ a✝ ∈ {x_1 ∈ w.weights.support | x_1 = x} ↔ a✝ ∈ {x}

Tactic:
simp only [Finset.mem_filter, mem_support_iff, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]

Goal state after:
X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : IsDomain K
w : StdSimplex K X
x : X
hx : ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0
a✝ : X
⊢ a✝ = x → ¬w.weights a✝ = 0
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : IsDomain K
w : StdSimplex K X
x : X
hx : ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0
⊢ w.restrict {x} hx = single x

Tactic:
simp only [← support_weights_eq_singleton, support_weights_restrict, Set.mem_singleton_iff]
  ext
  simp only [Finset.mem_filter, mem_support_iff, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]
  rintro rfl
  simpa using hx

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

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
f : StdSimplex R (StdSimplex R (StdSimplex R I))
⊢ (map (fun σ ↦ σ.join) f).join = f.join.join

Tactic:
exact (join_join f).symm

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

Goal state before:
pp: case inl.inr.inl
𝕜 : 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 : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : a • x + b • y ≤ e
⊢ (Set.Iic e).piecewise f g (a • x + b • y) ≤ a • f x + b • g y

pp: case inl.inr.inr
𝕜 : 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 : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
⊢ (Set.Iic e).piecewise f g (a • x + b • y) ≤ a • f x + b • g y

Tactic:
· rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hc]
      have hc' : a • x + b • e ≤ a • x + b • y := by gcongr
      trans a • f x + b • f e
      · exact (h_anti (hc'.trans hc) hc hc').trans (hf.2 hx Set.self_mem_Iic ha hb hab)
      · rw [h_eq]
        gcongr
        exact h_mono Set.self_mem_Ici hy.le hy.le

Goal state after:
case inl.inr.inr
𝕜 : 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 : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
⊢ (Set.Iic e).piecewise f g (a • x + b • y) ≤ a • f x + b • g y
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
⊢ dist (convexCombPair s t hs ht h x y) x = t * dist x y

Tactic:
refine (H ..).antisymm ?_

Goal state after:
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
⊢ t * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 0 ≤ ↑i

pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)

Tactic:
· simpa using i.prop.left

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)
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
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 0
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
⊢ dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j)) (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y t)) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y t)) (y t) <
    r

Tactic:
dist_convexCombPair_convexCombPair_le

Goal state after:
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
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 0
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
⊢ f j * dist (x j) (x j) + (1 - f j) * dist (y j) (y t) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y t)) (y t) <
    r
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
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j)) (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x t) (y j)) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x t) (y j)) (x t) <
    r

Tactic:
dist_convexCombPair_convexCombPair_le

Goal state after:
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
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (y j) (y j) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x t) (y j)) (x t) <
    r