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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
⊢ ‖(LinearMap.rTensor G ↑f) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp
      ((span_tmul_eq_top 𝕜 E G) ▸ Submodule.mem_top (x := x))

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
⊢ ‖(LinearMap.rTensor G ↑f) x‖ ≤ ‖f‖ * ‖x‖
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : EMetricSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ μHE[finrank ℝ E].IsAddHaarMeasure

Tactic:
rw [euclideanHausdorffMeasure_def, ENNReal.smul_def]
  exact IsAddHaarMeasure.smul _
    (by simpa using addHaarScalarFactor_volume_hausdorffMeasure_ne_zero (Module.finrank ℝ E))
    (by simp)

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

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
s : Set X
hs : ediam s ≤ r
⊢ ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ r

Tactic:
ediam_closure

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
s : Set X
hs : ediam s ≤ r
⊢ ediam s ≤ r
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case neg
𝕜 : 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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U ≠ finrank 𝕜 ↥f.range
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

Tactic:
symm
    rw [normDet_eq_zero_iff_rank_range_ne.mpr hrank.symm]
    contrapose hrank with hdet
    have h : IsUnit ((f.toMatrix bu.toBasis bv.toBasis).det) := by
      simpa using hdet
    let f' := LinearEquiv.ofIsUnitDet h
    have hf : f.range = ⊤ := f'.range
    rw [hf]
    simpa using f'.finrank_eq

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

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
c : ℝ≥0
hc : c ≠ 0
⊢ ¬(c = 0 ∧ (d₂ - d₁)⁻¹ ≠ 0)

Tactic:
exact mt And.left hc

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
x y : X
⊢ ‖kernel H x y‖ ≤ √‖kernel H x x‖ * √‖kernel H y y‖

Tactic:
grw [kernel_apply, opNorm_comp_le]
  simp [norm_kerFun_eq_sqrt_norm_kernel]

Goal state after:
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
hI : ¬I = 0
x y : E
hI' : I * I = -1
⊢ ‖-x - y‖ = ‖x + y‖

Tactic:
rw [← neg_add', norm_neg]

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

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

pp: case mpr
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ S → x ∈ S.mulI.mulI

Tactic:
· intro h
    rw [mem_mapEquiv_iff (scalarSMulCLE H UnitI), ← SetLike.forall_smul_mem_iff] at h
    simpa [← smul_assoc, Units.smul_def] using (h (-1 : ℝ))

Goal state after:
case mpr
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ S → x ∈ S.mulI.mulI
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (S ⊔ T).mulI = S.mulI ⊔ T.mulI

Tactic:
by
  rw [mulI, ← mapEquiv_sup_eq]

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

Goal state before:
pp: case inr.refine_1
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
⊢ f '' s ⊆ f '' ((⋃ i, t i) ∩ s)

Tactic:
← hst,

Goal state after:
case inr.refine_1
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
⊢ f '' s ⊆ f '' (s ∩ s)
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
r : 𝕜
s : Set E
⊢ μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s

Tactic:
simpa [ENNReal.coe_rpow_of_nonneg, hd]
      using (lipschitzWith_smul r).hausdorffMeasure_image_le hd s

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

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
⊢ μH[↑(Fintype.card ι)] (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ≤ ∏ x, volume ((fun i ↦ Ioo ↑(a i) ↑(b i)) x)

Tactic:
calc
    μH[Fintype.card ι] (Set.pi univ fun i : ι => Ioo (a i : ℝ) (b i)) ≤
        liminf (fun n : ℕ => ∑ i : γ n, ediam (t n i) ^ ((Fintype.card ι) : ℝ)) atTop :=
      hausdorffMeasure_le_liminf_sum _ (Set.pi univ fun i => Ioo (a i : ℝ) (b i))
        (fun n : ℕ => 1 / (n : ℝ≥0∞)) A t B C
    _ ≤ liminf (fun n : ℕ => ∑ i : γ n, (1 / (n : ℝ≥0∞)) ^ Fintype.card ι) atTop := by
      refine liminf_le_liminf ?_ ?_
      · filter_upwards [B] with _ hn
        apply Finset.sum_le_sum fun i _ => _
        simp only [ENNReal.rpow_natCast]
        intro i _
        exact pow_le_pow_left' (hn i) _
      · isBoundedDefault
    _ = liminf (fun n : ℕ => ∏ i : ι, (⌈((b i : ℝ) - a i) * n⌉₊ : ℝ≥0∞) / n) atTop := by
      simp only [γ, Finset.card_univ, Nat.cast_prod, one_mul, Fintype.card_fin, Finset.sum_const,
        nsmul_eq_mul, Fintype.card_pi, div_eq_mul_inv, Finset.prod_mul_distrib, Finset.prod_const]
    _ = ∏ i : ι, volume (Ioo (a i : ℝ) (b i)) := by
      simp only [Real.volume_Ioo]
      apply Tendsto.liminf_eq
      refine ENNReal.tendsto_finsetProd_of_ne_top _ (fun i _ => ?_) fun i _ => ?_
      · apply
          Tendsto.congr' _
            ((ENNReal.continuous_ofReal.tendsto _).comp
              ((tendsto_nat_ceil_mul_div_atTop (I i)).comp tendsto_natCast_atTop_atTop))
        apply eventually_atTop.2 ⟨1, fun n hn => _⟩
        intro n hn
        simp only [ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr hn), comp_apply,
          ENNReal.ofReal_natCast]
      · simp only [ENNReal.ofReal_ne_top, Ne, not_false_iff]

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.rightAngleRotationAux₂.toLinearMap ∘ₗ (-o.rightAngleRotationAux₁) = LinearMap.id

Tactic:
ext; simp [rightAngleRotationAux₂]

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.rightAngleRotationAux₁) ∘ₗ o.rightAngleRotationAux₂.toLinearMap = LinearMap.id

Tactic:
ext; simp [rightAngleRotationAux₂]

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)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ φ (o.rightAngleRotation x) = o.rightAngleRotation (φ x)

Tactic:
convert! (o.rightAngleRotation_map φ (φ x)).symm

Goal state after:
case e'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ x = φ.symm (φ x)

case e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ o = (map (Fin 2) φ.toLinearEquiv) o
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
⊢ (o.kahler x) x = ↑‖x‖ ^ 2

Tactic:
by
  simp [kahler_apply_apply]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ↑(e_dual f) = e.dualMap ↑f
he' : ∀ (f : StrongDual 𝕜 E), ↑(e_dual.symm f) = e.symm.dualMap ↑f
⊢ ∀ (f : StrongDual 𝕜 E), Continuous ⇑(e.symm.dualMap ↑f)

Tactic:
simpa [← he'] using fun f ↦ map_continuous (e_dual.symm f)

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

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

Tactic:
sub_eq_add_neg 1 z

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

Goal state before:
pp: s✝ : ℂ
hs : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
s : ℂ
⊢ -↑n < s.re → (∀ (m : ℕ), s ≠ -↑m) → DifferentiableAt ℂ Gamma s

Tactic:
hsre

Goal state after:
s✝ : ℂ
hs : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
s : ℂ
hsre : -↑n < s.re
⊢ (∀ (m : ℕ), s ≠ -↑m) → DifferentiableAt ℂ Gamma s
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
ht : t ∈ Ioo 0 ε
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)

Tactic:
calc _ ≤ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ := by gcongr
          _ = d * t ^ (s - b - 1) := ?_

Goal state after:
case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
ht : t ∈ Ioo 0 ε
⊢ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ = d * t ^ (s - b - 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun x ↦ ↑x * g x) atTop (𝓝 t)
⊢ Tendsto (fun x ↦ ↑x * log (1 + g x)) atTop (𝓝 t)

Tactic:
by
  apply hg.congr_dist
  refine IsBigO.trans_tendsto ?_ tendsto_inv_atTop_zero.ofReal
  simp_rw [dist_comm (_ * g _), dist_eq, ← mul_sub, isBigO_norm_left]
  calc
    _ =O[atTop] fun x ↦ x * g x ^ 2 := by
      have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hg.norm.isBoundedUnder_le
        (RCLike.tendsto_ofReal_atTop_cobounded ℂ)
      exact (isBigO_refl _ _).mul (log_sub_self_isBigO.comp_tendsto hg0)
    _ =ᶠ[atTop] fun x ↦ (x * g x) ^ 2 * x⁻¹ := by
      filter_upwards [eventually_ne_atTop 0] with x hx0
      rw [ofReal_inv, eq_mul_inv_iff_mul_eq₀ (mod_cast hx0)]
      ring
    _ =O[atTop] _ := by
      simpa using isBigO_const_of_tendsto hg (one_ne_zero (α := ℂ))
        |>.pow 2 |>.mul (isBigO_refl _ _)

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

Goal state before:
pp: g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
x : ℝ
hg1 : -1 ≤ g x
⊢ ↑x * Complex.log (1 + ↑(g x)) = ↑x * ↑(log (1 + g x))

Tactic:
Complex.ofReal_log (by linarith),

Goal state after:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
x : ℝ
hg1 : -1 ≤ g x
⊢ ↑x * Complex.log (1 + ↑(g x)) = ↑x * Complex.log ↑(1 + g x)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
⊢ u.betaIntegral 1 = 1 / u

Tactic:
simp_rw [betaIntegral, sub_self, cpow_zero, mul_one]
  rw [integral_cpow (Or.inl _)]
  · rw [ofReal_zero, ofReal_one, one_cpow, zero_cpow, sub_zero, sub_add_cancel]
    rw [sub_add_cancel]
    contrapose! hu; rw [hu, zero_re]
  · rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]

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

Goal state before:
pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) * u = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u ≠ 0

Tactic:
contrapose! hu; rw [hu, zero_re]

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
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P → Prop
⊢ (∀ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (x : V) in map Prod.snd (atTop ×ˢ 𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P x, p y

Tactic:
eventually_map

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
v : V
p : P → Prop
⊢ (∀ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P a.2, p y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: z : ℂ
n : ℕ
hn : n ≠ 0
⊢ z.GammaSeq n * (1 - z).GammaSeq n = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))

Tactic:
have aux : ∀ a b c d : ℂ, a * b * (c * d) = a * c * (b * d) := by intros; ring

Goal state after:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ z.GammaSeq n * (1 - z).GammaSeq n = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
rcases h₁₂.lt_or_gt with h₁₂lt | h₂₁lt

Goal state after:
case 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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

case inr
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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_2
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹

Tactic:
rw [mul_inv, inv_inv, inv_inv]

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: a : ℍ
⊢ normSq a = ‖a‖ * ‖a‖

Tactic:
rw [← inner_self, real_inner_self_eq_norm_mul_norm]

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: a : ℍ
⊢ ‖star a‖ = ‖a‖

Tactic:
simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]

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

Goal state before:
pp: case inr.calc_1
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • ((-↑(normSq q)) ^ n * q) = k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q

Tactic:
congr 1
    rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq, ← coe_mul_eq_smul]
    norm_cast

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < p 1
⊢ p 1 ≤ p 1 * p 1

Tactic:
simpa only [one_mul] using map_mul_le_mul p (1 : R) _

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)) < ε
⊢ ∃ g, g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖(map (algebraMap K L) g).coeff n - f.coeff n‖ < ε

Tactic:
have hdeg : (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i).natDegree
      = f.natDegree := by
    calc
      _ = (C (1 : K) * X ^ f.natDegree).natDegree := by
        apply Polynomial.natDegree_add_eq_left_of_natDegree_lt
        simp only [map_one, one_mul, natDegree_pow, natDegree_X, mul_one]
        rw [← Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)]
        apply Polynomial.natDegree_sum_le_of_forall_le
        refine fun i hi ↦ (Polynomial.natDegree_C_mul_X_pow_le _ _).trans ?_
        simpa [Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)] using hi
      _ = f.natDegree := by
        simp

Goal state after:
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‖ < ε
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case pos
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
x : R
hx : f x = 0
⊢ f x✝ * (f x / f x) ≤ f x✝

Tactic:
rw [hx, div_zero, mul_zero]

Goal state after:
case pos
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
x : R
hx : f x = 0
⊢ 0 ≤ f x✝
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 * f y / f y

Tactic:
div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) 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
⊢ f (x * y) ≤ f x * f y / 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 : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
⊢ Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (1 * nα x))

Tactic:
exact ((rpow_zero C ▸ ContinuousAt.tendsto (continuousAt_const_rpow (ne_of_gt hC0))).comp
      (tendsto_const_div_atTop_nhds_zero_nat 1)).mul tendsto_const_nhds

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n m : ℕ
hmn : m < n
⊢ 0 = 0 ∧ ¬↑(n - m) = 0

Tactic:
cast_eq_zero,

Goal state after:
case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n m : ℕ
hmn : m < n
⊢ 0 = 0 ∧ ¬n - m = 0
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n m : ℕ
hmn : ¬m < n
⊢ (if m < n then ‖if m = n then 1 else 0‖ ^ (1 / (↑n - ↑m)) else 0) = 0

Tactic:
rw [if_neg hmn]

Goal state after: