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

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : ℕ → ℝ := fun n ↦ (ϕ ∘ u) (n + 1)
⊢ 0 ≤ 2 * ϕ (u 0)

Tactic:
by specialize nonneg x; positivity

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
⊢ (c • T).IsPositive

Tactic:
by
  have hc' : starRingEnd 𝕜 c = c := by
    simp [conj_eq_iff_im, ← (le_iff_re_im.mp hc).right]
  refine ⟨hT.left.smul hc', fun x => ?_⟩
  rw [smul_apply, inner_smul_left, hc', mul_re, conj_eq_iff_im.mp hc', zero_mul, sub_zero]
  exact mul_nonneg ((re_nonneg_of_nonneg hc').mpr hc) (re_inner_nonneg_left hT x)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
x : E
hx : 0 < ⟪x, T x⟫
⊢ 0 ≤ α

Tactic:
have := by simpa [inner_smul_right] using h.inner_nonneg_right x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
x : E
hx : 0 < ⟪x, T x⟫
this : 0 ≤ α * ⟪x, T x⟫
⊢ 0 ≤ α
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
y : ℝ
⊢ ‖deriv (u ∘ update x i) y‖ₑ = ‖(fderiv ℝ u (update x i y)) (deriv (update x i) y)‖ₑ

Tactic:
rw [fderiv_comp_deriv _ (hu.differentiable one_ne_zero).differentiableAt
          (hasDerivAt_update x i y).differentiableAt]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
⊢ (S ∘SL T ∘SL adjoint S).IsPositive

Tactic:
by
  refine isPositive_def'.mpr ⟨hT.isSelfAdjoint.conj_adjoint S, fun x => ?_⟩
  rw [reApplyInnerSelf, comp_apply, ← adjoint_inner_right]
  exact hT.re_inner_nonneg_left _

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ∃ C, 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖

Tactic:
by
  rcases coercive with ⟨C, C_ge_0, coercivity⟩
  refine ⟨C, C_ge_0, ?_⟩
  intro v
  by_cases h : 0 < ‖v‖
  · refine (mul_le_mul_iff_left₀ h).mp ?_
    calc
      C * ‖v‖ * ‖v‖ ≤ B v v := coercivity v
      _ = ⟪B♯ v, v⟫_ℝ := (continuousLinearMapOfBilin_apply B v v).symm
      _ ≤ ‖B♯ v‖ * ‖v‖ := real_inner_le_norm (B♯ v) v
  · have : v = 0 := by simpa using h
    simp [this]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a✝ b✝ : F
hx : a✝ ∈ {y | Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)}
hy : b✝ ∈ {y | Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)}
⊢ a✝ + b✝ ∈ {y | Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)}

Tactic:
by rw [Set.mem_ofPred_eq, LinearMap.map_add] at *; exact hx.add hy

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
⊢ ∃ y,
    (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
        (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
      y.ofLp = x

Tactic:
refine ⟨toLp 2 x, ?_, rfl⟩

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
⊢ ∀ (u : WithLp 2 (F × E)) (x_1 : E) (x_2 : F),
    (x_1, x_2) ∈ g → toLp 2 (x_2, -x_1) = u → ⟪u.fst, (toLp 2 x).fst⟫ + ⟪u.snd, (toLp 2 x).snd⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
a b : ℕ
hl : b ≤ a
ha : a ∈ ↑T.singularValues.support
⊢ b ∈ ↑T.singularValues.support

Tactic:
rw [Finset.mem_coe, Finsupp.mem_support_iff, ← singularValues_pos_iff_ne_zero] at ⊢ ha

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
a b : ℕ
hl : b ≤ a
ha : 0 < T.singularValues a
⊢ 0 < T.singularValues b
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    (‖f‖ ^ 2 • @Matrix.gram E (Fin n) 𝕜 inst✝⁶.toInner e) i j - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j =
      @Matrix.gram F (Fin n) 𝕜 inst✝⁴.toInner (⇑f ∘ e) i j
⊢ ‖(LinearMap.rTensor G ↑f) x‖ ^ 2 ≤ (‖f‖ * ‖x‖) ^ 2

Tactic:
Matrix.smul_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • @Matrix.gram E (Fin n) 𝕜 inst✝⁶.toInner e i j - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j =
      @Matrix.gram F (Fin n) 𝕜 inst✝⁴.toInner (⇑f ∘ e) i j
⊢ ‖(LinearMap.rTensor G ↑f) x‖ ^ 2 ≤ (‖f‖ * ‖x‖) ^ 2
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤ RCLike.re (∑ x, ∑ x_1, inner 𝕜 (g x_1) (g x) * ∑ c, Matrix.vecMulVec (A c) (star (A c)) x_1 x)

Tactic:
Finset.mul_sum

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤ RCLike.re (∑ x, ∑ x_1, ∑ i, inner 𝕜 (g x_1) (g x) * Matrix.vecMulVec (A i) (star (A i)) x_1 x)
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
⊢ dimH univ = dimH univ

Tactic:
← e.dimH_preimage,

Goal state after:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
⊢ dimH univ = dimH (⇑e ⁻¹' univ)
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: U : Type u_5
inst✝² : NormedAddCommGroup U
inst✝¹ : InnerProductSpace ℝ U
inst✝ : FiniteDimensional ℝ U
f : U →ₗ[ℝ] U
⊢ f.normDet = |LinearMap.det f|

Tactic:
by
  simpa using f.normDet_eq_norm_det

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
⊢ μH[d₂] s = 0 ∨ μH[d₁] s = ∞

Tactic:
by_contra! H
  suffices ∀ c : ℝ≥0, c ≠ 0 → μH[d₂] s ≤ c * μH[d₁] s by
    rcases ENNReal.exists_nnreal_pos_mul_lt H.2 H.1 with ⟨c, hc0, hc⟩
    exact hc.not_ge (this c (pos_iff_ne_zero.1 hc0))
  intro c hc
  refine le_iff'.1 (mkMetric_mono_smul ENNReal.coe_ne_top (mod_cast hc) ?_) s
  have : 0 < ((c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹) := by
    rw [← ENNReal.coe_rpow_of_ne_zero hc, pos_iff_ne_zero, Ne, ENNReal.coe_eq_zero,
      NNReal.rpow_eq_zero_iff]
    exact mt And.left hc
  filter_upwards [Ico_mem_nhdsGE this]
  rintro r ⟨hr₀, hrc⟩
  lift r to ℝ≥0 using ne_top_of_lt hrc
  rw [Pi.smul_apply, smul_eq_mul,
    ← ENNReal.div_le_iff_le_mul (Or.inr ENNReal.coe_ne_top) (Or.inr <| mt ENNReal.coe_eq_zero.1 hc)]
  rcases eq_or_ne r 0 with (rfl | hr₀)
  · rcases lt_or_ge 0 d₂ with (h₂ | h₂)
    · simp only [h₂, ENNReal.zero_rpow_of_pos, zero_le, ENNReal.zero_div, ENNReal.coe_zero]
    · simp only [h.trans_le h₂, ENNReal.div_top, zero_le, ENNReal.zero_rpow_of_neg,
        ENNReal.coe_zero]
  · have : (r : ℝ≥0∞) ≠ 0 := by simpa only [ENNReal.coe_eq_zero, Ne] using hr₀
    rw [← ENNReal.rpow_sub _ _ this ENNReal.coe_ne_top]
    refine (ENNReal.rpow_lt_rpow hrc (sub_pos.2 h)).le.trans ?_
    rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (sub_pos.2 h).ne', ENNReal.rpow_one]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
C : ℝ
s : Set X
hC : ∀ x ∈ s, ‖kerFun H x‖ ≤ C
ι : Type u_5
l : Filter ι
F : ι → H
f : H
h : Tendsto F l (𝓝 f)
ε : ℝ
hε : ε > 0
hnorm : Tendsto (fun x ↦ ‖F x - f‖ * C) l (𝓝 0)
n : ι
hn : ‖F n - f‖ * C < ε
x : X
hx : x ∈ s
⊢ ‖(F n - f) x‖ < ε

Tactic:
norm_apply_le,

Goal state after:
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
C : ℝ
s : Set X
hC : ∀ x ∈ s, ‖kerFun H x‖ ≤ C
ι : Type u_5
l : Filter ι
F : ι → H
f : H
h : Tendsto F l (𝓝 f)
ε : ℝ
hε : ε > 0
hnorm : Tendsto (fun x ↦ ‖F x - f‖ * C) l (𝓝 0)
n : ι
hn : ‖F n - f‖ * C < ε
x : X
hx : x ∈ s
⊢ ‖F n - f‖ * √‖kernel H x x‖ < ε
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ 1 ≤ μH[0] {x}

Tactic:
· rw [hausdorffMeasure_apply]
    suffices
      (1 : ℝ≥0∞) ≤
        ⨅ (t : ℕ → Set X) (_ : {x} ⊆ ⋃ n, t n) (_ : ∀ n, ediam (t n) ≤ 1),
          ∑' n, ⨆ _ : (t n).Nonempty, ediam (t n) ^ (0 : ℝ) by
      apply le_trans this _
      convert! le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one
      rfl
    simp only [ENNReal.rpow_zero, le_iInf_iff]
    intro t hst _
    rcases mem_iUnion.1 (hst (mem_singleton x)) with ⟨m, hm⟩
    have A : (t m).Nonempty := ⟨x, hm⟩
    calc
      (1 : ℝ≥0∞) = ⨆ h : (t m).Nonempty, 1 := by simp only [A, ciSup_pos]
      _ ≤ ∑' n, ⨆ h : (t n).Nonempty, 1 := ENNReal.le_tsum _

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : I * I = -1
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖(I * I) • x + y‖ * 𝓚 ‖(I * I) • x + y‖ -
        I * 𝓚 ‖(I * I) • x - y‖ * 𝓚 ‖(I * I) • x - y‖) =
    4⁻¹ *
      (-I *
        (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
          I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖))

Tactic:
hI',

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : I * I = -1
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-1 • x + y‖ * 𝓚 ‖-1 • x + y‖ -
        I * 𝓚 ‖-1 • x - y‖ * 𝓚 ‖-1 • x - y‖) =
    4⁻¹ *
      (-I *
        (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
          I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
hs : MeasurableSet s
⊢ (Measure.map f μH[d]) s = (μH[d].restrict (range f)) s

Tactic:
map_apply hf.continuous.measurable hs,

Goal state after:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
hs : MeasurableSet s
⊢ μH[d] (f ⁻¹' s) = (μH[d].restrict (range f)) s
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
⊢ liminf (fun n ↦ ∑ i, ediam (t n i) ^ ↑(Fintype.card ι)) atTop ≤ liminf (fun n ↦ ∑ i, (1 / ↑n) ^ Fintype.card ι) atTop

Tactic:
by
      refine liminf_le_liminf ?_ ?_
      · filter_upwards [B] with _ hn
        apply Finset.sum_le_sum fun i _ => _
        simp only [ENNReal.rpow_natCast]
        intro i _
        exact pow_le_pow_left' (hn i) _
      · isBoundedDefault

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := ⋯
t : (n : ℕ) → γ n → Set (ι → ℝ) := ⋯
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
i : ι
x✝ : i ∈ Finset.univ
⊢ ∀ (n : ℕ),
    1 ≤ n →
      (ENNReal.ofReal ∘ (fun x ↦ ↑⌈(↑(b i) - ↑(a i)) * x⌉₊ / x) ∘ Nat.cast) n =
        (fun n ↦ ↑⌈(↑(b i) - ↑(a i)) * ↑n⌉₊ / ↑n) n

Tactic:
intro n hn

Goal state after:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
i : ι
x✝ : i ∈ Finset.univ
n : ℕ
hn : 1 ≤ n
⊢ (ENNReal.ofReal ∘ (fun x ↦ ↑⌈(↑(b i) - ↑(a i)) * x⌉₊ / x) ∘ Nat.cast) n = (fun n ↦ ↑⌈(↑(b i) - ↑(a i)) * ↑n⌉₊ / ↑n) n
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪o.rightAngleRotationAux₁ y, x⟫ = -(o.areaForm x) y

Tactic:
simp [o.areaForm_swap y x]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ Integrable (fun x ↦ ‖f c u x‖ ^ (1 / c)) (volume.restrict (Ioi 0))

Tactic:
apply Integrable.congr (GammaIntegral_convergent hu)

Goal state after:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := ⋯
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ (fun x ↦ rexp (-x) * x ^ (u - 1)) =ᵐ[volume.restrict (Ioi 0)] fun x ↦ ‖f c u x‖ ^ (1 / c)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
w : ℝ
hw1 : 0 < w
hw2 : w < a - s.re
⊢ ∃ v, 0 < v ∧ v < s.re - b ∧ v < a - s.re

Tactic:
obtain ⟨w', hw1', hw2'⟩ := exists_between (sub_pos.mpr hs_bot)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
w : ℝ
hw1 : 0 < w
hw2 : w < a - s.re
w' : ℝ
hw1' : 0 < w'
hw2' : w' < s.re - b
⊢ ∃ v, 0 < v ∧ v < s.re - b ∧ v < a - s.re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
⊢ ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    ∫ (x_1 : ℝ) in 0..x, ↑(rexp (-x)) * (↑x_1 ^ (s - 1) * (↑x - ↑x_1) ^ (t - 1))

Tactic:
congr 1 with y : 1

Goal state after:
case e_f
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
⊢ ↑(rexp (-y)) * ↑y ^ (s - 1) * (↑(rexp (-(x - y))) * ↑(x - y) ^ (t - 1)) =
    ↑(rexp (-x)) * (↑y ^ (s - 1) * (↑x - ↑y) ^ (t - 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ log 2 * 1 / 2 - log (3 / 2) < 0

Tactic:
div_sub' two_ne_zero

Goal state after:
case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
⊢ ∃ w' fs',
    ∑ j ∈ fs', w' j = 1 ∧
      (Finset.affineCombination k fs' p) w' = p' ∧
        ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑fs' \ {↑i}).indicator w' j

Tactic:
classical
  let fsx : s → Finset ι := fun i ↦ insert (i : ι) (fs i)
  have hfsx : ∀ i, (i : ι) ∈ fsx i := by simp [fsx]
  let wx : s → ι → k := fun i ↦ Set.indicator (fs i) (w i)
  have hwx : ∀ i, ∑ j ∈ fsx i, wx i j = 1 := by
    intro i
    simp_rw [← hw i, fsx, wx]
    by_cases hi : (i : ι) ∈ fs i <;> simpa [hi] using Finset.sum_congr rfl (by aesop)
  have hp'x : ∀ i : s, p' ∈ line[k, p i, (fsx i).affineCombination k p (wx i)] := by
    intro i
    convert! hp' i using 4
    simp_rw [fsx, wx]
    exact (Finset.affineCombination_indicator_subset _ _ (by simp)).symm
  obtain ⟨w', fs', h⟩ := hp.exists_affineCombination_eq_smul_eq_aux hs hfsx hwx hp'x
  refine ⟨w', fs', h.1, h.2.1, fun i ↦ ?_⟩
  obtain ⟨r, hr⟩ := h.2.2 i
  refine ⟨r, fun j ↦ ?_⟩
  convert! hr j using 2
  simp only [Set.indicator_apply, Set.mem_sdiff, SetLike.mem_coe, Set.mem_singleton_iff,
    Finset.coe_insert, Set.insert_sdiff_of_mem, fsx, wx]
  grind

Goal state after: