mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty ↑s
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(affineSpan ℝ s).direction := AffineIsometryEquiv.constVSub ℝ ⟨hne.some, ⋯⟩
hs_eq : s = Subtype.val '' Subtype.val ⁻¹' s
⊢ (interior (⇑φ '' Subtype.val ⁻¹' s)).Nonempty

Tactic:
← AffineIsometryEquiv.coe_toHomeomorph,

Goal state after:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty ↑s
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(affineSpan ℝ s).direction := AffineIsometryEquiv.constVSub ℝ ⟨hne.some, ⋯⟩
hs_eq : s = Subtype.val '' Subtype.val ⁻¹' s
⊢ (interior (⇑φ.toHomeomorph '' Subtype.val ⁻¹' s)).Nonempty
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ (starRingEnd 𝕜) ↑(re r) * inner_ 𝕜 x y + inner_ 𝕜 ((↑(im r) * I) • x) y =
    (starRingEnd 𝕜) (↑(re r) + ↑(im r) * I) * inner_ 𝕜 x y

Tactic:
← smul_smul,

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ (starRingEnd 𝕜) ↑(re r) * inner_ 𝕜 x y + inner_ 𝕜 (↑(im r) • I • x) y =
    (starRingEnd 𝕜) (↑(re r) + ↑(im r) * I) * inner_ 𝕜 x y
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inl.inr.inl
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
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
hd : 0 ≤ 0
⊢ 1 ≤ μH[0] s

Tactic:
exact one_le_hausdorffMeasure_zero_of_nonempty ⟨f x, 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)
⊢ o.rightAngleRotation.symm = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)

Tactic:
rw [rightAngleRotation]
  exact LinearIsometryEquiv.toLinearIsometry_injective rfl

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
hx : x ≠ 0
i : Fin 2
⊢ ![x, o.rightAngleRotation x] i ≠ 0

Tactic:
fin_cases i <;> simp [hx]

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
| cexp (-↑x)

Tactic:
← cpow_one (cexp _)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
| cexp (-↑x) ^ 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case pos
m : ℕ
hs : -↑m ≠ 0
⊢ deriv Gamma (-↑(m - 1)) = Gamma (-↑m) + -↑m * 0

pp: case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 1 ≤ m

Tactic:
deriv_zero_of_not_differentiableAt (not_differentiableAt_Gamma_neg_nat (m - 1)),

Goal state after:
case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 0 = Gamma (-↑m) + -↑m * 0

case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 1 ≤ m
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case pos
m : ℕ
hs : -↑m ≠ 0
⊢ deriv Gamma (-↑m + 1) = Gamma (-↑m) + -↑m * deriv Gamma (-↑m)

Tactic:
rw [← sub_neg_eq_add, ← neg_sub', ← Nat.cast_one, ← Nat.cast_sub,
      deriv_zero_of_not_differentiableAt (not_differentiableAt_Gamma_neg_nat m),
      deriv_zero_of_not_differentiableAt (not_differentiableAt_Gamma_neg_nat (m - 1)),
      Gamma_neg_nat_eq_zero, zero_add, mul_zero]

Goal state after:
case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 1 ≤ m
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

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

Tactic:
convert! (config := { sameFun := true })
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _ using 2

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

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

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

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

Goal state before:
pp: case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ -1 < (u - 1).re

Tactic:
rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]

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

Goal state before:
pp: x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ log (Γ (a * x + (1 - a) * y)) ≤ log (Γ x ^ a * Γ y ^ (1 - a))

pp: case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ x ^ a ≠ 0

pp: case hy
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ y ^ (1 - a) ≠ 0

pp: case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Γ y

pp: case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Γ x

Tactic:
· gcongr
    exact Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma hx hy ha hb hab

Goal state after:
case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ x ^ a ≠ 0

case hy
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ y ^ (1 - a) ≠ 0

case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Γ y

case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Γ x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
⊢ 0 < u.re - 1 - -1

Tactic:
sub_neg_eq_add,

Goal state after:
u : ℂ
hu : 0 < u.re
⊢ 0 < u.re - 1 + 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_2
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
⊢ ∀ᶠ (b : ℕ) in atTop, f x - f 1 - x * (log (↑b + 1) - log ↑b) ≤ logGammaSeq x b

Tactic:
filter_upwards with n

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

Goal state before:
pp: s : ℝ
hs : s ≠ 0
⊢ (s + 1).doublingGamma = s * s.doublingGamma

Tactic:
rw [doublingGamma, doublingGamma, (by abel : s + 1 - 1 = s - 1 + 1), add_div, add_assoc,
    add_halves (1 : ℝ), Gamma_add_one (div_ne_zero hs two_ne_zero), rpow_add two_pos, rpow_one]
  ring

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ pure v ≤ asymptoticNhds k V 0

Tactic:
rw [← map_const (f := atTop (α := k))]

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ map (fun x ↦ v) atTop ≤ asymptoticNhds k V 0
Module: Mathlib.Analysis.Normed.Affine.Ceva

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
r : Fin 3 → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i) = p i
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
⊢ ∏ x, dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2))) (r x)) =
    ∏ x, dist ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2))) (r x)) (t.points (x + 2))

Tactic:
dist_lineMap_right,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
r : Fin 3 → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i) = p i
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
⊢ ∏ x, dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2))) (r x)) =
    ∏ x, ‖1 - r x‖ * dist (t.points (x + 1)) (t.points (x + 2))
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
v : V
s : Set P
p : P
t₁ : Set k
ht₁ : t₁ ∈ atTop
t₂ : Set V
hs : t₁ • t₂ ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
x✝ : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : c ∈ Set.Ioi 0
⊢ ∀ a ∈ (fun x ↦ c • x) '' t₂, a ∈ (fun x ↦ x +ᵥ p) ⁻¹' s

Tactic:
Set.forall_mem_image

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
v : V
s : Set P
p : P
t₁ : Set k
ht₁ : t₁ ∈ atTop
t₂ : Set V
hs : t₁ • t₂ ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
x✝ : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : c ∈ Set.Ioi 0
⊢ ∀ ⦃x : V⦄, x ∈ t₂ → c • x ∈ (fun x ↦ x +ᵥ p) ⁻¹' s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hf
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ -1 < (s - 1).re

Tactic:
rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]

Goal state after:
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)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
i : ↑s
hi : ↑i ∈ fs i
⊢ ∀ x ∈ fs i, (↑(fs i)).indicator (w i) x = w i x

Tactic:
by aesop

Goal state after:
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)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
i : ↑s
hi : ↑i ∉ fs i
⊢ ∀ x ∈ fs i, (↑(fs i)).indicator (w i) x = w i x

Tactic:
by aesop

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

Goal state before:
pp: case pos.negSucc
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.negSucc a✝)
⊢ Gamma (1 + ↑a✝) * Gamma (1 - (1 + ↑a✝)) = 0

Tactic:
sub_add_cancel_left,

Goal state after:
case pos.negSucc
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.negSucc a✝)
⊢ Gamma (1 + ↑a✝) * Gamma (-↑a✝) = 0
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)

Tactic:
rcases hr (Equiv.swap 0 j) with ⟨x, hx⟩

Goal state after:
case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)
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:
WithLp.norm_seminormedAddCommGroupToProd

Goal state after:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ‖WithLp.toLp 1 x‖ = ‖x.fst‖ + ‖x.snd‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)! =
    ((z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)! + (z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)!) / 2 +
      ((z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! + (z ^ 2) ^ k * (I ^ 2) ^ k * (-z * I) / ↑(2 * k + 1)!) / 2

Tactic:
← two_mul,

Goal state after:
case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)! =
    2 * ((z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)!) / 2 +
      ((z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! + (z ^ 2) ^ k * (I ^ 2) ^ k * (-z * I) / ↑(2 * k + 1)!) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! / I =
    -((z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! + (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)!) * I / 2

Tactic:
← two_mul,

Goal state after:
case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! / I =
    -(2 * ((z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)!)) * I / 2
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝⁶ : SeminormedCommRing R
S : Type u_2
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
f✝ : AlgebraNorm R S
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra A S
inst✝ : IsScalarTower R A S
hinj : Function.Injective ⇑(algebraMap A S)
f : AlgebraNorm R S
x : A
⊢ f ((algebraMap A S) (-x)) = f ((algebraMap A S) x)

Tactic:
simp only [map_neg, map_neg_eq_map]

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
⊢ ∃ b ∈ g.aroots L, ‖a - b‖ < ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1

Tactic:
obtain ⟨b, h1, h2⟩ := exists_roots_norm_sub_lt_of_norm_coeff_sub_lt hε
      (f := f.map (algebraMap K L)) (by simpa using ha) (hfm.map _) (hgm.map _)
      (by simpa using hdeg) (by simpa [← map_sub] using hcoeff) hg

Goal state after:
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
b : L
h1 : b ∈ (map (algebraMap K L) g).roots
h2 : ‖a - b‖ < ((↑(map (algebraMap K L) f).natDegree + 1) * ε) ^ (↑(map (algebraMap K L) f).natDegree)⁻¹ * max ‖a‖ 1
⊢ ∃ b ∈ g.aroots L, ‖a - b‖ < ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
⊢ seminormFromBounded' f (x * y) ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
by
  apply ciSup_le
  by_cases hy : seminormFromBounded' f y = 0
  · rw [seminormFromBounded_eq_zero_iff f_nonneg f_mul] at hy
    intro z
    rw [mul_comm x y, mul_assoc, map_mul_zero_of_map_zero f_nonneg f_mul hy (x * z), zero_div]
    exact mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul x)
      (seminormFromBounded_nonneg f_nonneg f_mul y)
  · intro z
    rw [← div_le_iff₀ (lt_of_le_of_ne' (seminormFromBounded_nonneg f_nonneg f_mul _) hy)]
    apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z
    rw [div_le_iff₀ (lt_of_le_of_ne' (seminormFromBounded_nonneg f_nonneg f_mul _) hy),
      div_mul_eq_mul_div]
    by_cases hz : f z = 0
    · have hxyz : f (z * (x * y)) = 0 := map_mul_zero_of_map_zero f_nonneg f_mul hz _
      simp_rw [mul_comm, hxyz, zero_div]
      exact div_nonneg (mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul y) (f_nonneg _))
        (f_nonneg _)
    · rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), mul_comm (f (x * z))]
      by_cases hxz : f (x * z) = 0
      · rw [mul_comm x y, mul_assoc, mul_comm y, map_mul_zero_of_map_zero f_nonneg f_mul hxz y]
        exact mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul y) (f_nonneg _)
      · rw [← div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hxz)]
        apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) (x * z)
        rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hxz), mul_comm x y, mul_assoc]

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

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : NormedField L
inst✝ : Algebra K L
hd : DenseRange ⇑(algebraMap K L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : ¬f.natDegree = 0
c : ℕ → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L) (c i)) < ε
hdeg : (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i).natDegree = f.natDegree
⊢ ∃ g, g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖(map (algebraMap K L) g).coeff n - f.coeff n‖ < ε

Tactic:
use C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : NormedField L
inst✝ : Algebra K L
hd : DenseRange ⇑(algebraMap K L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : ¬f.natDegree = 0
c : ℕ → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L) (c i)) < ε
hdeg : (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i).natDegree = f.natDegree
⊢ (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i).Monic ∧
    f.natDegree = (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i).natDegree ∧
      ∀ (n : ℕ),
        ‖(map (algebraMap K L) (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i)).coeff n - f.coeff n‖ < ε
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ (fun y ↦ f (x * y) / f y) y ≤ f x * 1

Tactic:
← div_self hy0,

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ (fun y ↦ f (x * y) / f y) y ≤ f x * (f y / f y)
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
hf : RingHom.IsBoundedWrt (⇑nα) nβ f
x : α
⊢ nβ (f x) ≤ nα x

Tactic:
obtain ⟨C, hC0, hC⟩ := hf

Goal state after:
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
⊢ nβ (f x) ≤ nα x
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∀ (b : ℕ), 0 ≤ b → seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b

Tactic:
simp only [seminormFromConst_seq, neg_mul, map_neg_eq_map, zero_le, implies_true]

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
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
n : ℕ
| μ x

Tactic:
rw [← rpow_one (μ x)]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
n : ℕ
| μ x ^ 1