mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
this : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (sphere 0 |1|)
⊢ (fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖) =ᶠ[codiscreteWithin (sphere 0 |1|)] fun z ↦
    log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖

Tactic:
filter_upwards [this] with z hz

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
this : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (sphere 0 |1|)
z : ℂ
hz : ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0
⊢ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖ = log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
⊢ ∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R

Tactic:
have h8 : (sphere z₀ r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le

Goal state after:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
⊢ ∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1) + 1) = 2 * ∏ i ∈ Finset.range (k + 1), (2 * ↑i + 2) / (2 * ↑i + 3)

Tactic:
prod_range_succ_comm,

Goal state after:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1) + 1) =
    2 * ((2 * ↑k + 2) / (2 * ↑k + 3) * ∏ x ∈ Finset.range k, (2 * ↑x + 2) / (2 * ↑x + 3))
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1)) = π * ∏ i ∈ Finset.range (k + 1), (2 * ↑i + 1) / (2 * ↑i + 2)

Tactic:
prod_range_succ_comm,

Goal state after:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1)) =
    π * ((2 * ↑k + 1) / (2 * ↑k + 2) * ∏ x ∈ Finset.range k, (2 * ↑x + 1) / (2 * ↑x + 2))
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ |log (2 * R)| + 0 + 0 ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|

Tactic:
by
        gcongr <;> positivity

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:
simp only [cuspFunction]
  ext y
  obtain hy | rfl := ne_or_eq y 0
  · simp [hy]
  · simpa using! (tendsto_nhds_limUnder ⟨_, tendsto_nhds_zero hfcts⟩).add
      (tendsto_nhds_limUnder ⟨_, tendsto_nhds_zero hgcts⟩) |>.limUnder_eq

Goal state after:
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'
⊢ z - c ∈ Metric.eball 0 ↑r'

Tactic:
rw [Metric.eball_coe]

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'
⊢ z - c ∈ Metric.ball 0 ↑r'
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:
simpa using closure_ball_subset_closedBall hx

Goal state after:
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ k → ↑(Ioo (-1) 1)

Tactic:
refine codRestrict (fun x ↦ x / (1 + |x|)) _ fun x ↦ abs_lt.1 ?_

Goal state after:
case refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
x : k
⊢ |x / (1 + |x|)| < 1
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := ⋯
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ {x | (fun x ↦ (fun x ↦ log ‖f x‖) x = 0 x) x} ∈ codiscreteWithin CB

Tactic:
filter_upwards [this] with z hz

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
z : ℂ
hz : f z = 0 z
⊢ log ‖f z‖ = 0 z
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 : m
hi✝ : (i = k) = True
hi : i = k
j : m
hj✝ : (j = k) = True
hj : j = k
⊢ (M * auxMat M k).toSquareBlock (fun x ↦ x = k) True ⟨i, hi✝⟩ ⟨j, hj✝⟩ = (M k k • 1) ⟨i, hi✝⟩ ⟨j, hj✝⟩

Tactic:
simp [toSquareBlock_def, hi, hj, mul_auxMat_corner]

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

Goal state before:
pp: case symm
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G x y : Ultrafilter α
a✝ : Relation.EqvGen (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) x y
h : Ultrafilter.extend g x = Ultrafilter.extend g y
⊢ Ultrafilter.extend g y = Ultrafilter.extend g x

Tactic:
| symm x y _ h =>

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ IsOpen
    ((fun x ↦
        match x with
        | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
      s)

Tactic:
isOpen_sigma_iff

Goal state after:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ ∀ (i : (S : CompHaus) × C(↑S.toTop, X)),
    IsOpen
      (Sigma.mk i ⁻¹'
        (fun x ↦
            match x with
            | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
          s)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: case refine_1
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
s : Set (X ⊕ Y)
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X ⊕ Y)), IsClosed (⇑f ⁻¹' s)
S : CompHaus
x✝ : C(↑S.toTop, X)
f : ↑S.toTop → X
hf : Continuous[_, tX] f
g : ULift.{v, u} ↑S.toTop → X ⊕ Y := Sum.inl ∘ f ∘ ULift.down
hg : Continuous[_, instTopologicalSpaceSum] g
⊢ IsClosed (⇑{ toFun := f, continuous_toFun := hf } ⁻¹' Sum.inl ⁻¹' s)

Tactic:
exact (h (CompHaus.of (ULift.{v} S)) ⟨g, hg⟩).preimage continuous_uliftUp

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ ∀ a ∈ Finset.univ, Meromorphic (![f₁, f₂] a)

Tactic:
simpa using ⟨h₁f₁, h₁f₂⟩

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case hf
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
⊢ CircleIntegrable |(fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖| 0 r

Tactic:
apply (h₁f.sub h₂f).abs

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Measurable f
⊢ Measurable fun p ↦ cartanKernel f R p.1 p.2

Tactic:
unfold cartanKernel; fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
⊢ circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
by
  by_cases hf : MeromorphicAt f 0
  · rw [← circleAverage_congr_codiscreteWithin
      (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero hf h) zero_ne_one.symm]
    simp_rw [norm_sub_rev]
    rw [circleAverage_log_norm_sub_const_eq_posLog]
  have {a : ℂ} : ¬ MeromorphicAt (fun x ↦ f x - a) 0 := by
    rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]
  simp_all [circleAverage_const]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ Integrable (fun p ↦ cartanKernel f R p.1 p.2) ((volume.prod volume).restrict (uIoc 0 (2 * π) ×ˢ uIoc 0 (2 * π)))

Tactic:
← Measure.prod_restrict

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (uIoc 0 (2 * π))).prod (volume.restrict (uIoc 0 (2 * π))))
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int : Integrable (fun p ↦ cartanKernel f R p.1 p.2) ((volume.prod volume).restrict (Ioc 0 (2 * π) ×ˢ Ioc 0 (2 * π)))
⊢ IntegrableOn (fun x ↦ ∫ (α : ℝ) in 0..2 * π, cartanKernel f R α x) (Ioc 0 (2 * π)) volume

Tactic:
← Measure.prod_restrict

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int :
  Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (Ioc 0 (2 * π))).prod (volume.restrict (Ioc 0 (2 * π))))
⊢ IntegrableOn (fun x ↦ ∫ (α : ℝ) in 0..2 * π, cartanKernel f R α x) (Ioc 0 (2 * π)) volume
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int : Integrable (fun p ↦ cartanKernel f R p.1 p.2) ((volume.prod volume).restrict (Ioc 0 (2 * π) ×ˢ Ioc 0 (2 * π)))
⊢ IntegrableOn (fun x ↦ ∫ (β : ℝ) in 0..2 * π, cartanKernel f R x β) (Ioc 0 (2 * π)) volume

Tactic:
← Measure.prod_restrict

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int :
  Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (Ioc 0 (2 * π))).prod (volume.restrict (Ioc 0 (2 * π))))
⊢ IntegrableOn (fun x ↦ ∫ (β : ℝ) in 0..2 * π, cartanKernel f R x β) (Ioc 0 (2 * π)) volume
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.inl
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
xy : x ≤ y
yz : y ≤ z
⊢ HasConstantSpeedOnWith f (Icc x y ∪ Icc y z) l

Tactic:
exact hfs.union hft (isGreatest_Icc xy) (isLeast_Icc yz)

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 : ℝ
hr₁ : logCounting D' r = ↑N * log r - K
hr₂ : 1 ≤ r
hr₃ : ‖logCounting D r‖ ≤ C * ‖log r‖
⊢ (↑N - C) * log r ≤ K

Tactic:
grind [logCounting_le hle hr₂, norm_eq_abs, abs_of_nonneg, log_nonneg, logCounting_nonneg]

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

Goal state before:
pp: case cons
α : 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]
⊢ Triplewise p (head :: tail) ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < (head :: tail).length),
      p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]

Tactic:
simp only [triplewise_cons, length_cons, pairwise_iff_getElem, ih]

Goal state after:
case cons
α : 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]
⊢ ((∀ (i j : Nat) (_hi : i < tail.length) (_hj : j < tail.length), i < j → p head tail[i] tail[j]) ∧
      ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]) ↔
    ∀ (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]
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
x y z p : P
⊢ z -ᵥ p ∈ affineSegment R (x -ᵥ p) (y -ᵥ p) ↔ z ∈ affineSegment R x y

Tactic:
rw [← affineSegment_vsub_const_image, (vsub_left_injective p).mem_set_image]

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

Goal state before:
pp: case inr.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
x z : P
t : R
ht : t ∈ Set.Icc 0 1
hyx : (lineMap x z) t ≠ x
hyz : (lineMap x z) t ≠ z
ho : t ∈ Set.Ioo 0 1
⊢ (lineMap x z) t ∈ ⇑(lineMap x z) '' Set.Ioo 0 1

Tactic:
exact ⟨t, ho, rfl⟩

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
⊢ F.eventualRange i ⊆ ⇑(ConcreteCategory.hom (F.map f)) '' F.eventualRange j

Tactic:
obtain ⟨k, g, hg⟩ := F.isMittagLeffler_iff_eventualRange.1 h j

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map g))
⊢ F.eventualRange i ⊆ ⇑(ConcreteCategory.hom (F.map f)) '' F.eventualRange j
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : {i} ⊆ {i, i'}
subi' : {i'} ⊆ {i, i'}
⊢ ↑((ConcreteCategory.hom ((hallMatchingsFunctor t).map (homOfLE subi).op)) (u (Opposite.op {i, i'}))) ⟨i, ⋯⟩ =
      ↑(u (Opposite.op {i'})) ⟨i', ⋯⟩ →
    i = i'

Tactic:
← hu (CategoryTheory.homOfLE subi').op

Goal state after:
case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : {i} ⊆ {i, i'}
subi' : {i'} ⊆ {i, i'}
⊢ ↑((ConcreteCategory.hom ((hallMatchingsFunctor t).map (homOfLE subi).op)) (u (Opposite.op {i, i'}))) ⟨i, ⋯⟩ =
      ↑((ConcreteCategory.hom ((hallMatchingsFunctor t).map (homOfLE subi').op)) (u (Opposite.op {i, i'}))) ⟨i', ⋯⟩ →
    i = i'
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝³ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
i : J
x : F.obj i
⊢ ∃ a, (fun s ↦ ↑s i) a = x

Tactic:
by
  let s : Set (F.obj i) := {x}
  have := F.toPreimages_nonempty_of_surjective s Fsur (singleton_nonempty x)
  obtain ⟨sec, h⟩ := nonempty_sections_of_finite_cofiltered_system (F.toPreimages s)
  refine ⟨⟨fun j => (sec j).val, fun jk => by simpa [Subtype.ext_iff] using! h jk⟩, ?_⟩
  · have := (sec i).prop
    simp only [mem_iInter, mem_preimage] at this
    have := this (𝟙 i)
    rwa [map_id, id_apply] at this

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : n → α
⊢ σ.toPEquiv.toMatrix *ᵥ a = a ∘ ⇑σ

Tactic:
by
  ext j
  simp [toMatrix, mulVec, dotProduct]

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

Goal state before:
pp: case refine_2.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
⊢ Wbtw R x x z

pp: case refine_2.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : r ∈ Set.Ici 1
⊢ Wbtw R x y ((lineMap x y) r)

Tactic:
· exact wbtw_self_left _ _ _

Goal state after:
case refine_2.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : r ∈ Set.Ici 1
⊢ Wbtw R x y ((lineMap x y) r)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ Sbtw R x y z ↔ x ≠ y ∧ z ∈ ⇑(lineMap x y) '' Set.Ioi 1

Tactic:
refine ⟨fun h => ⟨h.left_ne, ?_⟩, fun h => ?_⟩

Goal state after:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Sbtw R x y z
⊢ z ∈ ⇑(lineMap x y) '' Set.Ioi 1

case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : x ≠ y ∧ z ∈ ⇑(lineMap x y) '' Set.Ioi 1
⊢ Sbtw R x y z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
hr : r₂ ≤ r₁
h' : y = r₁⁻¹ • r₂ • (z -ᵥ x) +ᵥ x
⊢ (lineMap x z) (r₂ / r₁) = y

Tactic:
simp only [lineMap_apply, h', vadd_vsub_assoc, smul_smul, eq_vadd_iff_vsub_eq, vsub_self,
    add_zero]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
hr : r₂ ≤ r₁
h' : y = r₁⁻¹ • r₂ • (z -ᵥ x) +ᵥ x
⊢ (r₂ / r₁) • (z -ᵥ x) = (r₁⁻¹ * r₂) • (z -ᵥ x)
Module: Mathlib.Analysis.Convex.Extrema

Goal state before:
pp: β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ (ya + yc) • f a = f a

Tactic:
yac,

Goal state after:
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ 1 • f a = f a
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
⊢ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x} ∩ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x} ⊆
    {x | x ∈ A ∧ ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x}

Tactic:
rintro x ⟨⟨hxA, hxB⟩, ⟨-, hxC⟩⟩
    exact ⟨hxA, fun z hz => add_le_add (hxB z hz) (hxC z hz)⟩

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

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx; · simp
  rw [gaugeRescale_def s t x, gaugeRescale_smul, gaugeRescale, gaugeRescale, smul_smul,
    div_mul_div_cancel₀]
  exacts [((gauge_pos hta htb).2 hx).ne', div_nonneg (gauge_nonneg _) (gauge_nonneg _)]

Goal state after: