awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo ψ (φ '' t) t
hψ : MonotoneOn ψ (φ '' t)
inr : eVariationOn (f ∘ id) (φ '' t) ≤ eVariationOn (f ∘ φ) t
⊢ eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
change eVariationOn (f ∘ id) (φ '' t) ≤ eVariationOn (f ∘ φ) t

Premises used: Function.comp, id, eVariationOn, Set.image
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo ψ (φ '' t) t
hψ : MonotoneOn ψ (φ '' t)
inr : eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t
⊢ eVariationOn (f ∘ id) (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
rw [← eq_of_eqOn (ψφs.comp_left : EqOn (f ∘ φ ∘ ψ) (f ∘ id) (φ '' t))]

Premises used: eVariationOn.eq_of_eqOn, Set.EqOn.comp_left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo ψ (φ '' t) t
hψ : MonotoneOn ψ (φ '' t)
⊢ eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
comp_le_of_monotoneOn _ ψ hψ ψts

Premises used: eVariationOn.comp_le_of_monotoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo ψ (φ '' t) t
hψ : MonotoneOn ψ (φ '' t)
⊢ eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
exact comp_le_of_monotoneOn _ ψ hψ ψts

Premises used: eVariationOn.comp_le_of_monotoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
inl : ∀ (h : x ≤ y), eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))
inr : ∀ (h : y ≤ x), eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))
⊢ eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))

Tactic:
rcases le_total x y with (h | h)

Premises used: le_total
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
⊢ eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' (t ∩ Icc x y))

Tactic:
comp_eq_of_monotoneOn f φ (hφ.mono Set.inter_subset_left)

Premises used: Set.inter_subset_left, eVariationOn.comp_eq_of_monotoneOn, MonotoneOn.mono
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
h₁ : φ '' t ∩ Icc (φ x) (φ y) = φ '' (t ∩ Icc x y)
⊢ eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))

Tactic:
convert! comp_eq_of_monotoneOn f φ (hφ.mono Set.inter_subset_left)

Premises used: Set.inter_subset_left, eVariationOn.comp_eq_of_monotoneOn, MonotoneOn.mono
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
h₁ : φ '' t ∩ Icc (φ x) (φ y) ≤ φ '' (t ∩ Icc x y)
h₂ : φ '' (t ∩ Icc x y) ≤ φ '' t ∩ Icc (φ x) (φ y)
⊢ φ '' t ∩ Icc (φ x) (φ y) = φ '' (t ∩ Icc x y)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
h₁ : ∀ (xu : x ≤ u), φ u ∈ φ '' (t ∩ Icc x y)
h₂ : ∀ (ux : u ≤ x), φ u ∈ φ '' (t ∩ Icc x y)
⊢ φ u ∈ φ '' (t ∩ Icc x y)

Tactic:
rcases le_total x u with (xu | ux)

Premises used: le_total
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
xu : x ≤ u
h₁ : ∀ (uy : u ≤ y), φ u ∈ φ '' (t ∩ Icc x y)
h₂ : ∀ (yu : y ≤ u), φ u ∈ φ '' (t ∩ Icc x y)
⊢ φ u ∈ φ '' (t ∩ Icc x y)

Tactic:
rcases le_total u y with (uy | yu)

Premises used: le_total
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
xu : x ≤ u
uy : u ≤ y
⊢ φ u ∈ φ '' (t ∩ Icc x y)

Tactic:
⟨u, ⟨us, ⟨xu, uy⟩⟩, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
xu : x ≤ u
uy : u ≤ y
⊢ φ u ∈ φ '' (t ∩ Icc x y)

Tactic:
exact ⟨u, ⟨us, ⟨xu, uy⟩⟩, rfl⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
xu : x ≤ u
yu : y ≤ u
h₁ : φ y ∈ φ '' (t ∩ Icc x y)
⊢ φ u ∈ φ '' (t ∩ Icc x y)

Tactic:
rw [le_antisymm vφy (hφ hy us yu)]

Premises used: le_antisymm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
xu : x ≤ u
yu : y ≤ u
⊢ φ y ∈ φ '' (t ∩ Icc x y)

Tactic:
⟨y, ⟨hy, ⟨h, le_rfl⟩⟩, rfl⟩

Premises used: le_rfl, Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
xu : x ≤ u
yu : y ≤ u
⊢ φ y ∈ φ '' (t ∩ Icc x y)

Tactic:
exact ⟨y, ⟨hy, ⟨h, le_rfl⟩⟩, rfl⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
ux : u ≤ x
h₁ : φ x ∈ φ '' (t ∩ Icc x y)
⊢ φ u ∈ φ '' (t ∩ Icc x y)

Tactic:
rw [← le_antisymm vφx (hφ us hx ux)]

Premises used: le_antisymm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
ux : u ≤ x
⊢ φ x ∈ φ '' (t ∩ Icc x y)

Tactic:
⟨x, ⟨hx, ⟨le_rfl, h⟩⟩, rfl⟩

Premises used: le_rfl, Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
ux : u ≤ x
⊢ φ x ∈ φ '' (t ∩ Icc x y)

Tactic:
exact ⟨x, ⟨hx, ⟨le_rfl, h⟩⟩, rfl⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
hu : u ∈ t
xu : x ≤ u
uy : u ≤ y
⊢ φ u ∈ φ '' t ∩ Icc (φ x) (φ y)

Tactic:
⟨⟨u, hu, rfl⟩, ⟨hφ hx hu xu, hφ hu hy uy⟩⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
hu : u ∈ t
xu : x ≤ u
uy : u ≤ y
⊢ φ u ∈ φ '' t ∩ Icc (φ x) (φ y)

Tactic:
exact ⟨⟨u, hu, rfl⟩, ⟨hφ hx hu xu, hφ hu hy uy⟩⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
inr : (φ '' t ∩ Icc (φ x) (φ y)).Subsingleton
inr₁ : (t ∩ Icc x y).Subsingleton
⊢ eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))

Tactic:
rw [eVariationOn.subsingleton, eVariationOn.subsingleton]

Premises used: eVariationOn.subsingleton
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
⊢ (φ '' t ∩ Icc (φ x) (φ y)).Subsingleton

Tactic:
(Set.subsingleton_Icc_of_ge (hφ hy hx h)).anti Set.inter_subset_right

Premises used: Set.Subsingleton.anti, Set.subsingleton_Icc_of_ge, Set.inter_subset_right
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
⊢ (t ∩ Icc x y).Subsingleton

Tactic:
(Set.subsingleton_Icc_of_ge h).anti Set.inter_subset_right

Premises used: Set.Subsingleton.anti, Set.subsingleton_Icc_of_ge, Set.inter_subset_right
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
⊢ (φ '' t ∩ Icc (φ x) (φ y)).Subsingleton

Tactic:
exacts [(Set.subsingleton_Icc_of_ge (hφ hy hx h)).anti Set.inter_subset_right,
      (Set.subsingleton_Icc_of_ge h).anti Set.inter_subset_right]

Premises used: Set.Subsingleton.anti, Set.subsingleton_Icc_of_ge, Set.inter_subset_right
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : AntitoneOn φ t
apply : eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
⊢ eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)

Tactic:
apply le_antisymm (comp_le_of_antitoneOn f φ hφ (mapsTo_image φ t))

Premises used: Set.mapsTo_image, le_antisymm, eVariationOn.comp_le_of_antitoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : AntitoneOn φ t
inl : IsEmpty β → eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
inr : Nonempty β → eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
⊢ eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
cases isEmpty_or_nonempty β

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : AntitoneOn φ t
h : IsEmpty β
⊢ eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
simp [Set.eq_empty_of_isEmpty]

Premises used: Set.eq_empty_of_isEmpty
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : AntitoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
⊢ EqOn (φ ∘ ψ) id (φ '' t)

Tactic:
have ψφs : EqOn (φ ∘ ψ) id (φ '' t) := (surjOn_image φ t).rightInvOn_invFunOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : AntitoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
⊢ MapsTo (Function.invFunOn φ t) (φ '' t) t

Tactic:
have ψts := (surjOn_image φ t).mapsTo_invFunOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : AntitoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo (Function.invFunOn φ t) (φ '' t) t
⊢ AntitoneOn ψ (φ '' t)

Tactic:
have hψ : AntitoneOn ψ (φ '' t) := Function.antitoneOn_of_rightInvOn_of_mapsTo hφ ψφs ψts
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : AntitoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo (Function.invFunOn φ t) (φ '' t) t
hψ : AntitoneOn ψ (φ '' t)
inr : eVariationOn (f ∘ id) (φ '' t) ≤ eVariationOn (f ∘ φ) t
⊢ eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
change eVariationOn (f ∘ id) (φ '' t) ≤ eVariationOn (f ∘ φ) t

Premises used: Function.comp, id, eVariationOn, Set.image
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : AntitoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo (Function.invFunOn φ t) (φ '' t) t
hψ : AntitoneOn ψ (φ '' t)
inr : eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t
⊢ eVariationOn (f ∘ id) (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
rw [← eq_of_eqOn (ψφs.comp_left : EqOn (f ∘ φ ∘ ψ) (f ∘ id) (φ '' t))]

Premises used: eVariationOn.eq_of_eqOn, Set.EqOn.comp_left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : AntitoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo (Function.invFunOn φ t) (φ '' t) t
hψ : AntitoneOn ψ (φ '' t)
⊢ eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
comp_le_of_antitoneOn _ ψ hψ ψts

Premises used: eVariationOn.comp_le_of_antitoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : AntitoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo (Function.invFunOn φ t) (φ '' t) t
hψ : AntitoneOn ψ (φ '' t)
⊢ eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
exact comp_le_of_antitoneOn _ ψ hψ ψts

Premises used: eVariationOn.comp_le_of_antitoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) =
    eVariationOn f (image (α := αᵒᵈ) (⇑ofDual : (a : αᵒᵈ) → α) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s))

Tactic:
comp_eq_of_antitoneOn f ofDual fun _ _ _ _ => id

Premises used: OrderDual.ofDual, eVariationOn.comp_eq_of_antitoneOn, id, DFunLike.coe
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
h : s = image (α := αᵒᵈ) (⇑ofDual : (a : αᵒᵈ) → α) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
⊢ eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) = eVariationOn f s

Tactic:
convert! comp_eq_of_antitoneOn f ofDual fun _ _ _ _ => id

Premises used: OrderDual.ofDual, eVariationOn.comp_eq_of_antitoneOn, id, DFunLike.coe
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ s = image (α := αᵒᵈ) (⇑ofDual : (a : αᵒᵈ) → α) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)

Tactic:
simp only [Equiv.image_preimage]

Premises used: Equiv.image_preimage
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
⊢ BoundedVariationOn (α := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s)

Tactic:
simpa [BoundedVariationOn] using hf

Premises used: BoundedVariationOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ BoundedVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔
    BoundedVariationOn f s

Tactic:
⟨fun h ↦ h.ofDual, fun h ↦ h.ofDual⟩

Premises used: BoundedVariationOn.ofDual, Iff.intro
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
⊢ s ∩ Iio a ⊆ s ∩ Iic a

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
apply : eVariationOn f (s ∩ Iic a) ≤ eVariationOn f (s ∩ Iio a)
⊢ eVariationOn f (s ∩ Iio a) = eVariationOn f (s ∩ Iic a)

Tactic:
apply le_antisymm (eVariationOn.mono _ (by grind))

Premises used: le_antisymm, eVariationOn.mono
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
rw :
  ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a }),
      ∑
        i ∈
          Finset.range
            (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })),
        edist
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })) :
                ℕ → α)
              (i + 1)))
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })) :
                ℕ → α)
              i)) ≤
    eVariationOn f (s ∩ Iio a)
⊢ eVariationOn f (s ∩ Iic a) ≤ eVariationOn f (s ∩ Iio a)

Tactic:
rw [eVariationOn_eq_strictMonoOn]

Premises used: eVariationOn.eVariationOn_eq_strictMonoOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
h₁ :
  ∀ (i : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a }),
    ∑
        i_1 ∈
          Finset.range
            (i.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })),
        edist
          (f
            ((↑(i.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })) :
                ℕ → α)
              (i_1 + 1)))
          (f
            ((↑(i.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })) :
                ℕ → α)
              i_1)) ≤
      eVariationOn f (s ∩ Iio a)
⊢ ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a }),
      ∑
        i ∈
          Finset.range
            (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })),
        edist
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })) :
                ℕ → α)
              (i + 1)))
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })) :
                ℕ → α)
              i)) ≤
    eVariationOn f (s ∩ Iio a)

Tactic:
apply iSup_le

Premises used: iSup_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iic a
⊢ n ∈ Iic n

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iic a
⊢ u n ≤ a

Tactic:
have : u n ≤ a := (u_mem n (by simp)).2