mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
⊢ mkMetric' m = ⨆ n, pre m (↑n)⁻¹

Tactic:
by
  ext1 s
  rw [iSup_apply]
  refine tendsto_nhds_unique (mkMetric'.tendsto_pre_nat m s)
    (tendsto_atTop_iSup fun k l hkl => mkMetric'.mono_pre_nat m hkl s)

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
m : ℝ≥0∞ → ℝ≥0∞
⊢ ⇑(mkMetric m) = ⇑(Measure.mkMetric m)

Tactic:
rw [← Measure.mkMetric_toOuterMeasure, Measure.coe_toOuterMeasure]

Goal state after:
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
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ∩ sᶜ = ∅
⊢ ↑(finrank ℝ E) ≤ dimH s

Tactic:
← sdiff_eq,

Goal state after:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t \ s = ∅
⊢ ↑(finrank ℝ E) ≤ dimH s
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : ¬I = 0
hI' : I * I = -1
I_smul : ∀ (v : E), ‖I • v‖ = ‖v‖
h₁ : ‖I • y - x‖ = ‖I • x + y‖
⊢ ‖I • y + x‖ = ‖I • x - y‖

Tactic:
convert (I_smul ((I : 𝕜) • y + x)).symm

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : ¬I = 0
hI' : I * I = -1
I_smul : ∀ (v : E), ‖I • v‖ = ‖v‖
h₁ : ‖I • y - x‖ = ‖I • x + y‖
⊢ I • x - y = I • (I • y + x)
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 : ℕ
⊢ ediam (u j) ≤ ε

Tactic:
ediam_iUnion_mem_option

Goal state after:
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) ≤ ε
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 ^ (d₂ - d₁)⁻¹) = 0

Tactic:
ENNReal.coe_eq_zero,

Goal state after:
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 ^ (d₂ - d₁)⁻¹ = 0
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 : X
⊢ ‖kernel H x x‖ = ‖kerFun H x‖ * ‖kerFun H x‖

Tactic:
← ContinuousLinearMap.norm_adjoint_comp_self,

Goal state after:
𝕜 : 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 : X
⊢ ‖kernel H x x‖ = ‖adjoint (kerFun H x) ∘SL kerFun H x‖
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 : X
⊢ ‖kerFun H x‖ = √‖kernel H x x‖

Tactic:
rw [norm_kernel_eq_norm_kerFun_sq, Real.sqrt_sq (norm_nonneg _)]

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‖ ^ 2 ≤ ‖kernel H x x‖ * ‖kernel H y y‖

Tactic:
grw [norm_kernel_le]; simp [mul_pow]

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 = ⊥
hrank : finrank ℝ ↥f.range = finrank ℝ U
bv : OrthonormalBasis (Fin (finrank ℝ U)) ℝ ↥f.range
⊢ μH[↑(finrank ℝ U)] (⇑f '' s) = ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s

Tactic:
let g : U ≃ₗᵢ[ℝ] f.range := (stdOrthonormalBasis ℝ U).equiv bv (Equiv.refl _)

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
bv : OrthonormalBasis (Fin (finrank ℝ U)) ℝ ↥f.range
g : U ≃ₗᵢ[ℝ] ↥f.range := (stdOrthonormalBasis ℝ U).equiv bv (Equiv.refl (Fin (finrank ℝ U)))
⊢ μH[↑(finrank ℝ U)] (⇑f '' s) = ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr.inl
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h✝ : d₁ ≤ d₂
s : Set X
h : d₁ < d₂
hs : μH[d₂] s = 0
⊢ μH[d₂] s ≤ μH[d₁] s

Tactic:
simp [hs]

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

Goal state before:
pp: case inr.inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h✝ : d₁ ≤ d₂
s : Set X
h : d₁ < d₂
hs : μH[d₁] s = ∞
⊢ μH[d₂] s ≤ μH[d₁] s

Tactic:
simp [hs]

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

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ (↑S.mulI.mulI).carrier ↔ x ∈ (↑S).carrier

Tactic:
simp only [Submodule.carrier_eq_coe, coe_toSubmodule, SetLike.mem_coe]

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ S.mulI.mulI ↔ x ∈ S
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case 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
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
⊢ μH[d] (f '' s) ≤ ↑0 ^ d * μH[↑r * d] s

pp: case inr
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
⊢ μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s

Tactic:
· rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
    · simp only [measure_empty, nonpos_iff_eq_zero, mul_zero, image_empty]
    have : f '' s = {f x} :=
      have : (f '' s).Subsingleton := by simpa [ediam_eq_zero_iff] using h.ediam_image_le
      (subsingleton_iff_singleton (mem_image_of_mem f hx)).1 this
    rw [this]
    rcases eq_or_lt_of_le hd with (rfl | h'd)
    · simp only [ENNReal.rpow_zero, one_mul, mul_zero]
      rw [hausdorffMeasure_zero_singleton]
      exact one_le_hausdorffMeasure_zero_of_nonempty ⟨x, hx⟩
    · have := nullSingletonClass_hausdorff Y h'd
      simp only [zero_le, measure_singleton]

Goal state after:
case inr
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
⊢ μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s
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
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
f : OfKernel K
h : (ContinuousLinearMap.pi fun x ↦ adjoint (kerFun K x)) f = 0
ff : H₀ K
⊢ ⟪↑ff, f⟫_𝕜 = 0

Tactic:
induction ff using Finsupp.induction with
    | zero =>
      have : @UniformSpace.Completion.coe' (H₀ K) PseudoMetricSpace.toUniformSpace 0 = 0 := rfl
      simp [this]
    | single_add i a =>
    simp only [UniformSpace.Completion.coe_add, inner_add_left, *, add_zero]
    rw [← UniformSpace.Completion.coe_toComplL (𝕜 := 𝕜)]
    have := (ext_iff_inner_left 𝕜).mp (congrFun h i.1) i.2
    have := by simpa [OfKernel.kerFun, adjoint_inner_right] using this
    rw [← mul_zero (conj a), ← this, ← inner_smul_left]
    refine (ext_iff_inner_right 𝕜).mp ?_ f
    simp [← UniformSpace.Completion.coe_toComplL (𝕜 := 𝕜),
      ← map_smul, -SeparationQuotient.mkCLM_apply, -UniformSpace.Completion.coe_toComplL]

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

Goal state before:
pp: ι : Type u_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
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
this : μH[↑(finrank ℝ E)] (⇑e '' K) < ∞
⊢ μH[↑(finrank ℝ E)] K < ∞

Tactic:
rw [← e.symm_image_image K]

Goal state after:
ι : Type u_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
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
this : μH[↑(finrank ℝ E)] (⇑e '' K) < ∞
⊢ μH[↑(finrank ℝ E)] (⇑e.symm '' ⇑e '' K) < ∞
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inl.inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set ℝ
this : NullSingletonClass μH[1]
hs : s.Nonempty
⊢ μH[1] ((fun r ↦ r • 0) '' s) = ‖0‖₊ • μH[1] s

Tactic:
simp [hs]

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

Goal state before:
pp: E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
⊢ Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))

Tactic:
refine AddMonoidHomClass.isometry_of_norm _ fun x => (norm_smul _ _).trans ?_

Goal state after:
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
⊢ ‖LinearMap.id x‖ * ‖‖v‖⁻¹ • v‖ = ‖x‖
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ᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, ↑w⟫ = 0
hw : ↑w ≠ 0
⊢ ‖x‖ * ‖↑w‖ ≤ ‖o.rightAngleRotationAux₁ x‖ * ‖↑w‖

Tactic:
rw [← o.abs_areaForm_of_orthogonal hw']

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
hw' : ⟪x, ↑w⟫ = 0
hw : ↑w ≠ 0
⊢ |(o.areaForm x) ↑w| ≤ ‖o.rightAngleRotationAux₁ x‖ * ‖↑w‖
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)
a x y : E
⊢ (o.kahler x) a * (o.kahler a) y = ↑(‖a‖ ^ 2) * (o.kahler x) y

Tactic:
apply Complex.ext

Goal state after:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ((o.kahler x) a * (o.kahler a) y).re = (↑(‖a‖ ^ 2) * (o.kahler x) y).re

case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ((o.kahler x) a * (o.kahler a) y).im = (↑(‖a‖ ^ 2) * (o.kahler x) y).im
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: w z : ℂ
⊢ ↑⟪w, z⟫ + (Complex.orientation.areaForm w) z • I = z * (starRingEnd ℂ) w

Tactic:
apply Complex.ext

Goal state after:
case a
w z : ℂ
⊢ (↑⟪w, z⟫ + (Complex.orientation.areaForm w) z • I).re = (z * (starRingEnd ℂ) w).re

case a
w z : ℂ
⊢ (↑⟪w, z⟫ + (Complex.orientation.areaForm w) z • I).im = (z * (starRingEnd ℂ) w).im
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ AEStronglyMeasurable (f c u) (volume.restrict (Ioi 0))

Tactic:
· refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
      refine .mul (by fun_prop) (continuousOn_of_forall_continuousAt fun x hx ↦ ?_)
      exact continuousAt_rpow_const _ _ (Or.inl (mem_Ioi.mp hx).ne')

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

Goal state before:
pp: s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x,
        ((ContinuousLinearMap.mul ℝ ℂ) (↑(rexp (-t_1)) * ↑t_1 ^ (s - 1)))
          (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    ((ContinuousLinearMap.mul ℝ ℂ) (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume))
      (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume)
⊢ Gamma s * Gamma t = Gamma (s + t) * s.betaIntegral t

Tactic:
simp_rw [ContinuousLinearMap.mul_apply'] at conv_int

Goal state after:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume
⊢ Gamma s * Gamma t = Gamma (s + t) * s.betaIntegral t
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: a s : ℂ
hs : 0 < s.re + a.re
⊢ HasMellin ((Ioc 0 1).indicator fun t ↦ ↑t ^ a) s (1 / (s + a))

Tactic:
by
  have := hasMellin_one_Ioc (by rwa [add_re] : 0 < (s + a).re)
  simp_rw [HasMellin, ← MellinConvergent.cpow_smul, ← mellin_cpow_smul, ← indicator_smul,
    smul_eq_mul, mul_one] at this
  exact this

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
h'g : ∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤
y : 𝕜
h₁y : AnalyticAt 𝕜 f y
h₂y : AnalyticAt 𝕜 g y
h₃y : f y ≠ 0
h₄y : g y ≠ 0
⊢ logDeriv (fun i ↦ f i * g i) y = logDeriv f y + logDeriv g y

Tactic:
exact logDeriv_mul y h₃y h₄y h₁y.differentiableAt h₂y.differentiableAt

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
s : Finset ι
F : ι → 𝕜 → 𝕜'
h : ∀ i ∈ s, MeromorphicOn (F i) U
h' : ∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
⊢ logDeriv (∏ i ∈ s, F i) =ᶠ[codiscreteWithin U] ∑ i ∈ s, logDeriv (F i)

Tactic:
have hA : ∀ᶠ y in codiscreteWithin U, ∀ i ∈ s, AnalyticAt 𝕜 (F i) y :=
    (eventually_all_finset s).2 fun i hi ↦ (h i hi).analyticAt_mem_codiscreteWithin
  have hN : ∀ᶠ y in codiscreteWithin U, ∀ i ∈ s, F i y ≠ 0 :=
    (eventually_all_finset s).2 fun i hi ↦ (h i hi).eventually_codiscreteWithin_apply_ne_zero
      (h' i hi)
  filter_upwards [hA, hN] with y h₁y h₂y
  rw [Finset.sum_apply, Finset.prod_fn]
  exact logDeriv_prod h₂y fun i hi ↦ (h₁y i hi).differentiableAt

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

Goal state before:
pp: case h
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ ↑n ≠ 0

Tactic:
exact Nat.cast_ne_zero.mpr hn

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ↑n ≠ 0

Tactic:
exact Nat.cast_ne_zero.mpr hn

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

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
hs : Convex k s
this : ∀ {s : Set V}, Convex k s → IsClosed[inst✝²] s → Convex k (asymptoticCone k s)
hs' : ¬IsClosed[inst✝²] s
⊢ Convex k (asymptoticCone k s)

Tactic:
rw [← asymptoticCone_closure]; exact this hs.closure isClosed_closure

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✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
⊢ (c • a • v + c • b • u) +ᵥ p ∈ s

Tactic:
smul_smul

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
⊢ ((c * a) • v + (c * b) • u) +ᵥ p ∈ s
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f.contLinear‖ * ‖g.contLinear‖ ≤ ‖f‖ * ‖g‖

Tactic:
by grw [f.norm_contLinear_le, g.norm_contLinear_le]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
p' : P
hp' : ∀ (i : Fin 3), p' ∈ line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
⊢ ∀ (i : ↑Set.univ), p' ∈ line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]

Tactic:
simpa [w] using hp'

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

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s

Tactic:
| succ n ihn =>

Goal state after:
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
⊢ (‖(WithLp.toLp 1 x).fst‖ ^ ENNReal.toReal 1 + ‖(WithLp.toLp 1 x).snd‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) =
    ‖x.fst‖ + ‖x.snd‖

Tactic:
simp only [WithLp.toLp_fst, ENNReal.toReal_one, Real.rpow_one, WithLp.toLp_snd, ne_eq,
    one_ne_zero, not_false_eq_true, div_self, fst, snd]

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

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

Tactic:
smul_smul

Goal state after:
case inr.calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ (k⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n))) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
⊢ ∃ f, IsPowMul ⇑f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean ⇑f

Tactic:
set B : Basis ι K L := Basis.extend h1

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
⊢ ∃ f, IsPowMul ⇑f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean ⇑f