mathlib-initiative/mathlib-tactics huggingface dataset:
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
α : Type u_3
f : α → 𝕜 → E
r : ℝ
hr : 1 ≤ r
a : α
s : Finset α
ha : a ∉ s
hs : (∀ a ∈ s, Meromorphic (f a)) → logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
h₁f : ∀ a_1 ∈ insert a s, Meromorphic (f a_1)
⊢ logCounting (f a) ⊤ r ≤ logCounting (f a) ⊤ r

Tactic:
by

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 : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
r : ℝ
hr : R₀ ≤ r
⊢ ∑ z ∈ t, (log r - log ‖z‖) = ↑N * log r - K

Tactic:
by

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
α : Type u_3
s : Finset α
f : α → 𝕜 → E
r : ℝ
h₁f : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r

Tactic:
by

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
α : Type u_3
s : Finset α
f : α → 𝕜 → E
h₁f : ∀ a ∈ s, Meromorphic (f a)
⊢ logCounting (∑ a ∈ s, f a) ⊤ ≤ᶠ[atTop] ∑ a ∈ s, logCounting (f a) ⊤

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ logCounting (f₁ * f₂) 0 r ≤ (logCounting f₁ 0 + logCounting f₂ 0) r

Tactic:
by

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 : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
⊢ ∀ᶠ (r : ℝ) in atTop, logCounting D' r = ↑N * log r - K

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ logCounting (f₁ * f₂) 0 ≤ᶠ[atTop] logCounting f₁ 0 + logCounting f₂ 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ logCounting (f₁ * f₂) ⊤ r ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) r

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ logCounting (f₁ * f₂) ⊤ ≤ᶠ[atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f : 𝕜 → 𝕜
n : ℕ
hf : Meromorphic f
⊢ logCounting (f ^ n) 0 = n • logCounting f 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
⊢ (s ∪ t) ∩ Icc z y = t ∩ Icc z y

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f : 𝕜 → 𝕜
n : ℕ
hf : Meromorphic f
⊢ logCounting (f ^ n) ⊤ = n • logCounting f ⊤

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f : 𝕜 → 𝕜
n : ℕ
hf : Meromorphic f
⊢ logCounting (f ^ n) ⊤ = n • logCounting f ⊤

Tactic:
by
  simp [logCounting, divisor_pow hf.meromorphicOn n]

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

Goal state before:
pp: R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ MeromorphicOn f (closedBall 0 |R|)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : HasConstantSpeedOnWith f s l
hft : HasConstantSpeedOnWith f t l
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
⊢ HasConstantSpeedOnWith f (s ∪ t) l

Tactic:
by

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

Goal state before:
pp: R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ logCounting (divisor f univ) R = circleAverage (fun x ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
by

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

Goal state before:
pp: R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ (logCounting f 0 - logCounting f ⊤) R = circleAverage (fun x ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
by

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 : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
hEq : ∀ᶠ (r : ℝ) in atTop, logCounting D' r = ↑N * log r - K
⊢ ∀ᶠ (r : ℝ) in atTop, (↑N - C) * log r ≤ K

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: 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
⊢ HasConstantSpeedOnWith f (Icc x z) l

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ HasConstantSpeedOnWith f s 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

Tactic:
by

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 : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
⊢ (support D).Finite

Tactic:
by

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φ :
  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 = ↑l * (y - x)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
h : Meromorphic f
⊢ logCounting f ⊤ =O[atTop] 1 ↔ AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ

Tactic:
by

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

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 ⊤ =O[atTop] log ↔ (MeromorphicOn.divisor f univ)⁻.support.Finite

Tactic:
by

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φ :
  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
⊢ ↑l' * (φ y - φ x) = (φ y - φ x) * ↑l'

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
a : α
l : List α
p : α → α → α → Prop
⊢ Triplewise p (a :: l) ↔ Pairwise (p a) l ∧ Triplewise p l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
a : α
p : α → α → α → Prop
⊢ Triplewise p [a]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
a b : α
p : α → α → α → Prop
⊢ Triplewise p [a, b]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
a b c : α
p : α → α → α → Prop
⊢ Triplewise p [a, b, c] ↔ p a b c

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
hl : Triplewise p l
⊢ Triplewise q l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β
p' : β → β → β → Prop
⊢ Triplewise p' (map f l) ↔ Triplewise (fun a b c ↦ p' (f a) (f b) (f c)) l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
p : α → α → α → Prop
f : α → β
p' : β → β → β → Prop
h : ∀ {a b c : α}, p' (f a) (f b) (f c) → p a b c
hl : Triplewise p' (map f l)
⊢ Triplewise p l

Tactic:
by

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
⊢ EqOn φ (fun y ↦ ↑l / ↑l' * (y - x) + φ x) s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasUnitSpeedOn (f ∘ φ) s
hf : HasUnitSpeedOn f (φ '' s)
x : ℝ
xs : x ∈ s
⊢ EqOn φ (fun y ↦ y - x + φ x) s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ : ℝ
⊢ 0 ∈ φ '' Icc 0 s

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
h :
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1),
    p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]
i j : Nat
hi : i < tail.length
hj : j < tail.length
hij : i < j
⊢ 0 < i + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ x : ℝ
xs : x ∈ Icc 0 s
hx : φ x = 0
this : MapsTo φ (Icc 0 s) (Icc 0 t)
⊢ 0 ∈ Icc 0 s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ : ℝ
⊢ φ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (Icc 0 t)
⊢ EqOn φ id (Icc 0 s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: α : 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
⊢ edist (naturalParameterization f s a (variationOnFromTo f s a b)) (f b) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : α → α → α → Prop
⊢ Triplewise p (l₁ ++ l₂) ↔
    Triplewise p l₁ ∧
      Triplewise p l₂ ∧ (∀ (a : α), a ∈ l₁ → Pairwise (p a) l₂) ∧ ∀ (a : α), a ∈ l₂ → Pairwise (fun x y ↦ p x y a) l₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l : List α
p : α → α → α → Prop
⊢ Triplewise p l.reverse ↔ Triplewise (fun a b c ↦ p c b a) l

Tactic:
by

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

Goal state before:
pp: 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
⊢ List.Wbtw R []

Tactic:
by

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

Goal state before:
pp: 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
⊢ List.Sbtw R []

Tactic:
by

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

Goal state before:
pp: 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
p₁ : P
⊢ List.Wbtw R [p₁]

Tactic:
by

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

Goal state before:
pp: 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
p₁ : P
⊢ List.Sbtw R [p₁]

Tactic:
by

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

Goal state before:
pp: 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
p₁ p₂ : P
⊢ List.Wbtw R [p₁, p₂]

Tactic:
by

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

Goal state before:
pp: 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
p₁ p₂ : P
⊢ List.Sbtw R [p₁, p₂] ↔ p₁ ≠ p₂

Tactic:
by

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

Goal state before:
pp: 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
p₁ p₂ p₃ : P
⊢ List.Wbtw R [p₁, p₂, p₃] ↔ Wbtw R p₁ p₂ p₃

Tactic:
by

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

Goal state before:
pp: 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✝ : IsOrderedRing R
p₁ p₂ p₃ : P
⊢ List.Sbtw R [p₁, p₂, p₃] ↔ Sbtw R p₁ p₂ p₃

Tactic:
by

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

Goal state before:
pp: 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
p₁ p₂ p₃ p₄ : P
⊢ List.Wbtw R [p₁, p₂, p₃, p₄] ↔ Wbtw R p₁ p₂ p₃ ∧ Wbtw R p₁ p₂ p₄ ∧ Wbtw R p₁ p₃ p₄ ∧ Wbtw R p₂ p₃ p₄

Tactic:
by

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

Goal state before:
pp: 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✝ : IsOrderedRing R
p₁ p₂ p₃ p₄ : P
⊢ List.Sbtw R [p₁, p₂, p₃, p₄] ↔ Sbtw R p₁ p₂ p₃ ∧ Sbtw R p₁ p₂ p₄ ∧ Sbtw R p₁ p₃ p₄ ∧ Sbtw R p₂ p₃ p₄

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
⊢ HasUnitSpeedOn (naturalParameterization f s a) (variationOnFromTo f s a '' s)

Tactic:
by

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
h : image (fun z ↦ ↑z) s' = univ
⊢ False

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝² : RCLike 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
hφcv : ConvexOn ℝ s φ
⊢ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = ⇑(LinearMap.id.prodMap reLm) ⁻¹' {p | p.1 ∈ s ∧ φ p.1 ≤ p.2}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝² : RCLike 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
hφcv : ConvexOn ℝ s φ
⊢ Convex ℝ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}

Tactic:
by

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

Goal state after:
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
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p | p.1 ∈ s ∧ ↑(φ p.1) ≤ p.2}
⊢ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = Prod.map id (Real.toEReal ∘ ⇑re) ⁻¹' A

Tactic:
by

Goal state after:
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
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
⊢ IsClosed {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}

Tactic:
by

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
⊢ #({x}.biUnion t) = #(t x)

Tactic:
by

Goal state after: