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

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z ↦ ‖f z - v‖) z
h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z ↦ f z - v) y
key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v
⊢ ∀ᶠ (w : ℂ) in 𝓝 z, f w = f z

Tactic:
filter_upwards [key] with h

Goal state after:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h✝ : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z ↦ ‖f z - v‖) z
h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z ↦ f z - v) y
key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v
h : ℂ
⊢ f h - v = f z - v → f h = f z
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ C + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2) =
    (C + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Tactic:
rw [integral_sub, mul_sub, add_sub_assoc]

Goal state after:
case hf
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ IntervalIntegrable (fun x ↦ sin x ^ n) MeasureTheory.volume a b

case hg
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ IntervalIntegrable (fun x ↦ sin x ^ (n + 2)) MeasureTheory.volume a b
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
z : E
hz : z ∈ sphere 0 1
t : ℂ
ht : t ∈ ball 0 r
⊢ AnalyticAt ℂ g (ray z t)

Tactic:
exact hgr (by simpa [ray, norm_smul, mem_sphere_zero_iff_norm.mp hz] using! ht)

Goal state after:
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
⊢ ∃ c, ∀ x ∈ U, f x = c

Tactic:
obtain ⟨z₀, _⟩ := h₂U.nonempty

Goal state after:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
z₀ : ℂ
h✝ : z₀ ∈ U
⊢ ∃ c, ∀ x ∈ U, f x = c
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
⊢ ∃ c, ∀ x ∈ U, f x = c

Tactic:
obtain ⟨z₀, _⟩ := h₂U.nonempty

Goal state after:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
z₀ : ℂ
h✝ : z₀ ∈ U
⊢ ∃ c, ∀ x ∈ U, f x = c
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ C + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n - cos x ^ (n + 2) =
    (C + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)

Tactic:
rw [integral_sub, mul_sub, add_sub_assoc]

Goal state after:
case hf
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ IntervalIntegrable (fun x ↦ cos x ^ n) MeasureTheory.volume a b

case hg
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ IntervalIntegrable (fun x ↦ cos x ^ (n + 2)) MeasureTheory.volume a b
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ circleAverage (∑ᶠ (u : ℂ), fun x ↦ ↑(D u) * log ‖x - u‖) c R =
    circleAverage (∑ u ∈ h.toFinset, fun x ↦ ↑(D u) * log ‖x - u‖) c R

Tactic:
by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    contrapose
    aesop

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝⁸ : TopologicalSpace X₁
X : Type u
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormalSpace X
s✝ : Set X
e : X₁ → X
Y✝ : Type v
inst✝⁵ : TopologicalSpace Y✝
inst✝⁴ : TietzeExtension Y✝
ι : Type u_1
Y : ι → Type v
inst✝³ : (i : ι) → TopologicalSpace (Y i)
inst✝² : ∀ (i : ι), TietzeExtension (Y i)
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, (i : ι) → Y i)
⊢ ∃ g, ContinuousMap.restrict s g = f

Tactic:
obtain ⟨g', hg'⟩ := Classical.skolem.mp <| fun i ↦
      ContinuousMap.exists_restrict_eq hs (ContinuousMap.piEquiv _ _ |>.symm f i)
    exact ⟨ContinuousMap.piEquiv _ _ g', by ext x i; congrm($(hg' i) x)⟩

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: ⊢ ContinuousOn (fun t ↦ ↑ofComplex (↑I * ↑t)) (Ioi 0)

Tactic:
by
  simp only [ofComplex_apply_eq_ite, continuousOn_iff_continuous_domRestrict,
    continuous_induced_rng]
  have : Continuous (fun t : ℝ ↦ Complex.I * t) := by fun_prop
  exact (this.comp continuous_subtype_val).congr (by simp +contextual)

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: z : ℍ
this : ↑√z.im ≠ 0
⊢ ↑z / ↑√z.im = ↑z * (↑√z.im)⁻¹

Tactic:
div_eq_mul_inv

Goal state after:
z : ℍ
this : ↑√z.im ≠ 0
⊢ ↑z * (↑√z.im)⁻¹ = ↑z * (↑√z.im)⁻¹
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
⊢ (g • z).im = z.im / Complex.normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)

Tactic:
simpa using z.im_smul_eq_div_normSq g

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ √(cosh (arsinh x) ^ 2) = √(1 + x ^ 2)

Tactic:
cosh_sq',

Goal state after:
x : ℝ
⊢ √(1 + sinh (arsinh x) ^ 2) = √(1 + x ^ 2)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ cosh (dist z w / 2) ^ 2 = (dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))) ^ 2

pp: case ha
z w : ℍ
⊢ 0 ≤ cosh (dist z w / 2)

pp: case hb
z w : ℍ
⊢ 0 ≤ dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))

Tactic:
cosh_sq',

Goal state after:
z w : ℍ
⊢ 1 + sinh (dist z w / 2) ^ 2 = (dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))) ^ 2

case ha
z w : ℍ
⊢ 0 ≤ cosh (dist z w / 2)

case hb
z w : ℍ
⊢ 0 ≤ dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ cosh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2 + sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2 =
    1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)

Tactic:
cosh_sq',

Goal state after:
z w : ℍ
⊢ 1 + sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2 + sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2 =
    1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist z w = r ↔ dist ↑z ↑w ^ 2 / (4 * z.im * w.im) = sinh (r / 2) ^ 2

Tactic:
dist_eq_iff_eq_sinh,

Goal state after:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist ↑z ↑w / (2 * √(z.im * w.im)) = sinh (r / 2) ↔ dist ↑z ↑w ^ 2 / (4 * z.im * w.im) = sinh (r / 2) ^ 2
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
hdist : Tendsto (dist c) (𝓝[≠] c) (𝓝[>] 0)
⊢ Tendsto (fun x ↦ R ^ 2 / dist c x) (𝓝[≠] c) atTop

Tactic:
div_eq_mul_inv

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
hdist : Tendsto (dist c) (𝓝[≠] c) (𝓝[>] 0)
⊢ Tendsto (fun x ↦ R ^ 2 * (dist c x)⁻¹) (𝓝[≠] c) atTop
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ rexp (log z.im) / w.im ≤ rexp (dist z w)

Tactic:
← exp_log w.im_pos,

Goal state after:
z w : ℍ
⊢ rexp (log z.im) / rexp (log w.im) ≤ rexp (dist z w)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ instTopologicalSpace = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

Tactic:
refine le_antisymm (continuous_id_iff_le.1 ?_) ?_

Goal state after:
case refine_1
z w : ℍ
r : ℝ
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] id

case refine_2
z w : ℍ
r : ℝ
⊢ PseudoMetricSpace.toUniformSpace.toTopologicalSpace ≤ instTopologicalSpace
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ (map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsCompact s) fun s ↦ some '' sᶜ ∪ {∞}

Tactic:
exact (hasBasis_coclosedCompact.map _).sup_pure _

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
⊢ NormalSpace (OnePoint X)

Tactic:
suffices R1Space (OnePoint X) by infer_instance

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
⊢ R1Space (OnePoint X)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 z) (cocompact X) ∧ Disjoint (map some (𝓝 z)) (𝓟 {∞})

Tactic:
disjoint_principal_right,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 z) (cocompact X) ∧ {∞}ᶜ ∈ map some (𝓝 z)
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
h : Meromorphic f
a₀ : E
⊢ characteristic f ⊤ - characteristic (fun x ↦ f x - a₀) ⊤ = proximity f ⊤ - proximity (fun x ↦ f x - a₀) ⊤

Tactic:
simp [← Pi.sub_def, characteristic, logCounting_sub_const h]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
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 : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
⊢ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y → w ∈ (s ∪ t) ∩ Icc z y

Tactic:
rintro (⟨ws, zw, wx⟩ | ⟨wt, xw, wy⟩)

Goal state after:
case mpr.inl
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 : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wx : w ≤ x
⊢ w ∈ (s ∪ t) ∩ Icc z y

case mpr.inr
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 : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
wt : w ∈ t
xw : x ≤ w
wy : w ≤ y
⊢ w ∈ (s ∪ t) ∩ Icc z y
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inr.inl.refl
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
ys : z ∈ s
zy : z ≤ z
⊢ eVariationOn f ((s ∪ t) ∩ Icc z z) = ENNReal.ofReal (↑l * (z - z))

Tactic:
simp only [Icc_self, sub_self, mul_zero, ENNReal.ofReal_zero]

Goal state after:
case inr.inl.refl
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
ys : z ∈ s
zy : z ≤ z
⊢ eVariationOn f ((s ∪ t) ∩ {z}) = 0
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:
induction s using Finset.induction with

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
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
⊢ 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:
rcases le_total c b with (cb | bc)

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

case inr
α : 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
bc : b ≤ c
⊢ 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))
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mp.inl
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : tx - tx * ty + ty = 0
⊢ x = (lineMap x z) ty

pp: case mp.inr
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z -ᵥ x = 0
⊢ x = (lineMap x z) ty

Tactic:
· nth_rw 1 [← mul_one tx] at h
      rw [← mul_sub, add_eq_zero_iff_neg_eq] at h
      have h' : ty = 0 := by
        refine le_antisymm ?_ hty.1
        rw [← h, Left.neg_nonpos_iff]
        exact mul_nonneg htx.1 (sub_nonneg.2 hty.2)
      simp [h']

Goal state after:
case mp.inr
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z -ᵥ x = 0
⊢ x = (lineMap x z) ty
Module: Mathlib.Combinatorics.Hall.Finite

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

Tactic:
ht'

Goal state after:
α : Type v
inst✝² : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝¹ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
inst✝ : Fintype ι'
t'✝ : ι' → Finset α
hι' : Fintype.card ι' ≤ n
ht' : ∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t'✝)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t'✝ x
Module: Mathlib.Analysis.Convex.Between

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x y z : P
⊢ Wbtw R x y z ∧ Wbtw R x z y ↔ y = z

Tactic:
by
  rw [wbtw_comm, wbtw_comm (z := y), eq_comm]
  exact wbtw_swap_left_iff R x

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : i ⟶ j
⊢ F.eventualRange j ⊆ range ⇑(ConcreteCategory.hom (F.map f)) ∧
      range ⇑(ConcreteCategory.hom (F.map f)) ⊆ F.eventualRange j ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))

Tactic:
eventualRange,

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : i ⟶ j
⊢ ⋂ i, ⋂ f, range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map f)) ∧
      range ⇑(ConcreteCategory.hom (F.map f)) ⊆ ⋂ i, ⋂ f, range ⇑(ConcreteCategory.hom (F.map f)) ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case e_x.e_a.convert_6
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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ 0 < 1 + 1

Tactic:
· lia

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
h : s = Set.univ
⊢ ofSet s = PEquiv.refl α

Tactic:
simp only [← ofSet_univ, h]

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⟩
⊢ (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, f⟩ ⊆
    (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k', g'⟩

Tactic:
refine (eq_of_le_of_not_lt hl ?_).ge

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⟩
⊢ ¬(fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k', g'⟩ ⊂
      (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, f⟩
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case e_y.e_a.convert_6
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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ 0 < 1 + 1

Tactic:
· lia

Goal state after: