mathlib-initiative/mathlib-tactics huggingface dataset:
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
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : (x, 0) ∈ f.closure.graph
⊢ (0, x) ∈ f'.graph

Tactic:
rw [← h, inverse_graph hf]

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
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : (x, 0) ∈ f.closure.graph
⊢ (0, x) ∈ (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph).topologicalClosure
Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
⊢ UniformEquicontinuous (birkhoffAverage 𝕜 f g)

Tactic:
refine Metric.uniformity_basis_dist_le.uniformEquicontinuous_iff_right.2 fun ε hε ↦ ?_

Goal state after:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ), (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2) ∈ {p | dist p.1 p.2 ≤ ε}
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case mp
𝕜 : 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
y : WithLp 2 (F × E)
h1 :
  ∀ (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
h2 : y.ofLp = x
a : E
b : F
hab : (a, b) ∈ g
⊢ ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
← h2,

Goal state after:
case mp
𝕜 : 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
y : WithLp 2 (F × E)
h1 :
  ∀ (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
h2 : y.ofLp = x
a : E
b : F
hab : (a, b) ∈ g
⊢ ⟪b, y.ofLp.1⟫ - ⟪a, y.ofLp.2⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case mp
𝕜 : 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
y : WithLp 2 (F × E)
h1 :
  ∀ (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
h2 : y.ofLp = x
a : E
b : F
hab : (a, b) ∈ g
⊢ ⟪b, y.ofLp.1⟫ - ⟪a, y.ofLp.2⟫ = 0

Tactic:
WithLp.ofLp_fst,

Goal state after:
case mp
𝕜 : 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
y : WithLp 2 (F × E)
h1 :
  ∀ (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
h2 : y.ofLp = x
a : E
b : F
hab : (a, b) ∈ g
⊢ ⟪b, y.fst⟫ - ⟪a, y.ofLp.2⟫ = 0
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖↑e.symm‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p
C₂ : ℝ≥0 := ‖↑e‖₊
v : E → F' := ⇑e ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ
h4v : ∀ (x : E), ‖fderiv ℝ v x‖ ≤ ↑C₂ * ‖fderiv ℝ u x‖
⊢ ↑‖↑toEuclidean.symm‖₊ * ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) *
      (↑‖↑toEuclidean‖₊ * eLpNorm (fderiv ℝ u) (↑p) μ) =
    ↑‖↑toEuclidean.symm‖₊ * ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * ↑‖↑toEuclidean‖₊ * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
simp_rw [mul_assoc]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : EMetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℕ
hf : Isometry f
s : Set X
⊢ volume.addHaarScalarFactor μH[↑d] • μH[↑d] (f '' s) = volume.addHaarScalarFactor μH[↑d] • μH[↑d] s

Tactic:
rw [Isometry.hausdorffMeasure_image hf (by simp)]

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
this : Encodable ↑s
⊢ dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)

Tactic:
rw [biUnion_eq_iUnion, dimH_iUnion, ← iSup_subtype'']

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

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun x ↦ (pre m ↑x) s) atBot (𝓝 ((mkMetric' m) s))

Tactic:
simp only [mkMetric', OuterMeasure.iSup_apply, iSup_subtype']

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun x ↦ (pre m ↑x) s) atBot (𝓝 (⨆ i, (pre m ↑i) s))
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
c : 𝕜
hc : ¬c = 0
h : f.ker = ⊥
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(c • f).range := bv.map (LinearIsometryEquiv.ofEq f.range (c • f).range ⋯)
this : finrank 𝕜 U = Fintype.card (Fin (finrank 𝕜 U))
⊢ ‖((toMatrix bu.toBasis bv'.toBasis) (c • f).rangeRestrict).det‖ =
    ‖c ^ Fintype.card (Fin (finrank 𝕜 U)) * ((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
← Matrix.det_smul,

Goal state after:
case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
c : 𝕜
hc : ¬c = 0
h : f.ker = ⊥
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(c • f).range := bv.map (LinearIsometryEquiv.ofEq f.range (c • f).range ⋯)
this : finrank 𝕜 U = Fintype.card (Fin (finrank 𝕜 U))
⊢ ‖((toMatrix bu.toBasis bv'.toBasis) (c • f).rangeRestrict).det‖ =
    ‖(c • (toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜) (inner_ 𝕜 y x) = inner_ 𝕜 x y

Tactic:
by
  simp only [inner_, map_sub, map_add, map_mul, map_inv₀, map_ofNat, conj_ofReal, conj_I]
  rw [add_comm y x, norm_sub_rev]
  by_cases hI : (I : 𝕜) = 0
  · simp only [hI, neg_zero, zero_mul]
  have hI' := I_mul_I_of_nonzero hI
  have I_smul (v : E) : ‖(I : 𝕜) • v‖ = ‖v‖ := by rw [norm_smul, norm_I_of_ne_zero hI, one_mul]
  have h₁ : ‖(I : 𝕜) • y - x‖ = ‖(I : 𝕜) • x + y‖ := by
    convert I_smul ((I : 𝕜) • x + y)
    linear_combination (norm := module) -hI' • x
  have h₂ : ‖(I : 𝕜) • y + x‖ = ‖(I : 𝕜) • x - y‖ := by
    convert (I_smul ((I : 𝕜) • y + x)).symm
    linear_combination (norm := module) -hI' • y
  rw [h₁, h₂]
  ring

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

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x y : H
⊢ (starRingEnd ℝ) ⟪y, x⟫.re = ⟪x, y⟫.re

Tactic:
simp only [← ipc.conj_inner_symm x y, conj_trivial]

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x y : H
⊢ ⟪y, x⟫.re = ((starRingEnd ℂ) ⟪y, x⟫).re
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
h : x ∈ S.mulI.mulI
⊢ x ∈ S

Tactic:
mem_mapEquiv_iff (scalarSMulCLE H UnitI),

Goal state after:
case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
h : (scalarSMulCLE H UnitI).symm x ∈ S.mulI
⊢ x ∈ S
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
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
x✝ : Nontrivial V
v : V
hv : v ≠ 0
h : ∀ (x : X →₀ V →L[𝕜] V) (x_1 : V), 0 ≤ RCLike.re (x.sum fun i a ↦ x.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 x_1), a x_1⟫_𝕜)
ff : X × V →₀ 𝕜
⊢ 0 ≤ RCLike.re (ff.sum fun x' v' ↦ ff.sum fun x v ↦ (starRingEnd 𝕜) v * v' * ⟪(K x'.1 x.1) x.2, x'.2⟫_𝕜)

Tactic:
convert! h (ff.sum fun xv z ↦ .single xv.1 ((z / ‖v‖ ^ 2) • (innerSL 𝕜 v).smulRight xv.2)) v

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
x✝ : Nontrivial V
v : V
hv : v ≠ 0
h : ∀ (x : X →₀ V →L[𝕜] V) (x_1 : V), 0 ≤ RCLike.re (x.sum fun i a ↦ x.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 x_1), a x_1⟫_𝕜)
ff : X × V →₀ 𝕜
⊢ (ff.sum fun x' v' ↦ ff.sum fun x v ↦ (starRingEnd 𝕜) v * v' * ⟪(K x'.1 x.1) x.2, x'.2⟫_𝕜) =
    (ff.sum fun xv z ↦ Finsupp.single xv.1 ((z / ↑‖v‖ ^ 2) • ((innerSL 𝕜) v).smulRight xv.2)).sum fun i a ↦
      (ff.sum fun xv z ↦ Finsupp.single xv.1 ((z / ↑‖v‖ ^ 2) • ((innerSL 𝕜) v).smulRight xv.2)).sum fun i_1 a_1 ↦
        ⟪(K i i_1) (a_1 v), a v⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
b a : F
x✝ : F →WOT[𝕜] F
| ⟪x✝ b, a⟫_𝕜

Tactic:
rw [← inner_conj_symm, ← RCLike.star_def]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
b a : F
x✝ : F →WOT[𝕜] F
| star ⟪a, x✝ b⟫_𝕜
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✝ : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜' (⇑f '' V)
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜'), r ≤ ‖c‖ → ⇑f '' V ⊆ c • U
x : 𝕜
hx : r < ‖x‖
⊢ r ≤ ‖σ x‖

Tactic:
by simpa using hx.le

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

Goal state before:
pp: case h
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : IsTopologicalAddGroup E
inst✝⁷ : ContinuousSMul 𝕜₁ E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₂ F
inst✝¹ : T1Space E
inst✝ : MontelSpace 𝕜₁ E
a : Set E
b : Set F
ha : IsVonNBounded 𝕜₁ (a, b).1
hb : (a, b).2 ∈ 𝓝 0
⊢ (IsCompact (closure[inst✝⁹] a, b).1 ∧ (closure[inst✝⁹] a, b).2 ∈ 𝓝 0) ∧
    ∀ x ∈ {f | ∀ x ∈ (closure[inst✝⁹] a, b).1, f x ∈ (closure[inst✝⁹] a, b).2},
      (LinearEquiv.toCompactConvergenceCLM σ E F).symm x ∈ {f | ∀ x ∈ (a, b).1, f x ∈ (a, b).2}

Tactic:
exact ⟨⟨MontelSpace.isCompact_of_isClosed_of_isVonNBounded 𝕜₁ isClosed_closure
      ha.closure, hb⟩, fun _ hf _ hx ↦ hf _ (subset_closure hx)⟩

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 : E
K : Submodule ℝ E := ℝ ∙ x
this✝¹ : finrank ℝ ↥K ≤ {x}.card
this✝ : {x}.card = 1
this : finrank ℝ ↥K + finrank ℝ ↥Kᗮ = finrank ℝ E
⊢ 0 < finrank ℝ ↥Kᗮ

Tactic:
have : finrank ℝ E = 2 := Fact.out

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this✝² : finrank ℝ ↥K ≤ {x}.card
this✝¹ : {x}.card = 1
this✝ : finrank ℝ ↥K + finrank ℝ ↥Kᗮ = finrank ℝ E
this : finrank ℝ E = 2
⊢ 0 < finrank ℝ ↥Kᗮ
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hf : IntegrableOn (fun x ↦ |(-rexp (-x))| • ↑((rexp ∘ Neg.neg) x) ^ (↑σ - 1) • f ((rexp ∘ Neg.neg) x)) univ volume
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
⊢ Integrable (fun x ↦ cexp (-↑σ * ↑x) • f (rexp (-x))) volume

Tactic:
simpa [rexp_cexp_aux] using hf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ log (1 + -z)⁻¹ = z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹

Tactic:
rw [log_inv _ <| slitPlane_arg_ne_pi hz, neg_eq_iff_eq_neg, ← neg_mul]

Goal state after:
z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ log (1 + -z) = -z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
⊢ (fun z ↦ log (1 + z) - logTaylor (n + 1) z) =O[𝓝 0] fun z ↦ z ^ (n + 1)

Tactic:
Asymptotics.isBigO_iff

Goal state after:
n : ℕ
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ c * ‖x ^ (n + 1)‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : 0 < ↑n
⊢ f ↑n + x * log ↑n = (1 - x) * f ↑n + x * f (↑n + 1)

Tactic:
rw [hf_feq hn']

Goal state after:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : 0 < ↑n
⊢ f ↑n + x * log ↑n = (1 - x) * f ↑n + x * (f ↑n + log ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
suffices ∀ m : ℕ, ↑m < x → x ≤ m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 <| f x - f 1) by
    refine this ⌈x - 1⌉₊ ?_ ?_
    · rcases lt_or_ge x 1 with ⟨⟩
      · rwa [Nat.ceil_eq_zero.mpr (by linarith : x - 1 ≤ 0), Nat.cast_zero]
      · convert! Nat.ceil_lt_add_one (by linarith : 0 ≤ x - 1)
        abel
    · rw [← sub_le_iff_le_add]; exact Nat.le_ceil _
  intro m
  induction m generalizing x with
  | zero =>
    rw [Nat.cast_zero, zero_add]
    exact fun _ hx' => tendsto_logGammaSeq_of_le_one hf_conv (@hf_feq) hx hx'
  | succ m hm =>
    intro hy hy'
    rw [Nat.cast_succ, ← sub_le_iff_le_add] at hy'
    rw [Nat.cast_succ, ← lt_sub_iff_add_lt] at hy
    specialize hm ((Nat.cast_nonneg _).trans_lt hy) hy hy'
    -- now massage gauss_product n (x - 1) into gauss_product (n - 1) x
    have :
      ∀ᶠ n : ℕ in atTop,
        logGammaSeq (x - 1) n =
          logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1) := by
      refine Eventually.mp (eventually_ge_atTop 1) (Eventually.of_forall fun n hn => ?_)
      have := logGammaSeq_add_one (x - 1) (n - 1)
      rw [sub_add_cancel, Nat.sub_add_cancel hn] at this
      rw [this]
      ring
    replace hm :=
      ((Tendsto.congr' this hm).add (tendsto_const_nhds : Tendsto (fun _ => log (x - 1)) _ _)).comp
        (tendsto_add_atTop_nat 1)
    have :
      ((fun x_1 : ℕ =>
            (fun n : ℕ =>
                  logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1))
                x_1 +
              (fun b : ℕ => log (x - 1)) x_1) ∘
          fun a : ℕ => a + 1) =
        fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n) := by
      ext1 n
      dsimp only [Function.comp_apply]
      rw [sub_add_cancel, Nat.add_sub_cancel]
    rw [this] at hm
    convert! hm.sub (tendsto_log_nat_add_one_sub_log.const_mul x) using 2
    · ring
    · have := hf_feq ((Nat.cast_nonneg m).trans_lt hy)
      rw [sub_add_cancel] at this
      rw [this]
      ring

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: a s : ℂ
hs : 0 < s.re + a.re
this :
  MellinConvergent (fun t ↦ ↑t ^ a • (Ioc 0 1).indicator (fun x ↦ 1) t) s ∧
    mellin ((Ioc 0 1).indicator fun x ↦ 1) (s + a) = 1 / (s + a)
⊢ HasMellin ((Ioc 0 1).indicator fun t ↦ ↑t ^ a) s (1 / (s + a))

Tactic:
← mellin_cpow_smul,

Goal state after:
a s : ℂ
hs : 0 < s.re + a.re
this :
  MellinConvergent (fun t ↦ ↑t ^ a • (Ioc 0 1).indicator (fun x ↦ 1) t) s ∧
    mellin (fun t ↦ ↑t ^ a • (Ioc 0 1).indicator (fun x ↦ 1) t) s = 1 / (s + a)
⊢ HasMellin ((Ioc 0 1).indicator fun t ↦ ↑t ^ a) s (1 / (s + a))
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → V
v : V
p : P
hf : Tendsto f l (asymptoticNhds k V v)
⊢ Tendsto (fun x ↦ f x +ᵥ p) l (asymptoticNhds k P v)

Tactic:
rw [← asymptoticNhds_vadd_pure, vadd_pure]
  exact tendsto_map.comp hf

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

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

Tactic:
rpow_zero,

Goal state after:
⊢ √π * 1 / √π = 1
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst✝²] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
ht : c ≤ t
h : t • u +ᵥ p ∈ s
⊢ SameRay k ((c • u +ᵥ p) -ᵥ p) ((t • u +ᵥ p) -ᵥ (c • u +ᵥ p))

Tactic:
vadd_vsub,

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst✝²] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
ht : c ≤ t
h : t • u +ᵥ p ∈ s
⊢ SameRay k (c • u) ((t • u +ᵥ p) -ᵥ (c • u +ᵥ p))
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
rw [norm_def, max_le_iff]
  constructor
  · calc
      ‖f.comp g 0‖ = ‖f (g 0)‖ := by simp
      _ = ‖f.contLinear (g 0) + f 0‖ := by rw [f.decomp]; simp
      _ ≤ ‖f.contLinear‖ * ‖g 0‖ + ‖f 0‖ := by grw [norm_add_le, f.contLinear.le_opNorm]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by grw [f.norm_contLinear_le, g.norm_image_zero_le]
  · calc
      ‖(f.comp g).contLinear‖ ≤ ‖f.contLinear‖ * ‖g.contLinear‖ :=
        (g.comp_contLinear f).symm ▸ f.contLinear.opNorm_comp_le _
      _ ≤ ‖f‖ * ‖g‖ := by grw [f.norm_contLinear_le, g.norm_contLinear_le]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by rw [le_add_iff_nonneg_right]; apply norm_nonneg

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

Goal state before:
pp: case mp
s : ℂ
⊢ Gamma s = 0 → ∃ m, s = -↑m

Tactic:
contrapose!

Goal state after:
case mp
s : ℂ
⊢ (∀ (m : ℕ), s ≠ -↑m) → Gamma s ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case left
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝 1)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
⊢ ‖x - (algebraMap ℂ F) w‖ ≤ M * (1 + (‖x - (algebraMap ℂ F) w - (x - (algebraMap ℂ F) y)‖ / M) ^ n)

Tactic:
sub_sub_sub_cancel_left,

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
⊢ ‖x - (algebraMap ℂ F) w‖ ≤ M * (1 + (‖(algebraMap ℂ F) y - (algebraMap ℂ F) w‖ / M) ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: x : ℝ
⊢ ∑' (n : ℕ), x ^ (2 * n) / ↑(2 * n)! ≤ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x ^ 2 / 2)

Tactic:
refine x.hasSum_cosh.summable.tsum_le_tsum (fun i ↦ ?_) <| expSeries_summable' (x ^ 2 / 2)

Goal state after:
x : ℝ
i : ℕ
⊢ x ^ (2 * i) / ↑(2 * i)! ≤ (↑i !)⁻¹ • (x ^ 2 / 2) ^ i