mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
⊢ finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = 1 + finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ - 1

Tactic:
Nat.add_sub_cancel_left

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
⊢ finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hc' : c ≠ 0
⊢ ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x ↦ (c • m) (ediam s)) =
    c • ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x ↦ m (ediam s))

Tactic:
smul_iSup,

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hc' : c ≠ 0
⊢ ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x ↦ (c • m) (ediam s)) =
    ⨆ i, ⨆ (_ : i > 0), c • boundedBy (extend fun s x ↦ m (ediam s))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case refine_1
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ i, t n i
u : ℕ → Set X := fun j ↦ ⋃ b ∈ decode₂ (ι n) j, t n b
j : ℕ
⊢ ⨆ i ∈ decode₂ (ι n) j, ediam (t n i) ≤ ε

Tactic:
exact iSup₂_le fun _ _ => (htn _).trans hrn.le

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

Goal state before:
pp: case refine_2
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
x✝¹ : 0 < ε
x✝ : ℕ
⊢ ediam ((fun x_1 ↦ {x}) x✝) ≤ ε

pp: case refine_3
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
x✝ : 0 < ε
⊢ ∑' (n : ℕ), ⨆ (_ : ((fun x_1 ↦ {x}) n).Nonempty), ediam ((fun x_2 ↦ {x}) n) ^ d ≤ 0

Tactic:
· simp only [ediam_singleton, zero_le]

Goal state after:
case refine_3
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
x✝ : 0 < ε
⊢ ∑' (n : ℕ), ⨆ (_ : ((fun x_1 ↦ {x}) n).Nonempty), ediam ((fun x_2 ↦ {x}) n) ^ d ≤ 0
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: case mpr.mem
𝕜 : 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)
inst✝ : ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint
f p x✝ : H →L[𝕜] H
hf : x✝ ∈ Set.range fun s ↦ star s * s
⊢ x✝.IsPositive

Tactic:
obtain ⟨f, rfl⟩ := hf
        simpa using! ContinuousLinearMap.IsPositive.adjoint_conj isPositive_one f

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

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
K : ℝ≥0
f : X → Y
s : Set X
h : LipschitzOnWith K f s
d : ℝ
hd : 0 ≤ d
⊢ μH[d] (f '' s) ≤ ↑K ^ d * μH[d] s

Tactic:
by
  simpa only [NNReal.coe_one, one_mul] using h.holderOnWith.hausdorffMeasure_image_le zero_lt_one hd

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ 0 < ‖r‖₊ ^ d

Tactic:
simp [pos_iff_ne_zero, hr]

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
h : ⟪x, y⟫ = 0
⊢ |(o.areaForm x) y| = ‖x‖ * ‖y‖

Tactic:
o.areaForm_to_volumeForm,

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
h : ⟪x, y⟫ = 0
⊢ |o.volumeForm ![x, y]| = ‖x‖ * ‖y‖
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)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : E
⊢ f (o.rightAngleRotation x) = I * f x

Tactic:
← Complex.rightAngleRotation,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : E
⊢ f (o.rightAngleRotation x) = Complex.orientation.rightAngleRotation (f x)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1) + fun z ↦ (-1) ^ (n + 1 + 1) * z ^ (n + 1) / (↑n + 1))
    (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j + (-1) ^ n * z ^ n) z

Tactic:
refine HasDerivAt.add ih ?_

Goal state after:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (fun z ↦ (-1) ^ (n + 1 + 1) * z ^ (n + 1) / (↑n + 1)) ((-1) ^ n * z ^ n) z
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x ↦ ↑(rexp (-x))) =O[atTop] fun x ↦ x ^ (-(s.re + 1))

pp: case convert_4
s : ℂ
hs : 0 < s.re
⊢ (fun x ↦ ↑(rexp (-x))) =O[𝓝[>] 0] fun x ↦ x ^ (-0)

Tactic:
· rw [← isBigO_norm_left]
    simp_rw [norm_real, isBigO_norm_left]
    simpa only [neg_one_mul] using (isLittleO_exp_neg_mul_rpow_atTop zero_lt_one _).isBigO

Goal state after:
case convert_4
s : ℂ
hs : 0 < s.re
⊢ (fun x ↦ ↑(rexp (-x))) =O[𝓝[>] 0] fun x ↦ x ^ (-0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
⊢ ‖z‖ ^ (n + 1) * ‖∫ (x : ℝ) in 0..1, ↑x ^ n * (1 + ↑x * z)⁻¹‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
mul_div_assoc

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
⊢ ‖z‖ ^ (n + 1) * ‖∫ (x : ℝ) in 0..1, ↑x ^ n * (1 + ↑x * z)⁻¹‖ ≤ ‖z‖ ^ (n + 1) * ((1 - ‖z‖)⁻¹ / (↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case refine_1
z : ℂ
hz : ‖z‖ < 1
⊢ Summable fun i ↦ ‖(-1) ^ (i + 1) * z ^ i / ↑i‖

pp: case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ (i + 1) * z ^ i / ↑i) atTop (nhds (log (1 + z)))

Tactic:
· refine (summable_geometric_of_norm_lt_one hz).norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) ?_
    intro n
    simp only [norm_div, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul, norm_natCast]
    rcases n.eq_zero_or_pos with rfl | hn
    · simp
    conv => enter [2]; rw [← div_one (‖z‖ ^ n)]
    gcongr
    norm_cast

Goal state after:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ (i + 1) * z ^ i / ↑i) atTop (nhds (log (1 + z)))
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 ↑m + log ↑m = f 1 + log ↑m !

Tactic:
IH,

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)! + log ↑m = f 1 + log ↑m !
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n ↦
      ((↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
        ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
⊢ Tendsto (fun n ↦ ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))

Tactic:
mul_div_assoc

Goal state after:
z : ℂ
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n ↦
      (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
          ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
⊢ Tendsto (fun n ↦ ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))
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:
Nat.ceil_le

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) = f n x
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
⊢ asymptoticCone k Set.univ = Set.univ

Tactic:
← AffineSubspace.top_coe k,

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
⊢ asymptoticCone k ↑⊤ = Set.univ
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : SeminormedAddCommGroup W
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : Ring R
inst✝² : Module R W
inst✝¹ : ContinuousConstSMul R W
inst✝ : SMulCommClass 𝕜 R W
p : W × (V →L[𝕜] W)
⊢ ({ toLinearEquiv := decompLinearEquiv 𝕜 R V W, norm_map' := ⋯ }.symm p).contLinear = p.2

Tactic:
decompLinearEquiv_symm_contLinear

Goal state after:
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : SeminormedAddCommGroup W
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : Ring R
inst✝² : Module R W
inst✝¹ : ContinuousConstSMul R W
inst✝ : SMulCommClass 𝕜 R W
p : W × (V →L[𝕜] W)
⊢ p.2 = p.2
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
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ e, dist (↑e z) z
this : c ≤ 0
e : PE ≃ᵢ PE
hx : e x = x
hy : e y = y
⊢ dist (e z) z ≤ c

Tactic:
exact le_ciSup h_bdd ⟨e, hx, hy⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: 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
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₁ x₂ : Fin (2 + 1)
hx : (x₁, x₂).1 < (x₁, x₂).2
⊢ ∀ ⦃a₂ : { x // x.1 < x.2 }⦄,
    (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(x₁, x₂), hx⟩ =
        (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) a₂ →
      ⟨(x₁, x₂), hx⟩ = a₂

Tactic:
⟨⟨y₁, y₂⟩, hy⟩

Goal state after:
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
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₁ x₂ : Fin (2 + 1)
hx : (x₁, x₂).1 < (x₁, x₂).2
y₁ y₂ : Fin (2 + 1)
hy : (y₁, y₂).1 < (y₁, y₂).2
⊢ (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(x₁, x₂), hx⟩ =
      (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(y₁, y₂), hy⟩ →
    ⟨(x₁, x₂), hx⟩ = ⟨(y₁, y₂), hy⟩
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℝ
⊢ ↑(Gamma s * Gamma (s + 1 / 2)) = ↑(Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π)

Tactic:
simpa only [← Gamma_ofReal, ofReal_cpow zero_le_two, ofReal_mul, ofReal_add, ofReal_div,
    ofReal_sub] using! Complex.Gamma_mul_Gamma_add_half ↑s

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

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
e : R
h : HasSum (fun n ↦ (expSeries 𝕜 R n) fun x_1 ↦ x.fst) e
⊢ HasSum (fun n ↦ ((expSeries 𝕜 (tsze R M) (n + 1)) fun x_1 ↦ x).snd)
    (e • x.snd - ∑ i ∈ Finset.range 1, ((expSeries 𝕜 (tsze R M) i) fun x_1 ↦ x).snd)

Tactic:
simp_rw [snd_expSeries_of_smul_comm _ _ hx]

Goal state after:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
e : R
h : HasSum (fun n ↦ (expSeries 𝕜 R n) fun x_1 ↦ x.fst) e
⊢ HasSum (fun n ↦ ((expSeries 𝕜 R n) fun x_1 ↦ x.fst) • x.snd)
    (e • x.snd - ∑ i ∈ Finset.range 1, ((expSeries 𝕜 (tsze R M) i) fun x_1 ↦ x).snd)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_1
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
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
x✝ : Simplex.Equilateral t
r : ℝ
hr : ∀ (i j : Fin (2 + 1)), i ≠ j → dist (t.points i) (t.points j) = r
⊢ dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)

Tactic:
simp [hr _ _ h₁₂, hr _ _ h₁₃, hr _ _ h₂₃]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_2.inr.inl
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
t : Triangle R P
i₃ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₂₃ : i ≠ i₃
h₁₃ : j ≠ i₃
h₁₂ : j ≠ i
h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃)
h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i)

Tactic:
exact dist_comm _ _

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

Goal state before:
pp: q : ℍ
hq : q.re = 0
n : ℕ
⊢ ((expSeries ℝ ℍ (2 * n + 1)) fun x ↦ q) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Tactic:
by
  rw [expSeries_apply_eq]
  obtain rfl | hq0 := eq_or_ne q 0
  · simp
  have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq
  have hqn := norm_ne_zero_iff.mpr hq0
  let k : ℝ := ↑(2 * n + 1)!
  calc
    k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • ((-normSq q) ^ n * q) := by rw [pow_succ, pow_mul, hq2]
    _ = k⁻¹ • ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) • q := ?_
    _ = ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q := ?_
  · congr 1
    rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq, ← coe_mul_eq_smul]
    norm_cast
  · rw [smul_smul]
    congr 1
    simp_rw [pow_succ, mul_div_assoc, div_div_cancel_left' hqn]
    ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: x : ℝ
⊢ ∑' (n : ℕ), x ^ (2 * n) / ↑(2 * n)! ≤ NormedSpace.exp (x ^ 2 / 2)

Tactic:
exp_eq_tsum ℝ

Goal state after:
x : ℝ
⊢ ∑' (n : ℕ), x ^ (2 * n) / ↑(2 * n)! ≤ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x ^ 2 / 2)
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
hq : q.re = 0
⊢ exp q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q

Tactic:
exp_eq_tsum ℝ

Goal state after:
q : ℍ
hq : q.re = 0
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q
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
H : ‖φ x z‖ ≠ 0
w : ℝ × ℝ
⊢ ‖φ x w‖ = ‖φ x z‖

Tactic:
set M : ℝ := ‖φ x z‖ with hM
  have hM₀ : 0 < M := by positivity
  -- we use the key result `norm_eq_of_isMinOn_of_forall_le`
  refine norm_eq_of_isMinOn_of_forall_le hM₀ hM.symm h (continuous_φ x) (fun {w} u hw n hn ↦ ?_) w
  -- show `‖φ x u‖ ≤ M * (1 + (‖φ x u - φ x w‖ / M) ^ n)`
  have HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1) := by
    simp only [field, div_pow, ← pow_succ', Nat.sub_add_cancel hn]
  rw [HH, le_div_iff₀ (by positivity)]; clear HH
  -- show `‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n`
  let q (y : ℝ × ℝ) : ℝ[X] := X ^ 2 - C y.1 * X + C y.2
  have hq (y : ℝ × ℝ) : IsMonicOfDegree (q y) 2 := isMonicOfDegree_sub_add_two ..
  have hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2 := by simp only [q]; ring
  have hdvd : q u ∣ q w ^ n - (q w - q u) ^ n := by
    nth_rewrite 1 [← sub_sub_self (q w) (q u)]
    exact sub_dvd_pow_sub_pow ..
  have H' : ((q w - q u) ^ n).natDegree < 2 * n := by rw [hsub]; compute_degree; grind
  -- write `q w ^ n = p * q u + (q w - q u) ^ n` with a monic polynomial `p` of deg. `2 * (n - 1)`,
  -- where `aeval x (q u) = φ x u` (*).
  obtain ⟨p, hp, hrel⟩ := ((hq w).pow n).of_dvd_sub (by grind) (hq u) H' hdvd; clear H' hdvd hsub
  rw [show 2 * n - 2 = 2 * (n - 1) by grind] at hp
  -- use that `‖aeval p x‖ ≥ M ^ (n - 1)`.
  grw [le_aeval_of_isMonicOfDegree hM₀.le (isMinOn_univ_iff.mp h) hp]
  -- from (*) above, deduce
  -- `‖φ x u‖ * ‖(aeval x) p‖ = ‖(aeval x) (q w ^ n) - (aeval x) ((q w - q u) ^ n)‖`
  -- and use that.
  rw [← sub_eq_iff_eq_add, eq_comm, mul_comm] at hrel
  apply_fun (‖aeval x ·‖) at hrel
  rw [map_mul, norm_mul, map_sub, aeval_eq_φ x u] at hrel
  rw [hrel, norm_sub_rev (φ ..)]
  exact (norm_sub_le ..).trans <| by simp [q, aeval_eq_φ, hw]

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
H : φ x z ≠ 0
⊢ False

Tactic:
set M := ‖φ x z‖

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
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
⊢ False
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
n : ℕ
hn : 1 ≤ n
⊢ f (x ^ n) = f x ^ n

Tactic:
cases n

Goal state after:
case zero
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
hn : 1 ≤ 0
⊢ f (x ^ 0) = f x ^ 0

case succ
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
n✝ : ℕ
hn : 1 ≤ n✝ + 1
⊢ f (x ^ (n✝ + 1)) = f x ^ (n✝ + 1)
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
inst✝ : NormedRing R
x : R
hx : ‖x‖ = 0
⊢ x = 0

Tactic:
by rw [← norm_eq_zero]; exact hx

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

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
inst✝ : NormedField R
x : R
hx : ‖x‖ = 0
⊢ x = 0

Tactic:
by rw [← norm_eq_zero]; exact hx

Goal state after: