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

Goal state before:
pp: case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e

Tactic:
rw [div_mul_comm, div_self (by norm_cast; linarith)]
        simp only [one_mul, add_sub_cancel, hz₂]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
f : ℂ → E
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Real.circleAverage f c)

Tactic:
by
  apply (intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' _ _ _).const_smul
  fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case neg
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
⊢ x - 1 < x * log x

Tactic:
· cases lt_or_eq_of_le h0 <;> aesop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: x : ℝ
⊢ |sinc x| ≤ 1

Tactic:
by_cases hx : x = 0
  · simp [hx]
  rw [sinc_of_ne_zero hx, abs_div]
  refine div_le_of_le_mul₀ (abs_nonneg _) zero_le_one ?_
  rw [one_mul]
  exact abs_sin_le_abs

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
a b : E
⊢ log⁺ ‖a + b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2

Tactic:
grw [norm_add_le, posLog_add, add_rotate]

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto (fun x ↦ g ↑x) atTop (𝓝 0)

Tactic:
simp_rw [g, ← ofReal_mul, ← ofReal_exp, coe_smul]
    have h₀ : Tendsto (fun x : ℝ => expR (ε * x)) atTop (𝓝 0) :=
      Real.tendsto_exp_atBot.comp (tendsto_const_nhds.neg_mul_atTop ε₀ tendsto_id)
    exact h₀.zero_smul_isBoundedUnder_le hre

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

Goal state before:
pp: 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}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ t ∈ ball 0 r, gray w t = g z₀
⊢ ‖z - z₀‖ < r

Tactic:
simpa [dist_eq_norm] using! mem_ball.mp hz

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case neg.hs
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ 0 < P.natDegree

Tactic:
natDegree_pos_iff_degree_pos

Goal state after:
case neg.hs
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ 0 < P.degree
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
⊢ ∑ x ∈ s, weight x • (z - x) = 0

Tactic:
by_cases hzP : P.eval z = 0

Goal state after:
case pos
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : eval z P = 0
⊢ ∑ x ∈ s, weight x • (z - x) = 0

case neg
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : ¬eval z P = 0
⊢ ∑ x ∈ s, weight x • (z - x) = 0
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
a : ℂ
⊢ cuspFunction h (a • f) = a • cuspFunction h f

Tactic:
simp only [cuspFunction] at *

Goal state after:
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a : ℂ
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) =
    a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))
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:
by
  simpa [sub_eq_add_neg, ← cuspFunction_neg hgcts]
    using cuspFunction_add hfcts (by simp [cuspFunction_neg, hgcts])

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < q.natDegree
⊢ False

Tactic:
natDegree_pos_iff_degree_pos

Goal state after:
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < q.degree
⊢ False
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ Metric.eball 0 ↑r'
H : HasSum (fun n ↦ (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x ↦ z - c) (f (c + (z - c)))
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
simp only [add_sub_cancel] at H

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ Metric.eball 0 ↑r'
H : HasSum (fun n ↦ (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x ↦ z - c) (f z)
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ sin x✝ ^ 2 = 1 - cos x✝ ^ 2

Tactic:
sin_sq

Goal state after:
a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ 1 - cos x✝ ^ 2 = 1 - cos x✝ ^ 2
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
x : ℂ
hx : x ∈ closure (ball 0 (r n))
⊢ ?m.450

Tactic:
by simpa using closure_ball_subset_closedBall hx

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
rcases exists_continuousOn_pow_eq hUc hUo continuousOn_id (by rwa [image_id]) two_ne_zero
    with ⟨f, hfc, hf_inv⟩

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : ∀ (x : ℂ), f x ^ 2 = id x
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
⊢ ↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|)) u) ≤ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u)

pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

Tactic:
· exact map_finsum (Int.castRingHom ℝ)
      ((divisor _ _).finiteSupport <| isCompact_closedBall ..) |>.le

Goal state after:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ 0 ≤ -(↑g).discr

Tactic:
· simpa using hell.le

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

Goal state before:
pp: a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
⊢ ∃ u v, (fun x ↦ ⟨!![a, b; 0, a⁻¹], ⋯⟩ • x) = (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x

Tactic:
refine ⟨⟨_, mul_self_pos.mpr ha⟩, b * a, ?_⟩

Goal state after:
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
⊢ (fun x ↦ ⟨!![a, b; 0, a⁻¹], ⋯⟩ • x) = (fun x ↦ b * a +ᵥ x) ∘ fun x ↦ ⟨a * a, ⋯⟩ • x
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
⊢ !![z.re, -z.im; z.im, z.re].trace = 2 * z.re

Tactic:
Matrix.trace_fin_two

Goal state after:
z : ℂ
⊢ !![z.re, -z.im; z.im, z.re] 0 0 + !![z.re, -z.im; z.im, z.re] 1 1 = 2 * z.re
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case convert_1
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ IsPreconnected {z | 0 < z.im}

Tactic:
exact (Complex.isConnected_of_upperHalfPlane subset_rfl (by grind)).isPreconnected

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

Goal state before:
pp: case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : IsIntegral K x
h₁ : ¬FiniteDimensional (↥K⟮x⟯) L
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
simp [finrank_of_not_finite h₁]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), G y ∈ t'
hGF : ⇑G ∘ e = ⇑F
g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }
hgG : ∀ {y : Y} {a : ℝ}, g y = a ↔ G y = ↑(h a)
⊢ ⇑g ∘ e = ⇑f

Tactic:
ext x
    exact hgG.2 (congr_fun hGF _)

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

Goal state before:
pp: x : ℝ
⊢ sinh (arsinh x) = x

Tactic:
by
  rw [sinh_eq, ← arsinh_neg, exp_arsinh, exp_arsinh, neg_sq]; simp

Goal state after:
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 : ℝ
⊢ inversion c R c = c

Tactic:
by simp [inversion]

Goal state after:
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 x : P
⊢ inversion c 0 x = c

Tactic:
by simp [inversion]

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

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

Tactic:
rw [dist_eq, mul_div_cancel_left₀ (arsinh _) two_ne_zero, sinh_arsinh]

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ DenseRange stoneCechUnit

Tactic:
unfold stoneCechUnit T2Quotient.mk

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
⊢ DenseRange fun x ↦ ⟦preStoneCechUnit x⟧
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case e'_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
x₁ x₂ : X
⊢ π x₁ = π x₂ ↔ ∃ a, a • x₂ = x₁

Tactic:
Quotient.eq',

Goal state after:
case e'_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
x₁ x₂ : X
⊢ R x₁ x₂ ↔ ∃ a, a • x₂ = x₁
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case convert_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ TopologicalSpace G

pp: case convert_7
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ ProperSMul G X

Tactic:
all_goals infer_instance

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✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
⊢ ∃ i, IsCompact i ∧ MapsTo f iᶜ N

Tactic:
obtain ⟨U, hU₁, hU₂, hU₃⟩ := mem_nhds_iff.mp hN

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst✝²] U
hU₃ : y ∈ U
⊢ ∃ i, IsCompact i ∧ MapsTo f iᶜ N
Module: Mathlib.Analysis.ConstantSpeed

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

Tactic:
· rw [variationOnFromTo.eq_of_ge f s yx, h ys xs yx]
      have := ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr yx))
      simp_all only [NNReal.val_eq_coe]; ring

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:
simp [List.Sbtw]

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:
simp [List.Sbtw]

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:
simp [List.Sbtw]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
f : P →ᵃ[R] P'
x y : P
⊢ ⇑f '' affineSegment R x y = affineSegment R (f x) (f y)

Tactic:
rw [affineSegment, affineSegment, Set.image_image, ← comp_lineMap]
  rfl

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

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
x : ↑s
r : ℝ
hr : r < s.domRestrict φ x
⊢ ∃ a ∈ range fun f ↦ ↑f x, r < a

Tactic:
obtain ⟨z, hz⟩ := exists_between hr

Goal state after:
case refine_3
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
x : ↑s
r : ℝ
hr : r < s.domRestrict φ x
z : ℝ
hz : r < z ∧ z < s.domRestrict φ x
⊢ ∃ a ∈ range fun f ↦ ↑f x, r < a
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : PartialOrder R
x : R
⊢ (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1

Tactic:
exact
    ⟨fun h => ⟨h.1.1.lt_of_ne (Ne.symm h.2.1), h.1.2.lt_of_ne h.2.2⟩, fun h =>
      ⟨⟨h.1.le, h.2.le⟩, h.1.ne', h.2.ne⟩⟩

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

Goal state before:
pp: case intro.ind
α : Type v
inst✝¹ : DecidableEq α
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : 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
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
hn : Fintype.card ι = n
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
rcases n with (_ | n)

Goal state after:
case intro.ind.zero
α : Type v
inst✝¹ : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
ih :
  ∀ m < 0,
    ∀ {ι : 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 ι = 0
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

case intro.ind.succ
α : 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
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Module: Mathlib.Analysis.Convex.Between

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

Tactic:
nth_rw 2 [affineSegment_comm]

Goal state after:
case 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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (max i j)) (s.points (min i j))
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
s : Simplex R P 1
⊢ s.interior = ⇑(lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1

Tactic:
by
  ext p
  constructor
  · rintro ⟨w, hw, h01, rfl⟩
    have h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1) := by
      rw [Fin.sum_univ_two] at hw
      ext i
      fin_cases i <;> simp [← hw]
    rw [h, Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _)]
    exact Set.mem_image_of_mem _ (h01 _)
  · rintro ⟨r, ⟨h0, h1⟩, rfl⟩
    rw [← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _), affineCombination_mem_interior_iff
        (Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)]
    intro i
    fin_cases i <;> simp [h0, h1]

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

Goal state before:
pp: k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
⊢ ⊥.toMatrix = 0

Tactic:
toMatrix_bot

Goal state after:
k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : M ∈ rowStochastic R n
hx : ∀ (i : n), 0 ≤ x i
⊢ ∀ (j : n), 0 ≤ (M *ᵥ x) j

Tactic:
intro j
  simp only [Matrix.mulVec, dotProduct]
  apply Finset.sum_nonneg
  intro k _
  refine Left.mul_nonneg ?_ (hx k)
  exact nonneg_of_mem_rowStochastic hM

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

Goal state before:
pp: case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖↑(u n_1) - ↑0‖ < ε / C
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
⊢ ‖(1 + ↑(u n)) • y - y‖ < ε

Tactic:
rw [show (1 + u n : ℝ) • y - y = (u n : ℝ) • y by rw [add_smul, one_smul, add_sub_cancel_left],
      norm_smul, Real.norm_eq_abs]

Goal state after:
case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖↑(u n_1) - ↑0‖ < ε / C
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
⊢ |↑(u n)| * ‖y‖ < ε