mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: ⊢ Tendsto log atBot atTop

Tactic:
convert tendsto_log_atTop.comp tendsto_neg_atBot_atTop

Goal state after:
⊢ log = log ∘ Neg.neg
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re
⊢ ¬r.re + 1 = 0

Tactic:
add_eq_zero_iff_eq_neg

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ ¬r.re = -1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hab : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
hr : r = -1
⊢ r + 1 = 0

Tactic:
add_eq_zero_iff_eq_neg

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hab : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
hr : r = -1
⊢ r = -1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ circleAverage (fun x ↦ log ‖1 - x⁻¹ * a‖) 0 1 = 0

Tactic:
circleAverage_zero_one_congr_inv (f := fun x ↦ log ‖1 - x * a‖),

Goal state after:
a : ℂ
h : ‖a‖ < 1
⊢ circleAverage (fun x ↦ log ‖1 - x * a‖) 0 1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case pos
a b c : ℝ
hc : c = 0
⊢ ∫ (x : ℝ) in a..b, c * (c ^ 2 + x ^ 2)⁻¹ = arctan (b / c) - arctan (a / c)

pp: case neg
a b c : ℝ
hc : ¬c = 0
⊢ ∫ (x : ℝ) in a..b, c * (c ^ 2 + x ^ 2)⁻¹ = arctan (b / c) - arctan (a / c)

Tactic:
· simp [hc]

Goal state after:
case neg
a b c : ℝ
hc : ¬c = 0
⊢ ∫ (x : ℝ) in a..b, c * (c ^ 2 + x ^ 2)⁻¹ = arctan (b / c) - arctan (a / c)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t + 1 = 0
⊢ t = -1

Tactic:
add_eq_zero_iff_eq_neg

Goal state after:
a b : ℝ
t : ℂ
ht : t = -1
⊢ t = -1
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_zer : I∞.ZeroAtFilter f
⊢ f =O[I∞] fun z ↦ rexp (-2 * π * z.im / h)

Tactic:
simpa [cuspFunction_zero_of_zero_at_inf hh h_zer, sub_zero] using
    exp_decay_sub_of_bounded_at_inf hh hf h_hol h_zer.boundedAtFilter

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

Goal state before:
pp: h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ cuspFunction h (f - g) = cuspFunction h f - cuspFunction h g

Tactic:
simpa [sub_eq_add_neg, ← cuspFunction_neg hgcts]
    using cuspFunction_add hfcts (by simp [cuspFunction_neg, hgcts])

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑(z - c).re ^ n = f z
hz' : z - c = ↑(z - c).re
n : ℕ
hz₁ : 0 ≤ (z - c).re
⊢ 0 ≤ (↑n.factorial)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n

Tactic:
positivity [zero_re ▸ (Complex.le_def.mp (h n)).1]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: x✝ : ℝ
h : x✝ ∈ Ι (-(π / 2)) (π / 2)
⊢ √(1 - sin x✝ ^ 2) * cos x✝ = cos x✝ ^ 2

Tactic:
uIoc_of_le (neg_le_self (le_of_lt (half_pos Real.pi_pos))),

Goal state after:
x✝ : ℝ
h : x✝ ∈ Set.Ioc (-(π / 2)) (π / 2)
⊢ √(1 - sin x✝ ^ 2) * cos x✝ = cos x✝ ^ 2
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 + ↑g 1 1 = 0
hc : ↑g 1 0 = 0
⊢ g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1)

Tactic:
add_eq_zero_iff_eq_neg

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
⊢ g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ num (-g) z = -num g z

Tactic:
simp [num]; ring

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ (smulAux' g z).im = |↑(GeneralLinearGroup.det g)| * z.im / Complex.normSq (denom g z)

Tactic:
by
  simp only [smulAux', σ]
  split_ifs with h <;>
  [rw [abs_of_pos h]; rw [abs_of_nonpos (not_lt.mp h)]] <;>
  simpa only [Complex.conjCAE_apply, Complex.star_def, Complex.conj_im,
    neg_mul, neg_div, neg_inj] using! moebius_im g z

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

Goal state before:
pp: case mp.inl.inl
g : GL (Fin 2) ℝ
hg : g • { coe := 1 + Complex.I, coe_im_pos := ⋯ } = { coe := 1 + Complex.I, coe_im_pos := ⋯ }
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g).det < 0
ha : (↑g).trace = 0
hb : ↑g 0 1 = ↑g 1 0
hc : ↑g 1 0 = 0
⊢ False

Tactic:
gl_smul_eq_self_iff_re_eq ha hc

Goal state after:
case mp.inl.inl
g : GL (Fin 2) ℝ
hg : { coe := 1 + Complex.I, coe_im_pos := ⋯ }.re = ↑g 0 1 / (2 * ↑g 1 1)
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g).det < 0
ha : (↑g).trace = 0
hb : ↑g 0 1 = ↑g 1 0
hc : ↑g 1 0 = 0
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case e_a
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) =
    (↑(↑g 0 0) * num h u + ↑(↑g 0 1) * denom h u) * denom (g * h) u

Tactic:
simp only [num, denom, Units.val_mul, mul_apply, Fin.sum_univ_succ,
    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one,
    Complex.ofReal_add, Complex.ofReal_mul]

Goal state after:
case e_a
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ ((↑(↑g 0 0) * ↑(↑h 0 0) + ↑(↑g 0 1) * ↑(↑h 1 0)) * u + (↑(↑g 0 0) * ↑(↑h 0 1) + ↑(↑g 0 1) * ↑(↑h 1 1))) *
      (↑(↑g 1 0) * (↑(↑h 0 0) * u + ↑(↑h 0 1)) + ↑(↑g 1 1) * (↑(↑h 1 0) * u + ↑(↑h 1 1))) =
    (↑(↑g 0 0) * (↑(↑h 0 0) * u + ↑(↑h 0 1)) + ↑(↑g 0 1) * (↑(↑h 1 0) * u + ↑(↑h 1 1))) *
      ((↑(↑g 1 0) * ↑(↑h 0 0) + ↑(↑g 1 1) * ↑(↑h 1 0)) * u + (↑(↑g 1 0) * ↑(↑h 0 1) + ↑(↑g 1 1) * ↑(↑h 1 1)))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: ⊢ Tendsto UpperHalfPlane.coe atImInfty (comap Complex.im atTop)

Tactic:
simpa only [atImInfty, tendsto_comap_iff, Function.comp_def,
    funext UpperHalfPlane.coe_im] using tendsto_comap

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

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

Tactic:
← Real.sqrt_mul z.im_pos.le,

Goal state after:
z : ℍ
this : ↑√z.im ≠ 0
⊢ (↑z.re + ↑√(z.im * z.im) * Complex.I) / ↑√z.im = ↑z * (↑√z.im)⁻¹
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (∑ x, if x = k then M i x * -M k j else if x = j then M i x * M k k else M i x * 0) = 0

Tactic:
mul_neg,

Goal state after:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (∑ x, if x = k then -(M i x * M k j) else if x = j then M i x * M k k else M i x * 0) = 0
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M k k • det 1 * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det =
    M k k * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det

Tactic:
det_one,

Goal state after:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M k k • 1 * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det =
    M k k * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁴ : CommRing R
inst✝³ : CommRing S
M : Matrix m m S
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
k : m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ f.polyToMatrix (cornerAddX M k k k) = (-f (M k k)).charmatrix

Tactic:
by
  simp [cornerAddX, Matrix.add_apply, charmatrix,
    RingHom.polyToMatrix, -AlgEquiv.symm_toRingEquiv, map_neg]

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
nontriviality A

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist ↑z ↑(w.center |log (z.im / w.im)|) = w.im * |(z.im / w.im - (z.im / w.im)⁻¹) / 2|

Tactic:
dist_of_re_eq,

Goal state after:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist (↑z).im (↑(w.center |log (z.im / w.im)|)).im = w.im * |(z.im / w.im - (z.im / w.im)⁻¹) / 2|

z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ (↑z).re = (↑(w.center |log (z.im / w.im)|)).re
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
⊢ g a = g b

Tactic:
have e := ultrafilter_extend_extends g
  rw [← congrFun e a, ← congrFun e b, Function.comp_apply, Function.comp_apply]
  rw [preStoneCechUnit, preStoneCechUnit, Quot.eq] at h
  generalize (pure a : Ultrafilter α) = F at h
  generalize (pure b : Ultrafilter α) = G at h
  induction h with
  | rel x y a => exact let ⟨a, hx, hy⟩ := a; preStoneCechCompat hg hx hy
  | refl x => rfl
  | symm x y _ h => rw [h]
  | trans x y z _ _ h h' => exact h.trans h'

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
z : X
⊢ Disjoint (𝓝 ↑z) (𝓝 ∞)

Tactic:
by
    rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact,
      disjoint_map coe_injective, ← principal_singleton, disjoint_principal_right, compl_infty]
    exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩

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

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A

Tactic:
obtain ⟨A, hA⟩ := cdsq_le (K := S • K) (hK.image <| continuous_const_smul S)

Goal state after:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |characteristic f ⊤ r - characteristic (fun x ↦ f x - a₀) ⊤ r| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
← Pi.sub_apply,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |(characteristic f ⊤ - characteristic (fun x ↦ f x - a₀) ⊤) r| ≤ log⁺ ‖a₀‖ + log 2
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
⊢ Integrable (fun x ↦ ∫ (α : ℝ) in Ioc 0 (2 * π), ‖cartanKernel f R α x‖) (volume.restrict (Ioc 0 (2 * π)))

Tactic:
have h_meas_K : Measurable (fun a : ℝ × ℝ ↦ (cartanKernel f R a.1 a.2)⁺) := by fun_prop

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
⊢ Integrable (fun x ↦ ∫ (α : ℝ) in Ioc 0 (2 * π), ‖cartanKernel f R α x‖) (volume.restrict (Ioc 0 (2 * π)))
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
⊢ (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) (D₁ + D₂)) z) * log (r * ‖z‖⁻¹) + ↑((D₁ + D₂) 0) * log r) =
    (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ↑(D₁ 0) * log r) + fun r ↦
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹) + ↑(D₂ 0) * log r

Tactic:
by
    simp only [map_add, coe_add, Pi.add_apply, Int.cast_add]
    ext r
    have {A B C D : ℝ} : A + B + (C + D) = A + C + (B + D) := by ring
    rw [Pi.add_apply, this]
    congr 1
    · have h₁s : ((D₁.toClosedBall r).support ∪ (D₂.toClosedBall r).support).Finite := by
        apply Set.finite_union.2
        constructor
        <;> apply finiteSupport _ (isCompact_closedBall 0 |r|)
      repeat
        rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]
        try simp_rw [← Finset.sum_add_distrib, ← add_mul]
      repeat
        intro x hx
        by_contra
        simp_all
    · ring

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
⊢ ∃ᶠ (x : ℝ) in atTop, ‖1 x‖ < a * ‖logCounting D x‖

Tactic:
simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
⊢ ∀ (a_1 : ℝ), ∃ b, a_1 ≤ b ∧ 1 < a * |logCounting D b|
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
  rcases le_total x y with (xy | yx)
  · rcases le_total y z with (yz | zy)
    · rw [← Set.Icc_union_Icc_eq_Icc xy yz]
      exact hfs.union hft (isGreatest_Icc xy) (isLeast_Icc yz)
    · rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩
      rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ←
        hfs ⟨xu, uz.trans zy⟩ ⟨xv, vz.trans zy⟩, Icc_inter_Icc, sup_of_le_right xu,
        inf_of_le_right (vz.trans zy)]
  · rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩
    rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ←
      hft ⟨yx.trans xu, uz⟩ ⟨yx.trans xv, vz⟩, Icc_inter_Icc, sup_of_le_right (yx.trans xu),
      inf_of_le_right vz]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: 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 b a) (variationOnFromTo f s a c)) =
    ENNReal.ofReal (variationOnFromTo f s b c)

Tactic:
← variationOnFromTo.eq_neg_swap f

Goal state after:
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 (variationOnFromTo f s b c)
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
x : P
⊢ (fun a ↦ (const R R x) a) '' Set.Icc 0 1 = {x}

Tactic:
AffineMap.coe_const,

Goal state after:
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
x : P
⊢ (fun a ↦ Function.const R x a) '' Set.Icc 0 1 = {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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (t₂ * t₁) • (z -ᵥ w) +ᵥ w = t₂ • ((lineMap w z) t₁ -ᵥ w) +ᵥ w

Tactic:
lineMap_vsub_left,

Goal state after:
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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (t₂ * t₁) • (z -ᵥ w) +ᵥ w = t₂ • t₁ • (z -ᵥ w) +ᵥ w
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mpr.«0»
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
s : Simplex R P 1
r : R
h0 : 0 ≤ r
h1 : r ≤ 1
⊢ Finset.affineCombinationLineMapWeights 0 1 r ((fun i ↦ i) ⟨0, ⋯⟩) ∈ Set.Icc 0 1

Tactic:
simp [h0, h1]

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

Goal state before:
pp: case mpr.«1»
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
s : Simplex R P 1
r : R
h0 : 0 ≤ r
h1 : r ≤ 1
⊢ Finset.affineCombinationLineMapWeights 0 1 r ((fun i ↦ i) ⟨1, ⋯⟩) ∈ Set.Icc 0 1

Tactic:
simp [h0, h1]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x : β
y : α
⊢ some y = f.symm x ↔ f y = some x

Tactic:
rw [← eq_some_iff, eq_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : CommRing R
⊢ ↑↑(Perm.sign σ) * det 1 = ↑↑(Perm.sign σ)

Tactic:
det_one,

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : CommRing R
⊢ ↑↑(Perm.sign σ) * 1 = ↑↑(Perm.sign σ)
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : CommRing R
⊢ (Perm.permMatrix R σ).det = ↑↑(Perm.sign σ)

Tactic:
by
  rw [← Matrix.mul_one (σ.permMatrix R), PEquiv.toMatrix_toPEquiv_mul,
    det_permute, det_one, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
v : n → R
inst✝ : CommRing R
⊢ Perm.permMatrix R σ *ᵥ v = v ∘ ⇑σ

Tactic:
by
  ext j
  simp [mulVec_eq_sum, Pi.single, Function.update, Equiv.eq_symm_apply]

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

Goal state before:
pp: case mpr.«0»
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
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
⊢ Finset.affineCombinationLineMapWeights 0 1 r ((fun i ↦ i) ⟨0, ⋯⟩) ∈ Set.Ioo 0 1

Tactic:
simp [h0, h1]

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

Goal state before:
pp: case mpr.«1»
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
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
⊢ Finset.affineCombinationLineMapWeights 0 1 r ((fun i ↦ i) ⟨1, ⋯⟩) ∈ Set.Ioo 0 1

Tactic:
simp [h0, h1]

Goal state after:
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✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
s : Simplex R P 1
p : P
⊢ p ∈ ⇑(lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1 ↔
    p ∈ ⇑(lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1 ∧ s.points 0 ≠ s.points 1

Tactic:
simp [s.independent.injective.ne (by decide : (0 : Fin 2) ≠ 1)]

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

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃ m
M : Matrix m n α
⊢ f.toPEquiv.toMatrix * M = M.submatrix (⇑f) id

Tactic:
ext i j
  rw [toMatrix_mul_apply, Equiv.toPEquiv_apply, submatrix_apply, id]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ t.preimage p ⋯

Tactic:
refine h _ x ?_

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ p x ∈ (convexHull 𝕜) ↑(image p (t.preimage p ⋯))
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ 2 * f x₀ ≤ f y + f (2 • x₀ - y)

Tactic:
have := hf.2 hx' hx (by positivity) (by positivity) (add_halves _)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this✝ : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
this : f ((1 / 2) • y + (1 / 2) • (2 • x₀ - y)) ≤ (1 / 2) • f y + (1 / 2) • f (2 • x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (2 • x₀ - y)
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ici y
hxy : y < x
⊢ ContinuousWithinAt f (Ici y) x

Tactic:
· have h := hf_cvx.continuousOn_interior x
    simp only [nonempty_Iio, interior_Ici', mem_Ioi] at h
    rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hxy)] at h
    exact (h hxy).continuousWithinAt

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
g : N → P
hg : IsAffineMap R g
f : M → N
hf : IsAffineMap R f
s : StdSimplex R M
⊢ (g ∘ f) (sConvexComb s) = sConvexComb (map (g ∘ f) s)

Tactic:
by
    simp [StdSimplex.map_comp, hf.map_sConvexComb, hg.map_sConvexComb]

Goal state after: