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

Goal state before:
pp: case hf
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
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
⊢ CircleIntegrable (fun x ↦ Real.log ‖f x‖) c R

pp: case h₂f
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
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
⊢ ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M

Tactic:
· exact (h₁f.mono sphere_subset_closedBall).meromorphicOn.circleIntegrable_log_norm

Goal state after:
case h₂f
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
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
⊢ ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: 𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ ↑(closedBall y r) ≃ₜ ↑(closedBall 0 1)

Tactic:
symm

Goal state after:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ ↑(closedBall 0 1) ≃ₜ ↑(closedBall y r)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.refine_2.inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ f x
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖

Tactic:
rcases le_total (f x) (‖f‖ / 3) with hle₂ | hle₂

Goal state after:
case inr.refine_2.inr.inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ f x
hle₂ : f x ≤ ‖f‖ / 3
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖

case inr.refine_2.inr.inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ f x
hle₂ : ‖f‖ / 3 ≤ f x
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det) / |↑g 1 0|

Tactic:
by
  rw [gl_smul_eq_self_iff_dist_sq_eq h htrace hc, eq_comm, ← Real.sqrt_eq_iff_eq_sq, eq_comm,
    Real.sqrt_div', Real.sqrt_sq_eq_abs] <;> positivity [neg_pos.mpr h]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : (-g).IsElliptic
⊢ fixedPt (-g) hg = fixedPt g ⋯

Tactic:
by
  ext
  simp [fixedPt, Matrix.discr_fin_two, Matrix.det_neg]
  ring

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2)) → C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0

Tactic:
rintro ⟨a, ha⟩
    simp [← ha]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case refine_1
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : 1 ≤ n
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
⊢ ((Matrix.scalar (Fin 2)) a + m) ^ n = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m

Tactic:
induction n, hn using Nat.le_induction with
    | base => simp
    | succ n hn IH =>
      simp only [pow_succ, IH, add_mul, Nat.add_sub_cancel, mul_add, ← map_mul, add_assoc]
      simp only [scalar_apply, ← smul_eq_mul_diagonal, ← mul_smul,
        ← smul_eq_diagonal_mul, smul_mul, ← sq, hmsq, smul_zero, add_zero, ← add_smul,
        Nat.cast_add_one, add_mul, one_mul]
      rw [(by lia : n = n - 1 + 1), pow_succ, (by lia : n - 1 + 1 = n)]
      ring_nf

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

Goal state before:
pp: g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ HasDerivAt (fun z ↦ denom g z ^ k) (↑k * ↑(↑g 1 0) * denom g ↑τ ^ (k - 1)) ↑τ

Tactic:
have hd : HasDerivAt (denom g ·) (g 1 0) τ := by
    simpa [denom] using hasDerivAt_id _ |>.const_mul _ |>.add_const (g 1 1 : ℂ)

Goal state after:
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
hd : HasDerivAt (fun x ↦ denom g x) ↑(↑g 1 0) ↑τ
⊢ HasDerivAt (fun z ↦ denom g z ^ k) (↑k * ↑(↑g 1 0) * denom g ↑τ ^ (k - 1)) ↑τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ 1 + dist ↑z ↑w ^ 2 / (2 * √(z.im * w.im)) ^ 2 = dist (↑z) ((starRingEnd ℂ) ↑w) ^ 2 / (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:
one_add_div,

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

z w : ℍ
⊢ (2 * √(z.im * w.im)) ^ 2 ≠ 0

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.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ c
⊢ dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d

pp: case inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Tactic:
· rw [dist_self, zero_mul]
    positivity

Goal state after:
case inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a : { x // 0 < x }
⊢ Isometry fun x ↦ a • x

Tactic:
by
  refine Isometry.of_dist_eq fun y₁ y₂ => ?_
  simp only [dist_eq, coe_pos_real_smul, pos_real_im]; congr 2
  rw [dist_smul₀, mul_mul_mul_comm, Real.sqrt_mul (mul_self_nonneg _), Real.sqrt_mul_self_eq_abs,
    Real.norm_eq_abs, mul_left_comm]
  exact mul_div_mul_left _ _ (mt _root_.abs_eq_zero.1 a.2.ne')

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

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
⊢ Continuous[_, inst✝²] (Ultrafilter.extend f)

Tactic:
have h (b : Ultrafilter α) : ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c) :=
    -- b.map f is an ultrafilter on γ, which is compact, so it converges to some c in γ.
    let ⟨c, _, h'⟩ :=
      isCompact_univ.ultrafilter_le_nhds (b.map f) (by rw [le_principal_iff]; exact univ_mem)
    ⟨c, le_trans (map_mono (ultrafilter_comap_pure_nhds _)) h'⟩

Goal state after:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
⊢ Continuous[_, inst✝²] (Ultrafilter.extend f)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: 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
t : Set X
⊢ IsProperMap fun gx ↦ (gx.1 • ↑gx.2, gx.2)

Tactic:
by
  let Φ : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
  have Φ_proper : IsProperMap Φ := ProperSMul.isProperMap_smul_pair
  let α : G × t ≃ₜ (Φ ⁻¹' snd ⁻¹' t) :=
    have : univ ×ˢ t = Φ ⁻¹' snd ⁻¹' t := by ext; simp [Φ]
    Homeomorph.Set.univ G |>.symm.prodCongr (.refl t) |>.trans
      ((Homeomorph.Set.prod _ t).symm) |>.trans (Homeomorph.setCongr this)
  let β : X × t ≃ₜ (snd ⁻¹' t) :=
    Homeomorph.Set.univ X |>.symm.prodCongr (.refl t) |>.trans
      ((Homeomorph.Set.prod _ t).symm) |>.trans (Homeomorph.setCongr univ_prod)
  exact β.symm.isProperMap.comp (Φ_proper.restrictPreimage (snd ⁻¹' t)) |>.comp α.isProperMap

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
⊢ ‖∫ (x : ℝ), (cartanKernel f R x β)⁺ ∂μ‖ ≤ ‖2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)‖

Tactic:
have h_bound_nonneg : 0 ≤ (2 * π) * (log⁺ ‖f (circleMap 0 R β)‖ + log 2) := by
      positivity [posLog_nonneg (x := ‖f (circleMap 0 R β)‖)]

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)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ‖∫ (x : ℝ), (cartanKernel f R x β)⁺ ∂μ‖ ≤ ‖2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)‖
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.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
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
q : ENNReal.ofReal (↑l * (x - z) + ↑l * (y - x)) = ENNReal.ofReal (↑l * (x - z)) + ENNReal.ofReal (↑l * (y - x))
⊢ ENNReal.ofReal (↑l * (x - z)) + ENNReal.ofReal (↑l * (y - x)) = ENNReal.ofReal (↑l * (y - z))

Tactic:
simp only [NNReal.val_eq_coe] at q

Goal state after:
case inl.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
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
q : ENNReal.ofReal (↑l * (x - z) + ↑l * (y - x)) = ENNReal.ofReal (↑l * (x - z)) + ENNReal.ofReal (↑l * (y - x))
⊢ ENNReal.ofReal (↑l * (x - z)) + ENNReal.ofReal (↑l * (y - x)) = ENNReal.ofReal (↑l * (y - z))
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) → eVariationOn f s = 0

pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ eVariationOn f s = 0 → ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0

Tactic:
· by_contra! ⟨h, hfs⟩
    simp_rw [ne_eq, eVariationOn.eq_zero_iff] at hfs h
    push Not at hfs
    obtain ⟨x, xs, y, ys, hxy⟩ := hfs
    rcases le_total x y with (xy | yx)
    · exact hxy (h xs ys x ⟨xs, le_rfl, xy⟩ y ⟨ys, xy, le_rfl⟩)
    · rw [edist_comm] at hxy
      exact hxy (h ys xs y ⟨ys, le_rfl, yx⟩ x ⟨xs, yx, le_rfl⟩)

Goal state after:
case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ eVariationOn f s = 0 → ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ :
  LocallyBoundedVariationOn (f ∘ φ) s ∧
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo (f ∘ φ) s x y = ↑l * (y - x)
hf :
  LocallyBoundedVariationOn f (φ '' s) ∧
    ∀ ⦃x : ℝ⦄, x ∈ φ '' s → ∀ ⦃y : ℝ⦄, y ∈ φ '' s → variationOnFromTo f (φ '' s) x y = ↑l' * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ (φ y - φ x) * ↑l' = (y - x) * ↑l

Tactic:
symm

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ :
  LocallyBoundedVariationOn (f ∘ φ) s ∧
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo (f ∘ φ) s x y = ↑l * (y - x)
hf :
  LocallyBoundedVariationOn f (φ '' s) ∧
    ∀ ⦃x : ℝ⦄, x ∈ φ '' s → ∀ ⦃y : ℝ⦄, y ∈ φ '' s → variationOnFromTo f (φ '' s) x y = ↑l' * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ (y - x) * ↑l = (φ y - φ x) * ↑l'
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_1.refine_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✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ Pairwise (Sbtw R head) tail

pp: case cons.refine_1.refine_2
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
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ Triplewise (Sbtw R) tail

pp: case cons.refine_1.refine_3
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
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ ∀ (a : P), head :: tail ≠ [a, a]

Tactic:
· clear ih
        induction tail with
        | nil => simp
        | cons head2 tail ih' =>
          rw [pairwise_cons] at hp hpne hpne ⊢
          refine ⟨fun a ha ↦ ⟨hp.1 a ha, ?_⟩, ?_⟩
          · refine ⟨(hpne.1 head2 ?_).symm, hpne.2.1 a ha⟩
            simp
          · rw [wbtw_cons] at ht
            grind [List.pairwise_iff_forall_sublist]

Goal state after:
case cons.refine_1.refine_2
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
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ Triplewise (Sbtw R) tail

case cons.refine_1.refine_3
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
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ ∀ (a : P), head :: tail ≠ [a, a]
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : IsOrderedRing R
x y : V
⊢ affineSegment R x y = segment R x y

Tactic:
segment_eq_image_lineMap,

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : IsOrderedRing R
x y : V
⊢ affineSegment R x y = ⇑(lineMap x y) '' Set.Icc 0 1
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
w x z : P
h₁ : Wbtw R w x z
h : w ≠ x
h₂ : Wbtw R x w z
⊢ False

Tactic:
exact h (h₁.swap_left_iff.1 h₂)

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✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R w x z
h₂ : Wbtw R x y z
h : w ≠ x
⊢ w ≠ y

Tactic:
rintro rfl
  exact h (h₁.swap_left_iff.1 h₂)

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ (f.symm.trans f).symm = (ofSet {b | (f.symm b).isSome = true}).symm

Tactic:
simp [symm_trans_rev, self_trans_symm, -symm_symm]

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✝¹ : Zero R
inst✝ : One R
⊢ (toPEquiv σ).symm.toMatrix = Perm.permMatrix R σ⁻¹

Tactic:
← Equiv.toPEquiv_symm,

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Zero R
inst✝ : One R
⊢ (Equiv.symm σ).toPEquiv.toMatrix = Perm.permMatrix R σ⁻¹
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✝ : NonAssocSemiring R
σ τ : Perm n
⊢ Perm.permMatrix R (τ⁻¹ * σ⁻¹) = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹

Tactic:
permMatrix_mul

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ✝ τ✝ : Perm n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
σ τ : Perm n
⊢ Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹ = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹
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
⊢ 0 ≠ 1

Tactic:
decide

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 n
inst✝ : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
⊢ Option.casesOn (f.toPEquiv.symm j) 0 (M i) = M.submatrix id (⇑f.symm) i j

Tactic:
← Equiv.toPEquiv_symm,

Goal state after:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
⊢ Option.casesOn (f.symm.toPEquiv j) 0 (M i) = M.submatrix id (⇑f.symm) i j
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 m
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : m → α
j : n
⊢ (a ᵥ* σ.toPEquiv.toMatrix) j = (a ∘ ⇑σ.symm) j

Tactic:
simp [toMatrix, ← σ.eq_symm_apply, vecMul, dotProduct]

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

Goal state before:
pp: case h.none
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬f i = g i
hf : f i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ g i then 1 else 0

Tactic:
rcases hg : g i with - | gi

Goal state after:
case h.none.none
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬f i = g i
hf : f i = none
hg : g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0

case h.none.some
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬f i = g i
hf : f i = none
gi : n
hg : g i = some gi
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ some gi then 1 else 0
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case h.some
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬f i = g i
fi : n
hf : f i = some fi
⊢ ∃ x, ¬(if x ∈ some fi then 1 else 0) = if x ∈ g i then 1 else 0

Tactic:
· use fi
    simp [hf.symm, Ne.symm hi]

Goal state after: