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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_4
inst✝ : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (∃ m u, toEuclideanLin.symm (toContinuousLinearMap.symm (∑ i, ((rankOne 𝕜) (u i)) (u i))) = M) ↔
    ∃ m v, M = ∑ i, vecMulVec (v i) (star (v i))

Tactic:
coe_toContinuousLinearMap_symm,

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_4
inst✝ : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (∃ m u, toEuclideanLin.symm ↑(∑ i, ((rankOne 𝕜) (u i)) (u i)) = M) ↔ ∃ m v, M = ∑ i, vecMulVec (v i) (star (v i))
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f ≤ f.closure

pp: case neg
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : ¬f.IsClosable
⊢ f ≤ f.closure

Tactic:
· refine le_of_le_graph ?_
    rw [← hf.graph_closure_eq_closure_graph]
    exact (graph f).le_topologicalClosure

Goal state after:
case neg
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : ¬f.IsClosable
⊢ f ≤ f.closure
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
h1 : (fun a ↦ a.swap) '' ↑f.graph = ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' ↑f.graph
h2 :
  (fun a ↦ a.swap) '' closure[instTopologicalSpaceProd] ↑f.graph =
    ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' closure[instTopologicalSpaceProd] ↑f.graph
⊢ closure[instTopologicalSpaceProd] (Prod.swap '' ↑f.graph) ⊆ Prod.swap '' closure[instTopologicalSpaceProd] ↑f.graph

Tactic:
rw [h1, h2]

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
h1 : (fun a ↦ a.swap) '' ↑f.graph = ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' ↑f.graph
h2 :
  (fun a ↦ a.swap) '' closure[instTopologicalSpaceProd] ↑f.graph =
    ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' closure[instTopologicalSpaceProd] ↑f.graph
⊢ closure[instTopologicalSpaceProd] (⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' ↑f.graph) ⊆
    ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' closure[instTopologicalSpaceProd] ↑f.graph
Module: Mathlib.Dynamics.BirkhoffSum.Average

Goal state before:
pp: R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : ↑n ≠ 0
⊢ (↑n)⁻¹ • n • g x = g x

Tactic:
← Nat.cast_smul_eq_nsmul R,

Goal state after:
R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : ↑n ≠ 0
⊢ (↑n)⁻¹ • ↑n • g x = g x
Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic

Goal state before:
pp: case hg_ker
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
⊢ ↑(↑((↑f).eqLocus ↑1).orthogonalProjectionOnto).ker ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(↑f - 1).range

Tactic:
rw [Submodule.ker_orthogonalProjectionOnto, ← Submodule.topologicalClosure_coe,
      SetLike.coe_subset_coe, ← Submodule.orthogonal_orthogonal_eq_closure]

Goal state after:
case hg_ker
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
⊢ ((↑f).eqLocus ↑1)ᗮ ≤ (↑f - 1).rangeᗮᗮ
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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
⊢ (∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ - ⟪a, x.2⟫ = 0) → ∃ (x_1 : x.1 ∈ T†.domain), ↑T† ⟨x.1, ⋯⟩ = x.2

Tactic:
intro h
    simp_rw [sub_eq_zero] at h
    have hx : x.fst ∈ T†.domain := by
      apply mem_adjoint_domain_of_exists
      use x.snd
      rintro ⟨a, ha⟩
      rw [← inner_conj_symm, ← h a ha, inner_conj_symm]
    use hx
    apply hT.eq_of_inner_right 𝕜
    rintro a ha
    rw [← h a ha, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩]

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

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
ι : Type u_6
ι' : Type u_7
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
x : E ⊗[𝕜] F
e : OrthonormalBasis ι 𝕜 E
f : OrthonormalBasis ι' 𝕜 F
⊢ inner 𝕜 x x = ↑(∑ i, ‖((e.toBasis.tensorProduct f.toBasis).repr x) i‖ ^ 2)

Tactic:
by
  classical
  have : x = ∑ i : ι, ∑ j : ι', (e.toBasis.tensorProduct f.toBasis).repr x (i, j) • e i ⊗ₜ f j := by
    conv_lhs => rw [← (e.toBasis.tensorProduct f.toBasis).sum_repr x]
    simp [← Finset.sum_product', Basis.tensorProduct_apply']
  conv_lhs => rw [this]
  simp only [inner_def, map_sum, LinearMap.sum_apply]
  simp [OrthonormalBasis.inner_eq_ite, ← Finset.sum_product', RCLike.mul_conj]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
hausdorffMeasure_pi_real,

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ volume (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c✝ : ℝ
c : ℝ := -c✝
hc : 0 < c
x : H
⊢ ‖x‖ ^ 2 * c = re ((starRingEnd 𝕜) ((algebraMap ℝ 𝕜) c) * ⟪x, x⟫_𝕜)

Tactic:
RCLike.algebraMap_eq_ofReal,

Goal state after:
𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c✝ : ℝ
c : ℝ := -c✝
hc : 0 < c
x : H
⊢ ‖x‖ ^ 2 * c = re ((starRingEnd 𝕜) ↑c * ⟪x, x⟫_𝕜)
Module: Mathlib.Analysis.InnerProductSpace.Trace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : Module.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ RCLike.re ((trace 𝕜 E) T) = ∑ i, hT.eigenvalues hn i

Tactic:
by
  rw [hT.trace_eq_sum_eigenvalues]
  exact RCLike.ofReal_re_ax _

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 := 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
n : ℕ
hn : 1 ≤ n
npos : 0 < ↑n
x : ι → ℝ
hx : ∀ (i : ι), ↑(a i) < x i ∧ x i < ↑(b i)
f : γ n := fun i ↦ ⟨⌊(x i - ↑(a i)) * ↑n⌋₊, ⋯⟩
i : ι
⊢ ↑(a i) + (x i - ↑(a i)) * ↑n / ↑n ≤ ↑(a i) + (↑⌊(x i - ↑(a i)) * ↑n⌋₊ + 1) / ↑n

Tactic:
by
          gcongr
          exact (Nat.lt_floor_add_one _).le

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
h_tendsto : Tendsto (fun n ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n ↦ (c ^ n)⁻¹ • u n)
hf : IsVonNBounded 𝕜' (Set.range fun x ↦ (σ c ^ x)⁻¹ • f (u x))
this✝ : Tendsto (fun n ↦ σ c ^ n) atTop (𝓝 0)
this : Tendsto ((fun n ↦ σ c ^ n) • fun n ↦ (σ c ^ n)⁻¹ • f (u n)) atTop (𝓝 0)
⊢ Tendsto (⇑f ∘ u) atTop (𝓝 0)

Tactic:
exact this.congr fun n ↦ by simp [c_ne]

Goal state after:
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
this : ⟪o.rightAngleRotationAux₁ y, o.rightAngleRotationAux₁ x⟫ = ⟪y, x⟫
⊢ -(o.areaForm y) (o.rightAngleRotationAux₁ x) = ⟪y, -x⟫

Tactic:
← o.inner_rightAngleRotationAux₁_left,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
this : ⟪o.rightAngleRotationAux₁ y, o.rightAngleRotationAux₁ x⟫ = ⟪y, x⟫
⊢ -⟪o.rightAngleRotationAux₁ y, o.rightAngleRotationAux₁ x⟫ = ⟪y, -x⟫
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.kahler (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.kahler x) y

Tactic:
by
  simp only [kahler_rightAngleRotation_left, kahler_rightAngleRotation_right]
  linear_combination -o.kahler x y * Complex.I_sq

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

Goal state before:
pp: case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (⟪a, x⟫ + ((o.areaForm x) a * 0 - 0 * 1)) * (⟪a, y⟫ + ((o.areaForm a) y * 0 - 0 * 1)) -
      (0 + ((o.areaForm x) a * 1 + 0 * 0)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) =
    ‖a‖ ^ 2 * (⟪x, y⟫ + ((o.areaForm x) y * 0 - 0 * 1)) - 0 * (0 + ((o.areaForm x) y * 1 + 0 * 0))

Tactic:
o.areaForm_swap x a

Goal state after:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (⟪a, x⟫ + (-(o.areaForm a) x * 0 - 0 * 1)) * (⟪a, y⟫ + ((o.areaForm a) y * 0 - 0 * 1)) -
      (0 + (-(o.areaForm a) x * 1 + 0 * 0)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) =
    ‖a‖ ^ 2 * (⟪x, y⟫ + ((o.areaForm x) y * 0 - 0 * 1)) - 0 * (0 + ((o.areaForm x) y * 1 + 0 * 0))
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (⟪a, x⟫ + ((o.areaForm x) a * 0 - 0 * 1)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) +
      (0 + ((o.areaForm x) a * 1 + 0 * 0)) * (⟪a, y⟫ + ((o.areaForm a) y * 0 - 0 * 1)) =
    ‖a‖ ^ 2 * (0 + ((o.areaForm x) y * 1 + 0 * 0)) + 0 * (⟪x, y⟫ + ((o.areaForm x) y * 0 - 0 * 1))

Tactic:
o.areaForm_swap x a

Goal state after:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (⟪a, x⟫ + (-(o.areaForm a) x * 0 - 0 * 1)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) +
      (0 + (-(o.areaForm a) x * 1 + 0 * 0)) * (⟪a, y⟫ + ((o.areaForm a) y * 0 - 0 * 1)) =
    ‖a‖ ^ 2 * (0 + ((o.areaForm x) y * 1 + 0 * 0)) + 0 * (⟪x, y⟫ + ((o.areaForm x) y * 0 - 0 * 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ↑s ≠ -↑m

Tactic:
← Complex.ofReal_natCast,

Goal state after:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ↑s ≠ -↑↑m
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
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
⊢ rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)

Tactic:
dsimp only [f]

Goal state after:
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
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
⊢ rexp (-x) * x ^ (u - 1) = (rexp (-c * x) * x ^ (c * (u - 1))) ^ (1 / c)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ (∫ (x : ℝ) in 0..π / 2, ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n)) -
      ∫ (x : ℝ) in 0..π / 2, (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)) =
    ∫ (x : ℝ) in 0..π / 2,
      -((↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z)))

pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ n - 1 ≠ 0

Tactic:
← integral_sub

Goal state after:
case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ ∫ (x : ℝ) in 0..π / 2,
      ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
        (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)) =
    ∫ (x : ℝ) in 0..π / 2,
      -((↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z)))

case e'_3.hf
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ IntervalIntegrable (fun x ↦ ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n)) volume 0 (π / 2)

case e'_3.hg
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ IntervalIntegrable (fun x ↦ (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))) volume 0 (π / 2)

case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ n - 1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f 1 + log (↑(m - 1)! * ↑m) = f 1 + log ↑m !

Tactic:
←
    Nat.cast_mul

Goal state after:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f 1 + log ↑((m - 1)! * m) = f 1 + log ↑m !
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ log (Γ x) = log (Γ x) - log (Γ 1)

Tactic:
Gamma_one,

Goal state after:
x : ℝ
hx : 0 < x
⊢ log (Γ x) = log (Γ x) - log 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
⊢ EqOn f Γ (Ioi 0)

Tactic:
suffices EqOn (log ∘ f) (log ∘ Gamma) (Ioi (0 : ℝ)) from
    fun x hx ↦ log_injOn_pos (hf_pos hx) (Gamma_pos_of_pos hx) (this hx)
  intro x hx
  have e1 := BohrMollerup.tendsto_logGammaSeq hf_conv ?_ hx
  · rw [Function.comp_apply (f := log) (g := f) (x := 1), hf_one, log_one, sub_zero] at e1
    exact tendsto_nhds_unique e1 (BohrMollerup.tendsto_log_gamma hx)
  · intro y hy
    rw [Function.comp_apply, Function.comp_apply, hf_feq hy, log_mul hy.ne' (hf_pos hy).ne']
    ring

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

Goal state before:
pp: ⊢ √π * Γ 1 * 2 ^ 0 / √π = 1

Tactic:
Gamma_one,

Goal state after:
⊢ √π * 1 * 2 ^ 0 / √π = 1
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
t : V → Set ℝ
ht : ∀ i ∈ Metric.sphere 0 1, t i ∈ atTop
u : V → Set V
hu : ∀ i ∈ Metric.sphere 0 1, u i ∈ 𝓝 i
smul_subset_s : ∀ i ∈ Metric.sphere 0 1, t i • u i ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, x ∈ Metric.sphere 0 1
h₂ : Metric.sphere 0 1 ⊆ ⋃ x ∈ cover, u x
x : P
hx : ‖x -ᵥ p‖ ∈ Set.Ioi 0 ∩ ⋂ x ∈ cover, t x
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
⊢ x' ∈ Metric.sphere 0 1

Tactic:
mem_sphere_zero_iff_norm,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
t : V → Set ℝ
ht : ∀ i ∈ Metric.sphere 0 1, t i ∈ atTop
u : V → Set V
hu : ∀ i ∈ Metric.sphere 0 1, u i ∈ 𝓝 i
smul_subset_s : ∀ i ∈ Metric.sphere 0 1, t i • u i ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, x ∈ Metric.sphere 0 1
h₂ : Metric.sphere 0 1 ⊆ ⋃ x ∈ cover, u x
x : P
hx : ‖x -ᵥ p‖ ∈ Set.Ioi 0 ∩ ⋂ x ∈ cover, t x
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
⊢ ‖x'‖ = 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
n : ℕ
hn : x ≤ ↑n
⊢ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) = f n x

Tactic:
dsimp only [f]

Goal state after:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
n : ℕ
hn : x ≤ ↑n
⊢ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) = (Ioc 0 ↑n).indicator (fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ Tendsto (fun x ↦ z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 (↑π / sin (↑π * z)))

Tactic:
have : ↑π / sin (↑π * z) = 1 * (π / sin (π * z)) := by rw [one_mul]

Goal state after:
case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun x ↦ z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 (↑π / sin (↑π * z)))
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
hq : q.re = 0
n : ℕ
⊢ (↑(2 * n)!)⁻¹ • q ^ (2 * n) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)

Tactic:
have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq

Goal state after:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : q ^ 2 = -↑(normSq q)
⊢ (↑(2 * n)!)⁻¹ • q ^ (2 * n) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case inr
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Tactic:
have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq

Goal state after:
case inr
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:

Tactic:
_ = (g.roots.map (fun x ↦ NormedField.toMulRingNorm K (a - x))).prod := rfl
  _ = ‖(g.roots.map (fun x ↦ a - x)).prod‖ := by
    rw [g.roots.prod_hom' (NormedField.toMulRingNorm K) (fun x : K ↦ a - x)]
    rfl
  _ = ‖g.eval a‖ := by
    congr
    rw [hg.eval_eq_prod_roots_of_monic hgm]
  _ ≤ ‖g.eval a - f.eval a‖ + ‖f.eval a‖ := by
    convert! norm_add_le (g.eval a - f.eval a) (f.eval a)
    simp
  _ = ‖(∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i - f.coeff i) * X ^ i).eval a‖ := by
    rw [← eval_sub]
    simp only [ha, norm_zero, add_zero]
    rw [(g - f).as_sum_range' (g.natDegree + 1)]
    · congr
      simp [← C_mul_X_pow_eq_monomial]
    · simpa [hdeg, Nat.lt_succ_iff] using g.natDegree_sub_le f
  _ ≤ ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ := by
    have := norm_sum_le (Finset.range (g.natDegree + 1))
        (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
    simpa [eval_mul, eval_finsetSum] using this
    -- The following tactic does not work here:
    -- simpa [eval_mul, eval_finsetSum] using norm_sum_le (Finset.range (g.natDegree + 1))
    --     (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
  _ < _ := by
    rw [hdeg]
    convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_
    · simp [mul_assoc]
    · simp only [Finset.mem_range, norm_mul, norm_pow]
      intro i hi
      apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
      · simpa [← map_sub] using hcoeff i
      · refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_
        exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)
      all_goals positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedField L
inst✝ : NormedAlgebra K L
f g : K[X]
ε : ℝ
hε : 0 < ε
a : L
ha : (aeval a) f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : (map (algebraMap K L) g).Splits
⊢ eval ?m.110 (map (algebraMap K L) f) = 0

Tactic:
simpa using ha

Goal state after: