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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E ⊗[𝕜] 𝕜
⊢ inner 𝕜 ((TensorProduct.rid 𝕜 E) x) ((TensorProduct.rid 𝕜 E) y) = inner 𝕜 x y

Tactic:
simp [← lid_comm]

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

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
⊢ borel X ≤ μ.caratheodory

Tactic:
rw [borel_eq_generateFrom_isClosed]

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
⊢ MeasurableSpace.generateFrom {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} ≤ μ.caratheodory
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_4.h
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
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ 0 ≤ (↑q)⁻¹ - 1 / ↑p'

Tactic:
one_div

Goal state after:
case e'_4.h
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
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ 0 ≤ (↑q)⁻¹ - (↑p')⁻¹
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : dimH s < ↑d
⊢ μH[↑d] s = 0

Tactic:
rw [dimH_def] at h
  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hsd', hd'd⟩
  rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hd'd
  exact (hausdorffMeasure_zero_or_top hd'd s).resolve_right fun h₂ => hsd'.not_ge <|
    le_iSup₂ (α := ℝ≥0∞) d' h₂

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

Goal state before:
pp: 𝕜 : 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
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range := ⋯ ▸ stdOrthonormalBasis 𝕜 ↥f.range
⊢ ¬‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖ = 0

Tactic:
norm_eq_zero.not

Goal state after:
𝕜 : 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
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range := ⋯ ▸ stdOrthonormalBasis 𝕜 ↥f.range
⊢ ¬((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det = 0
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: ι : Type u_5
inst✝ : Fintype ι
⊢ dimH univ = ↑(Fintype.card ι)

Tactic:
by
  simp only [← Metric.iUnion_ball_nat_succ (0 : ι → ℝ), dimH_iUnion,
    dimH_ball_pi _ (Nat.cast_add_one_pos _), iSup_const]

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

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet

Tactic:
by_cases hf : f.ker = ⊥
  · let bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
    obtain ⟨bv⟩ := (f.normDet_ne_zero_tfae.out 1 3).mp hf
    by_cases hgf : (g ∘ₗ f).ker = ⊥
    · obtain ⟨bw⟩ := ((g ∘ₗ f).normDet_ne_zero_tfae.out 1 3).mp hgf
      let bw' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 (g.domRestrict f.range).range :=
        bw.map (LinearIsometryEquiv.ofEq _ _ (by simp [LinearMap.range_comp]))
      rw [(g ∘ₗ f).normDet_eq_norm_det_toMatrix_rangeRestrict bu bw,
        f.normDet_eq_norm_det_toMatrix_rangeRestrict bu bv,
        (g.domRestrict f.range).normDet_eq_norm_det_toMatrix_rangeRestrict bv bw']
      rw [← norm_mul, ← Matrix.det_mul, ← LinearMap.toMatrix_comp]
      rfl
    · have hg : (g.domRestrict f.range).ker ≠ ⊥ := by
        contrapose hf with hgf'
        rw [← LinearMap.ker_rangeRestrict, ← LinearMap.ker_comp_of_ker_eq_bot _ hgf']
        exact hgf
      simp [normDet_eq_zero_iff_ker_ne_bot.mpr hgf, normDet_eq_zero_iff_ker_ne_bot.mpr hg]
  · have hgf : (g ∘ₗ f).ker ≠ ⊥ := by
      contrapose hf with hbot
      simpa [hbot] using ker_le_ker_comp f g
    simp [normDet_eq_zero_iff_ker_ne_bot.mpr hf, normDet_eq_zero_iff_ker_ne_bot.mpr hgf]

Goal state after:
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
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
y : X
v : V
x : X
⊢ ((kerFun H y) v) x = (kernel H x y) v

Tactic:
by
  simp [kernel, kerFun]

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

Goal state before:
pp: case pos
U : Type u_5
V : Type u_6
inst✝⁸ : NormedAddCommGroup U
inst✝⁷ : InnerProductSpace ℝ U
inst✝⁶ : FiniteDimensional ℝ U
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MeasurableSpace U
inst✝² : BorelSpace U
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : U →ₗ[ℝ] V
s : Set U
h : f.ker = ⊥
⊢ μH[↑(finrank ℝ U)] (⇑f '' s) = ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s

Tactic:
have hrank : finrank ℝ ↥f.range = finrank ℝ U := (f.normDet_ne_zero_tfae.out 1 2).mp h

Goal state after:
case pos
U : Type u_5
V : Type u_6
inst✝⁸ : NormedAddCommGroup U
inst✝⁷ : InnerProductSpace ℝ U
inst✝⁶ : FiniteDimensional ℝ U
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MeasurableSpace U
inst✝² : BorelSpace U
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : U →ₗ[ℝ] V
s : Set U
h : f.ker = ⊥
hrank : finrank ℝ ↥f.range = finrank ℝ U
⊢ μH[↑(finrank ℝ U)] (⇑f '' s) = ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ { val := UnitI.inv, inv := ↑UnitI, val_inv := ⋯, inv_val := ⋯ } • x ∈ Sᗮ ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0

Tactic:
Units.smul_mk_apply

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ UnitI.inv • x ∈ Sᗮ ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c : ℝ
hc : c < 0
⊢ IsUnit (f + -(algebraMap ℝ (H →L[𝕜] H)) c)

Tactic:
← map_neg

Goal state after:
𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c : ℝ
hc : c < 0
⊢ IsUnit (f + (algebraMap ℝ (H →L[𝕜] H)) (-c))
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
e : X ≃ᵢ Y
d : ℝ
⊢ μH[d].restrict univ = μH[d]

Tactic:
restrict_univ

Goal state after:
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
e : X ≃ᵢ Y
d : ℝ
⊢ μH[d] = μH[d]
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case refine_2
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 : Nontrivial ↥Kᗮ
⊢ ‖x‖ ≤ ‖o.rightAngleRotationAux₁ x‖

Tactic:
obtain ⟨w, hw₀⟩ : ∃ w : Kᗮ, w ≠ 0 := exists_ne 0

Goal state after:
case refine_2
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 : Nontrivial ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
⊢ ‖x‖ ≤ ‖o.rightAngleRotationAux₁ x‖
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin f (s / -1) = mellin f (-s)

Tactic:
div_neg,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin f (-(s / 1)) = mellin f (-s)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ((-z) ^ n - 1) / -(z + 1)

Tactic:
div_neg,

Goal state after:
case e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - -(((-z) ^ n - 1) / (z + 1))
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
have help : IntervalIntegrable (fun t : ℝ ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1 :=
    IntervalIntegrable.mul_const (Continuous.intervalIntegrable (by fun_prop) 0 1) (1 - ‖z‖)⁻¹

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: n : ℕ
⊢ ¬ContinuousAt Gamma (-↑n)

Tactic:
by
  induction n
  case zero =>
    rw [Nat.cast_zero, neg_zero]
    exact not_continuousAt_Gamma_zero
  case succ n ih =>
    contrapose ih
    rw [Nat.cast_add, Nat.cast_one] at ih
    suffices ContinuousAt (fun s ↦ Gamma (s - 1 + 1)) (-n) by simpa using this
    suffices ContinuousAt (fun s ↦ Gamma (s + 1)) (-n - 1) from
      this.comp' (f := fun s ↦ s - 1) (continuous_sub_right 1).continuousAt
    rw [← neg_add']
    have h0 : -(n + 1) ≠ (0 : ℂ) := neg_ne_zero.mpr n.cast_add_one_ne_zero
    exact ((continuousAt_id.mul ih).continuousWithinAt.congr Gamma_add_one
      (Gamma_add_one (-(n + 1)) h0)).continuousAt (compl_singleton_mem_nhds h0)

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

Goal state before:
pp: z : ℂ
n : ℕ
hz : z ≠ 0
⊢ (1 - z ^ 2 / (↑n + 1) ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n + 2) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)

Tactic:
by
  convert! integral_cos_mul_cos_pow (by lia : 2 ≤ 2 * n + 2) hz using 3
  · simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_two]
    nth_rw 2 [← mul_one (2 : ℂ)]
    rw [← mul_add, mul_pow, ← div_div]
    ring
  · push_cast; ring
  · push_cast; ring

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

Goal state before:
pp: case e_a
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
⊢ ↑x ^ (s - 1) = ↑a ^ (s - 1) * ↑(x / a) ^ (s - 1)

pp: case e_a
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
⊢ (↑a - ↑x) ^ (t - 1) = ↑a ^ (t - 1) * (1 - ↑(x / a)) ^ (t - 1)

Tactic:
· rw [← mul_cpow_ofReal_nonneg ha.le (div_pos hx.1 ha).le, ofReal_div, mul_div_cancel₀ _ ha']

Goal state after:
case e_a
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
⊢ (↑a - ↑x) ^ (t - 1) = ↑a ^ (t - 1) * (1 - ↑(x / a)) ^ (t - 1)
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
x y : PE
e : PE ≃ᵢ PE :=
  ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans
    (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)

Tactic:
have hx : e x = x := by simp [e]

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 y : PE
e : PE ≃ᵢ PE :=
  ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans
    (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv
hx : e x = x
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

Tactic:
refine tendsto_nhds_unique ((GammaSeq_tendsto_Gamma z).mul (GammaSeq_tendsto_Gamma <| 1 - z)) ?_

Goal state after:
case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ Tendsto (fun x ↦ z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 (↑π / sin (↑π * z)))
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).Regular ↔ s.Regular

Tactic:
refine ⟨fun h σ ↦ ?_, fun h σ ↦ ?_⟩
  · rcases h ((e.symm.trans σ).trans e) with ⟨x, hx⟩
    refine ⟨x, ?_⟩
    ext i
    simpa using congrFun hx (e i)
  · rcases h ((e.trans σ).trans e.symm) with ⟨x, hx⟩
    refine ⟨x, ?_⟩
    ext i
    simpa using congrFun hx (e.symm i)

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

Goal state before:
pp: case neg
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 i) (s.points j) = dist (s.points 0) (s.points 1)

Tactic:
rcases hr ((Equiv.swap 0 i).trans (Equiv.swap 1 j)) with ⟨x, hx⟩
    nth_rw 2 [← x.dist_eq]
    simp_rw [← Function.comp_apply (f := x), ← hx]
    simp only [Equiv.coe_trans, comp_apply, Equiv.swap_apply_left]
    convert! rfl
    · exact Equiv.swap_apply_of_ne_of_ne hi hij
    · rw [Equiv.swap_apply_of_ne_of_ne (by simp [hn]) (Ne.symm hi)]
      simp

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: α : Type u_1
L : SummationFilter α
f : α → ℝ
r : ℝ
h : HasSum (fun a ↦ ↑(f a)) (↑r) L
⊢ HasSum f r L

Tactic:
by
    simpa only using!
    h.map (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _ _) continuous_re

Goal state after:
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 * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I =
    ((-z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)! - (z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)!) * I / 2 +
      ((-z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)! - (z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)!) * I / 2

Tactic:
simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ, pow_mul, mul_pow, neg_sq, sub_self,
    zero_mul, zero_div, zero_add, neg_mul, mul_neg, neg_div, ← neg_add', ← two_mul,
    neg_mul, neg_div, mul_assoc, mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0), Complex.div_I]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Ultra

Goal state before:
pp: case succ
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
n : ℕ
hn : ‖↑n‖₊ ≤ 1
⊢ ‖↑(n + 1)‖₊ ≤ 1

Tactic:
simpa only [Nat.cast_add, Nat.cast_one, hn, max_eq_right] using
    nnnorm_add_one_le_max_nnnorm_one (n : R)

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

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

Tactic:
rw [exp_eq]

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ∑ k ∈ Finset.range (Finset.range (m + 1)).card, ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m)

Tactic:
Finset.card_range

Goal state after:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m)
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f✝ : AlgebraNorm R S
f f' : MulAlgebraNorm R S
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) f'
⊢ f = f'

Tactic:
simp only [AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe, DFunLike.coe_fn_eq] at h

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f✝ : AlgebraNorm R S
f f' : MulAlgebraNorm R S
h : f.toMulRingSeminorm = f'.toMulRingSeminorm
⊢ f = f'
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
⊢ liminf (u + v) f ≤ limsup u f + liminf v f

Tactic:
have h := isCoboundedUnder_ge_add h₂ h₄
  have h' := isBoundedUnder_ge_add h₁ h₃
  refine le_add_of_forall_lt fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun _ c_ab ↦ ?_
  refine ((frequently_lt_of_liminf_lt h₄ b_v).and_eventually
    (eventually_lt_of_limsup_lt a_u h₂)).mono fun _ ab_x ↦ ?_
  exact (add_lt_add ab_x.2 ab_x.1).trans c_ab

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

Goal state before:
pp: 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
ixy : ι
left✝ : ixy ∈ univ
hixy_def : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖) = ‖(B.repr (x * y)) ixy‖
⊢ ‖(∑ x_1, (B.repr x) x_1 • B.repr (∑ i, B x_1 * (B.repr y) i • B i)) ixy‖ ≤
    B.norm (B c.1 * B c.2) * B.norm x * B.norm y

Tactic:
map_finsetSum,

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
ixy : ι
left✝ : ixy ∈ univ
hixy_def : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖) = ‖(B.repr (x * y)) ixy‖
⊢ ‖(∑ x_1, (B.repr x) x_1 • ∑ i, B.repr (B x_1 * (B.repr y) i • B i)) ixy‖ ≤
    B.norm (B c.1 * B c.2) * B.norm x * B.norm y
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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
⊢ seminormFromBounded' f x = f x

Tactic:
by
  simp_rw [seminormFromBounded', hx, ← mul_div_assoc']
  apply le_antisymm
  · refine ciSup_le (fun x ↦ ?_)
    by_cases hx : f x = 0
    · rw [hx, div_zero, mul_zero]; exact f_nonneg _
    · rw [div_self hx, mul_one]
  · by_cases! f_ne_zero : f ≠ 0
    · conv_lhs => rw [← mul_one (f x)]
      rw [← div_self (map_one_ne_zero f_ne_zero f_nonneg f_mul)]
      have h_bdd : BddAbove (Set.range fun y ↦ f x * (f y / f y)) := by
        use f x
        rintro r ⟨y, rfl⟩
        by_cases hy0 : f y = 0
        · simp only [hy0, div_zero, mul_zero]; exact f_nonneg _
        · simp only [div_self hy0, mul_one, le_refl]
      exact le_ciSup h_bdd (1 : R)
    · simp_rw [f_ne_zero, Pi.zero_apply, zero_div, zero_mul, ciSup_const]; rfl

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
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
heq : L + ε = L + ε / 2 + ε / 2
⊢ (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - (L + ε / 2) * 1 ≤ ε / 2

Tactic:
rw [mul_assoc, ← mul_sub, mul_comm, ← le_div_iff₀ hL0', div_div]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
heq : L + ε = L + ε / 2 + ε / 2
⊢ (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))