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

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
x : 𝕜₂
y : E →SWOT[σ] F
⊢ (fun x_1 ↦
      match x_1 with
      | (x_2, y_1) => y_1 ((x • y) x_2)) =
    (RingHom.id 𝕜₂) x • fun x ↦
      match x with
      | (x, y_1) => y_1 (y x)

Tactic:
ext

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
x : 𝕜₂
y : E →SWOT[σ] F
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (match x✝ with
    | (x_1, y_1) => y_1 ((x • y) x_1)) =
    ((RingHom.id 𝕜₂) x • fun x ↦
        match x with
        | (x, y_1) => y_1 (y x))
      x✝
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0 ↔ SameRay ℝ x y

Tactic:
constructor

Goal state after:
case neg.mp
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

case neg.mpr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
⊢ SameRay ℝ x y → 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0
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
⊢ ↑⟪x, y⟫ + (o.areaForm x) y • Complex.I = (starRingEnd ℂ) (↑⟪y, x⟫ + (o.areaForm y) x • Complex.I)

Tactic:
real_inner_comm,

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
⊢ ↑⟪y, x⟫ + (o.areaForm x) y • Complex.I = (starRingEnd ℂ) (↑⟪y, x⟫ + (o.areaForm y) x • Complex.I)
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
⊢ IntegrableOn (fun t ↦ t ^ (s.re - 1) * ‖f t‖) (Ioi 0) volume

Tactic:
exact mellin_convergent_of_isBigO_scalar hfc.norm hf_top.norm_left hs_top hf_bot.norm_left hs_bot

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

Goal state before:
pp: f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
⊢ (fun n ↦ f n ^ n) = fun n ↦ (1 + (f n - 1)) ^ n

Tactic:
ext

Goal state after:
f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
x✝ : ℕ
⊢ f x✝ ^ x✝ = (1 + (f x✝ - 1)) ^ x✝
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ 1 - ↑(x / a) = ↑(1 - x / a)

Tactic:
by norm_cast

Goal state after:
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
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n !) ≤ f (x + ↑(n + 1))

Tactic:
add_comm x _

Goal state after:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n !) ≤ f (↑(n + 1) + x)
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
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn bound (Ioi 0) volume
t : ℝ
ht : t ∈ Ioi 0
y : ℂ
x✝ : y ∈ Metric.ball s v
ht' : ↑t ≠ 0
⊢ HasDerivAt (fun z ↦ ↑t ^ (z - 1)) (↑t ^ (y - 1) * ↑(log t)) y

Tactic:
convert! ((hasDerivAt_id' y).sub_const 1).const_cpow (Or.inl ht') using 1

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
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn bound (Ioi 0) volume
t : ℝ
ht : t ∈ Ioi 0
y : ℂ
x✝ : y ∈ Metric.ball s v
ht' : ↑t ≠ 0
⊢ ↑t ^ (y - 1) * ↑(log t) = ↑t ^ (y - 1) * Complex.log ↑t * 1
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
v : V
p : P
⊢ asymptoticNhds k V v +ᵥ pure p = asymptoticNhds k P v

Tactic:
simp_rw [asymptoticNhds, vadd_pure, map_iSup, map_map, Function.comp_def]
  refine (Equiv.vaddConst p).iSup_congr fun _ => ?_
  simp [add_vadd]

Goal state after:
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
s t : Set P
⊢ asymptoticCone k (s ∪ t) = asymptoticCone k s ∪ asymptoticCone k t

Tactic:
ext

Goal state after:
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
s t : Set P
x✝ : V
⊢ x✝ ∈ asymptoticCone k (s ∪ t) ↔ x✝ ∈ asymptoticCone k s ∪ asymptoticCone k t
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
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : IsStrictOrderedRing k
inst✝³ : IsTopologicalAddGroup V
inst✝² : ContinuousSMul k V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
s : Set P
⊢ asymptoticCone k (closure[inst✝¹] s) = asymptoticCone k s

Tactic:
ext

Goal state after:
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
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : IsStrictOrderedRing k
inst✝³ : IsTopologicalAddGroup V
inst✝² : ContinuousSMul k V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
s : Set P
x✝ : V
⊢ x✝ ∈ asymptoticCone k (closure[inst✝¹] s) ↔ x✝ ∈ asymptoticCone k s
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
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
⊢ asymptoticCone k (asymptoticCone k s) = asymptoticCone k s

Tactic:
ext

Goal state after:
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
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
x✝ : V
⊢ x✝ ∈ asymptoticCone k (asymptoticCone k s) ↔ x✝ ∈ asymptoticCone k s
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) 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ ∧ ‖(f.comp g).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
constructor

Goal state after:
case left
𝕜 : 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) 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

case right
𝕜 : 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).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖
Module: Mathlib.Analysis.Normed.Affine.MazurUlam

Goal state before:
pp: E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e ↦ dist (↑e z) z)
R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z
e : PE ≃ᵢ PE
hx : e x = x
hy : e y = y
⊢ f e ∈ s

Tactic:
constructor

Goal state after:
case left
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y : PE
z : PE := ⋯
s : Set (PE ≃ᵢ PE) := ⋯
this : Nonempty ↑s
h_bdd : BddAbove (range fun e ↦ dist (↑e z) z)
R : PE ≃ᵢ PE := ⋯
f : PE ≃ᵢ PE → PE ≃ᵢ PE := ⋯
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z
e : PE ≃ᵢ PE
hx : e x = x
hy : e y = y
⊢ (f e) x = x

case right
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y : PE
z : PE := ⋯
s : Set (PE ≃ᵢ PE) := ⋯
this : Nonempty ↑s
h_bdd : BddAbove (range fun e ↦ dist (↑e z) z)
R : PE ≃ᵢ PE := ⋯
f : PE ≃ᵢ PE → PE ≃ᵢ PE := ⋯
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z
e : PE ≃ᵢ PE
hx : e x = x
hy : e y = y
⊢ (f e) y = y
Module: Mathlib.Analysis.Normed.Affine.MazurUlam

Goal state before:
pp: E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
⊢ f.toRealAffineIsometryEquiv.toIsometryEquiv = f

Tactic:
ext

Goal state after:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x✝ : PE
⊢ f.toRealAffineIsometryEquiv.toIsometryEquiv x✝ = f x✝
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

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

Tactic:
constructor

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

case mpr
s : ℂ
⊢ (∃ m, s = -↑m) → Gamma s = 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
⊢ AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ

Tactic:
refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ

Goal state after:
s : ℂ
⊢ DifferentiableOn ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ

Tactic:
refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ

Goal state after:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ DifferentiableOn ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: 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) ∧ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, ↑n ∈ {1}ᶜ

Tactic:
constructor

Goal state after:
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)

case right
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, ↑n ∈ {1}ᶜ
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: case pos
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : Summable fun n ↦ (expSeries ℚ R n) fun x_1 ↦ x.fst
⊢ (∑' (n : ℕ), (expSeries ℚ (tsze R M) n) fun x_1 ↦ x) =
    inl (∑' (n : ℕ), (expSeries ℚ R n) fun x_1 ↦ x.fst) + inr ((∑' (n : ℕ), (expSeries ℚ R n) fun x_1 ↦ x.fst) • x.snd)

Tactic:
refine (hasSum_expSeries_of_smul_comm ℚ x hx ?_).tsum_eq

Goal state after:
case pos
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : Summable fun n ↦ (expSeries ℚ R n) fun x_1 ↦ x.fst
⊢ HasSum (fun n ↦ (expSeries ℚ R n) fun x_1 ↦ x.fst) (∑' (n : ℕ), (expSeries ℚ R n) fun x_1 ↦ x.fst)
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊

Tactic:
ext

Goal state after:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ↑‖x‖₊ = ↑(‖x.fst‖₊ + ‖x.snd‖₊)
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: z w : ℂ
⊢ ↑(z + w) = ↑z + ↑w

Tactic:
ext

Goal state after:
case a
z w : ℂ
⊢ (↑(z + w)).re = (↑z + ↑w).re

case a
z w : ℂ
⊢ (↑(z + w)).imI = (↑z + ↑w).imI

case a
z w : ℂ
⊢ (↑(z + w)).imJ = (↑z + ↑w).imJ

case a
z w : ℂ
⊢ (↑(z + w)).imK = (↑z + ↑w).imK
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: z w : ℂ
⊢ ↑(z * w) = ↑z * ↑w

Tactic:
ext

Goal state after:
case a
z w : ℂ
⊢ (↑(z * w)).re = (↑z * ↑w).re

case a
z w : ℂ
⊢ (↑(z * w)).imI = (↑z * ↑w).imI

case a
z w : ℂ
⊢ (↑(z * w)).imJ = (↑z * ↑w).imJ

case a
z w : ℂ
⊢ (↑(z * w)).imK = (↑z * ↑w).imK
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: r : ℝ
z : ℂ
⊢ r • ↑z = ↑r * ↑z

Tactic:
ext

Goal state after:
case a
r : ℝ
z : ℂ
⊢ (r • ↑z).re = (↑r * ↑z).re

case a
r : ℝ
z : ℂ
⊢ (r • ↑z).imI = (↑r * ↑z).imI

case a
r : ℝ
z : ℂ
⊢ (r • ↑z).imJ = (↑r * ↑z).imJ

case a
r : ℝ
z : ℂ
⊢ (r • ↑z).imK = (↑r * ↑z).imK
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
p : ℝ[X]
n : ℕ
hp : p.IsMonicOfDegree (2 * n)
⊢ M ^ n ≤ ‖(aeval x) p‖

Tactic:
by
  induction n generalizing p with
  | zero => simp_all
  | succ n ih =>
    rw [mul_add, mul_one] at hp
    obtain ⟨f₁, f₂, hf₁, hf₂, H⟩ := hp.eq_isMonicOfDegree_two_mul_isMonicOfDegree
    obtain ⟨a, b, hab⟩ := isMonicOfDegree_two_iff'.mp hf₁
    rw [H, aeval_mul, norm_mul, mul_comm, pow_succ, hab, aeval_eq_φ x (a, b)]
    exact mul_le_mul (ih hf₂) (h (a, b)) hM (norm_nonneg _)

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

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : ‖φ x u‖ * ‖(aeval x) p‖ = ‖(aeval x) (q w ^ n) - (aeval x) ((q w - q u) ^ n)‖
⊢ ‖(aeval x) (q w ^ n) - (aeval x) ((q w - q u) ^ n)‖ ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
norm_sub_rev (φ ..)

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : ‖φ x u‖ * ‖(aeval x) p‖ = ‖(aeval x) (q w ^ n) - (aeval x) ((q w - q u) ^ n)‖
⊢ ‖(aeval x) (q w ^ n) - (aeval x) ((q w - q u) ^ n)‖ ≤ M ^ n + ‖φ x w - φ x u‖ ^ n
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
refine (if_pos h).trans_le (mul_nonneg ?_ ?_) <;>
            · change _ ≤ ite _ _ _
              split_ifs
              exacts [le_rfl, zero_le_one]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : DecidableEq R✝
inst✝³ : NoZeroDivisors R✝
inst✝² : Nontrivial R✝
R : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
N : MulRingNorm R
⊢ (fun v ↦
        { toFun := v.toFun, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯,
          eq_zero_of_map_eq_zero' := ⋯ })
      ((fun N ↦ { toFun := N.toFun, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }) N) =
    N

Tactic:
constructor

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
⊢ ∃ (_ : 0 < B.norm (B c.1 * B c.2)), ∀ (x y : L), B.norm (x * y) ≤ B.norm (B c.1 * B c.2) * B.norm x * B.norm y

Tactic:
constructor

Goal state after:
case h.h
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
⊢ ∀ (x y : L), B.norm (x * y) ≤ B.norm (B c.1 * B c.2) * B.norm x * B.norm y

case h.w
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
⊢ 0 < B.norm (B c.1 * B c.2)
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯ ↔ z ∈ ⊥
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = σ.symm z
⊢ ‖z - z'‖ ≤ max ‖z‖ ‖z'‖

Tactic:
simpa [norm_neg, sub_eq_add_neg] using (IsUltrametricDist.norm_add_le_max z (- z'))

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
⊢ closedBall 0 (‖c‖ ^ n * r) = c ^ n • closedBall 0 r

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
x✝ : 𝕜
⊢ x✝ ∈ closedBall 0 (‖c‖ ^ n * r) ↔ x✝ ∈ c ^ n • closedBall 0 r
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : ¬n = 0
⊢ ↑(mu μ hn n) / ↑n ≤ 1

Tactic:
rw [div_le_one (cast_pos.mpr (Nat.pos_of_ne_zero hn0)), cast_le]
    exact mu_le _ _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ (Set.range fun x_1 ↦ μ (x ^ s (ψ ↑x_1)) ^ (1 / ↑(ψ ↑x_1))) = Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
x✝ : ℝ
⊢ (x✝ ∈ Set.range fun x_1 ↦ μ (x ^ s (ψ ↑x_1)) ^ (1 / ↑(ψ ↑x_1))) ↔
    x✝ ∈ Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))