mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
⊢ (↑(γ * n'))⁻¹ = (↑p')⁻¹

Tactic:
hp',

Goal state after:
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
⊢ (↑(γ * n'))⁻¹ = ↑p⁻¹ - (↑n)⁻¹
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
⊢ ((↑γ - 1) * q)⁻¹ = (↑p')⁻¹

Tactic:
hp',

Goal state after:
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
⊢ ((↑γ - 1) * q)⁻¹ = ↑p⁻¹ - (↑n)⁻¹
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E ⊗[𝕜] F
⊢ 0 ≤ RCLike.re (inner 𝕜 x x)

Tactic:
by
  /-
  Similarly to the above proof, for `x : E ⊗ F`, there exists finite submodules `E', F'` such that
  `x ∈ mapIncl E' F'`.
  And so the rest then follows from the above lemmas `inner_mapIncl_mapIncl` and `inner_self`.
  -/
  obtain ⟨E', F', iE', iF', hz⟩ := exists_finite_submodule_of_setFinite {x} (Set.finite_singleton x)
  obtain ⟨y, rfl⟩ := Set.singleton_subset_iff.mp hz
  obtain e := stdOrthonormalBasis 𝕜 E'
  obtain f := stdOrthonormalBasis 𝕜 F'
  rw [inner_mapIncl_mapIncl, inner_self y e f, RCLike.ofReal_re]
  exact Finset.sum_nonneg fun _ _ ↦ sq_nonneg _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y x✝¹ x✝ : E ⊗[𝕜] F
h1 : inner 𝕜 ((TensorProduct.comm 𝕜 E F) x✝¹) ((TensorProduct.comm 𝕜 E F) y) = inner 𝕜 x✝¹ y
h2 : inner 𝕜 ((TensorProduct.comm 𝕜 E F) x✝) ((TensorProduct.comm 𝕜 E F) y) = inner 𝕜 x✝ y
⊢ inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝¹ + x✝)) ((TensorProduct.comm 𝕜 E F) y) = inner 𝕜 (x✝¹ + x✝) y

Tactic:
by simp only [inner_add_left, map_add, h1, h2]

Goal state after:
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 x✝¹ x✝ : 𝕜 ⊗[𝕜] E
h1 : inner 𝕜 ((TensorProduct.lid 𝕜 E) x✝¹) ((TensorProduct.lid 𝕜 E) y) = inner 𝕜 x✝¹ y
h2 : inner 𝕜 ((TensorProduct.lid 𝕜 E) x✝) ((TensorProduct.lid 𝕜 E) y) = inner 𝕜 x✝ y
⊢ inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝¹ + x✝)) ((TensorProduct.lid 𝕜 E) y) = inner 𝕜 (x✝¹ + x✝) y

Tactic:
by simp only [inner_add_left, map_add, h1, h2]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
x✝¹ x✝ : E ⊗[𝕜] F ⊗[𝕜] G
h1 : inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) x✝¹) ((TensorProduct.assoc 𝕜 E F G) y) = inner 𝕜 x✝¹ y
h2 : inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) x✝) ((TensorProduct.assoc 𝕜 E F G) y) = inner 𝕜 x✝ y
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝¹ + x✝)) ((TensorProduct.assoc 𝕜 E F G) y) = inner 𝕜 (x✝¹ + x✝) y

Tactic:
by simp only [inner_add_left, map_add, h1, h2]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℕ
h : d₁ < d₂
s : Set X
⊢ ↑d₁ < ↑d₂

Tactic:
simpa using h

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

Goal state before:
pp: case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
r n : ℕ
⊢ ∑ a ∈ Finset.range n, μ (S (2 * a + 1 + r) \ S (2 * a + r)) ≤ μ (⋃ n, S n)

Tactic:
← hm.finset_iUnion_of_pairwise_separated

Goal state after:
case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
r n : ℕ
⊢ μ (⋃ i ∈ Finset.range n, S (2 * i + 1 + r) \ S (2 * i + r)) ≤ μ (⋃ n, S n)

case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
r n : ℕ
⊢ ∀ i ∈ Finset.range n,
    ∀ j ∈ Finset.range n, i ≠ j → AreSeparated (S (2 * i + 1 + r) \ S (2 * i + r)) (S (2 * j + 1 + r) \ S (2 * j + r))
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
tfae_1_iff_2 : f.normDet = 0 ↔ f.ker ≠ ⊥
tfae_1_iff_3 : f.normDet = 0 ↔ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U
tfae_3_iff_4 : finrank 𝕜 ↥f.range ≠ finrank 𝕜 U ↔ finrank 𝕜 ↥f.range < finrank 𝕜 U
h : ¬finrank 𝕜 ↥f.range = finrank 𝕜 U ↔ ¬Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
⊢ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U ↔ IsEmpty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)

Tactic:
simpa using h

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
x : X
r : ℕ → ℝ≥0∞ := fun x ↦ 0
t : ℕ → Unit → Set X := fun x_1 x_2 ↦ {x}
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : Unit), ediam (t n i) ≤ r n

Tactic:
simp only [t, r, imp_true_iff, ediam_singleton, eventually_atTop,
        nonpos_iff_eq_zero, exists_const]

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
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
h : K.IsHermitian
f : X →₀ V →L[𝕜] V
⊢ (f.sum fun i m ↦ f.sum fun i_1 m_1 ↦ star m_1 * (K i_1 i * m)) =
    f.sum fun i xi ↦ f.sum fun j xj ↦ star xi * (K i j * xj)

Tactic:
rw [Finsupp.sum_comm]

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
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
x✝ : Nontrivial V
v : V
hv : v ≠ 0
h : ∀ (x : X →₀ V →L[𝕜] V) (x_1 : V), 0 ≤ RCLike.re (x.sum fun i a ↦ x.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 x_1), a x_1⟫_𝕜)
ff : X × V →₀ 𝕜
⊢ 0 ≤ RCLike.re (ff.sum fun xv z ↦ ff.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)

Tactic:
rw [Finsupp.sum_comm]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
x✝ : Nontrivial V
v : V
hv : v ≠ 0
h : ∀ (x : X →₀ V →L[𝕜] V) (x_1 : V), 0 ≤ RCLike.re (x.sum fun i a ↦ x.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 x_1), a x_1⟫_𝕜)
ff : X × V →₀ 𝕜
⊢ 0 ≤ RCLike.re (ff.sum fun x' v' ↦ ff.sum fun x v ↦ (starRingEnd 𝕜) v * v' * ⟪(K x'.1 x.1) x.2, x'.2⟫_𝕜)
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
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
x✝ : Nontrivial V
v✝ : V
hv : v✝ ≠ 0
tfae_1_to_2 :
  (∀ (x : X →₀ V →L[𝕜] V) (x_1 : V),
      0 ≤ RCLike.re (x.sum fun i a ↦ x.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 x_1), a x_1⟫_𝕜)) →
    ∀ (f : X × V →₀ 𝕜),
      0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)
tfae_2_to_3 :
  (∀ (f : X × V →₀ 𝕜),
      0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)) →
    ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun x w ↦ vv.sum fun x' w' ↦ ⟪(K x' x) w, w'⟫_𝕜)
h : ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun x w ↦ vv.sum fun x' w' ↦ ⟪(K x' x) w, w'⟫_𝕜)
ff : X →₀ V →L[𝕜] V
v : V
⊢ 0 ≤ RCLike.re (ff.sum fun i a ↦ ff.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 v), a v⟫_𝕜)

Tactic:
rw [Finsupp.sum_comm]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
x✝ : Nontrivial V
v✝ : V
hv : v✝ ≠ 0
tfae_1_to_2 :
  (∀ (x : X →₀ V →L[𝕜] V) (x_1 : V),
      0 ≤ RCLike.re (x.sum fun i a ↦ x.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 x_1), a x_1⟫_𝕜)) →
    ∀ (f : X × V →₀ 𝕜),
      0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)
tfae_2_to_3 :
  (∀ (f : X × V →₀ 𝕜),
      0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)) →
    ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun x w ↦ vv.sum fun x' w' ↦ ⟪(K x' x) w, w'⟫_𝕜)
h : ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun x w ↦ vv.sum fun x' w' ↦ ⟪(K x' x) w, w'⟫_𝕜)
ff : X →₀ V →L[𝕜] V
v : V
⊢ 0 ≤ RCLike.re (ff.sum fun x' v' ↦ ff.sum fun x v_1 ↦ ⟪(K x x') (v' v), v_1 v⟫_𝕜)
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 g : H₀ K
⊢ (starRingEnd 𝕜)
      (Finsupp.sum g fun x z ↦
        match x with
        | (y, u) =>
          Finsupp.sum f fun x w ↦
            match x with
            | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜) =
    Finsupp.sum f fun x z ↦
      match x with
      | (y, u) =>
        Finsupp.sum g fun x w ↦
          match x with
          | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜

Tactic:
rw [Finsupp.sum_comm]

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
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
f g : H₀ K
⊢ (starRingEnd 𝕜)
      (Finsupp.sum f fun x' v' ↦
        Finsupp.sum g fun x v ↦
          match x' with
          | (x_1, v_1) => star v * v' * ⟪(K x_1 x.1) x.2, v_1⟫_𝕜) =
    Finsupp.sum f fun x z ↦
      match x with
      | (y, u) =>
        Finsupp.sum g fun x w ↦
          match x with
          | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜
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
x : X
v : V
⊢ ‖(K x x) v‖ * ‖v‖ ≤ ‖K x x‖ * ‖v‖ * ‖v‖

Tactic:
simp [mul_le_mul_of_nonneg_right, le_opNorm]

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
⊢ liminf (fun n ↦ ∏ i, ↑⌈(↑(b i) - ↑(a i)) * ↑n⌉₊ / ↑n) atTop = ∏ i, volume (Ioo ↑(a i) ↑(b i))

Tactic:
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.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
hs : MeasurableSet s
⊢ μH[d] (⇑(AffineMap.homothety x c) ⁻¹' s) = (‖c‖₊⁻¹ ^ d • μH[d]) s

Tactic:
hausdorffMeasure_homothety_preimage hd x hc s,

Goal state after:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
hs : MeasurableSet s
⊢ ‖c‖₊⁻¹ ^ d • μH[d] s = (‖c‖₊⁻¹ ^ d • μH[d]) s
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case «0».«1»
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
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ ⟪![x, y] ((fun i ↦ i) ⟨0, ⋯⟩), ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩)⟫ = 0

Tactic:
simpa using h

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

Goal state before:
pp: case refine_1.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 = ‖o.rightAngleRotationAux₁ x‖
⊢ ‖o.rightAngleRotationAux₁ x‖ ≤ ‖x‖

Tactic:
rw [← h]
          positivity

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
⊢ Pairwise fun i j ↦ ⟪![x, o.rightAngleRotation x] i, ![x, o.rightAngleRotation x] j⟫ = 0

Tactic:
intro i j hij
        fin_cases i <;> fin_cases j <;> simp_all

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)
a x y : E
⊢ (o.kahler x) a * (o.kahler a) y = ↑(‖a‖ ^ 2) * (o.kahler x) y

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
⊢ ↑(‖a‖ ^ 2) * (o.kahler x) y = ↑‖a‖ ^ 2 * (o.kahler x) y

Tactic:
· apply Complex.ext
    · simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re,
        Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
      rw [real_inner_comm a x, o.areaForm_swap x a]
      linear_combination o.inner_mul_inner_add_areaForm_mul_areaForm a x y
    · simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re,
        Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
      rw [real_inner_comm a x, o.areaForm_swap x a]
      linear_combination o.inner_mul_areaForm_sub a x y

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

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0

Tactic:
simpa using h

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

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ y = 0

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℂ 𝕜 E
c : 𝕜
⊢ mellin (fun t ↦ c • f t) s = c • mellin f s

Tactic:
by
  simp only [mellin, smul_comm, integral_smul]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this : EqOn (fun t ↦ ↑t ^ (s - 1) • f (a * t)) (fun t ↦ ↑a ^ (1 - s) • (fun u ↦ ↑u ^ (s - 1) • f u) (a * t)) (Ioi 0)
⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f (a * t) = ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t

Tactic:
setIntegral_congr_fun measurableSet_Ioi this,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this : EqOn (fun t ↦ ↑t ^ (s - 1) • f (a * t)) (fun t ↦ ↑a ^ (1 - s) • (fun u ↦ ↑u ^ (s - 1) • f u) (a * t)) (Ioi 0)
⊢ ∫ (x : ℝ) in Ioi 0, ↑a ^ (1 - s) • (fun u ↦ ↑u ^ (s - 1) • f u) (a * x) ∂volume =
    ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 = ‖1‖

Tactic:
exact norm_one.symm

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case hbc
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ ‖f t‖ ≤ d * ‖t ^ (-a)‖

Tactic:
exact he t ((le_max_left e 1).trans_lt ht).le

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2
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 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ HasFiniteIntegral (fun t ↦ t ^ (s - 1) * f t) (volume.restrict (Ioo 0 ε))

Tactic:
apply HasFiniteIntegral.mono' (g := fun t => d * t ^ (s - b - 1))
    · refine (Integrable.hasFiniteIntegral ?_).const_mul _
      rw [← IntegrableOn, ← integrableOn_Ioc_iff_integrableOn_Ioo, ←
        intervalIntegrable_iff_integrableOn_Ioc_of_le hε.le]
      exact intervalIntegral.intervalIntegrable_rpow' (by linarith)
    · refine (ae_restrict_iff' measurableSet_Ioo).mpr (Eventually.of_forall fun t ht => ?_)
      rw [mul_comm, norm_mul]
      specialize hε' _ ht.1
      · rw [dist_eq_norm, sub_zero, norm_of_nonneg ht.1.le]
        exact ht.2
      · calc _ ≤ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ := by gcongr
          _ = d * t ^ (s - b - 1) := ?_
        simp_rw [norm_of_nonneg (rpow_nonneg ht.1.le _), mul_assoc]
        rw [← rpow_add ht.1]
        congr 2
        abel

Goal state after: