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

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ ε * ϕ x * 2 ^ k ≤ ε * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'

pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ 0 < 2 ^ k

Tactic:
mul_assoc,

Goal state after:
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ ε * (ϕ x * 2 ^ k) ≤ ε * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'

X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ 0 < 2 ^ k
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b : P
v : V
⊢ ⟪a -ᵥ b, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0

Tactic:
by
  rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero]

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

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ ⟪a -ᵥ c, a -ᵥ b⟫ = dist a c ^ 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0

Tactic:
inner_vsub_vsub_left_eq_dist_sq_left_iff,

Goal state after:
V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ ⟪a -ᵥ c, c -ᵥ b⟫ = 0 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace 𝕜 F
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
x : E
hba2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← neg_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace 𝕜 F
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
x : E
hba2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι✝ : Type u_1
A : ι✝ → Type u_2
inst✝⁸ : (i : ι✝) → MeasurableSpace (A i)
μ✝ : (i : ι✝) → Measure (A i)
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
p : ℝ
ι : Type := Fin (finrank ℝ E)
⊢ ℝ≥0

Tactic:
have : finrank ℝ E = finrank ℝ (ι → ℝ) := by
    rw [finrank_fintype_fun_eq_card, Fintype.card_fin (finrank ℝ E)]

Goal state after:
ι✝ : Type u_1
A : ι✝ → Type u_2
inst✝⁸ : (i : ι✝) → MeasurableSpace (A i)
μ✝ : (i : ι✝) → Measure (A i)
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
p : ℝ
ι : Type := Fin (finrank ℝ E)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
⊢ ℝ≥0
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : E →ₗ[𝕜] F
⊢ (S ∘ₗ T ∘ₗ LinearMap.adjoint S).IsPositive

Tactic:
have := FiniteDimensional.complete 𝕜 E

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : E →ₗ[𝕜] F
this : CompleteSpace E
⊢ (S ∘ₗ T ∘ₗ LinearMap.adjoint S).IsPositive
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : Fin (Module.finrank 𝕜 E) → E := fun i ↦ ↑√(⋯.eigenvalues ⋯ i) • (⋯.eigenvectorBasis ⋯) i
x✝ : E
⊢ T x✝ =
    ∑ x,
      ((starRingEnd 𝕜) ↑√(⋯.eigenvalues ⋯ x) * ⟪(⋯.eigenvectorBasis ⋯) x, x✝⟫ * ↑√(⋯.eigenvalues ⋯ x)) •
        (⋯.eigenvectorBasis ⋯) x

Tactic:
mul_assoc,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : Fin (Module.finrank 𝕜 E) → E := fun i ↦ ↑√(⋯.eigenvalues ⋯ i) • (⋯.eigenvectorBasis ⋯) i
x✝ : E
⊢ T x✝ =
    ∑ x,
      ((starRingEnd 𝕜) ↑√(⋯.eigenvalues ⋯ x) * (⟪(⋯.eigenvectorBasis ⋯) x, x✝⟫ * ↑√(⋯.eigenvalues ⋯ x))) •
        (⋯.eigenvectorBasis ⋯) x
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hf : f.IsClosable
hfg : g ≤ f
⊢ g.IsClosable

Tactic:
by
  obtain ⟨f', hf⟩ := hf
  have : g.graph.topologicalClosure ≤ f'.graph := by
    rw [← hf]
    exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)
  use g.graph.topologicalClosure.toLinearPMap
  rw [Submodule.toLinearPMap_graph_eq]
  exact fun _ hx hx' => f'.graph_fst_eq_zero_snd (this hx) hx'

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

Goal state before:
pp: case hg_ker.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (↑f - 1).rangeᗮ
⊢ ‖↑f x‖ ≤ ‖↑1 x‖

pp: case hg_ker.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (↑f - 1).rangeᗮ
⊢ RCLike.re ⟪↑f x, ↑1 x⟫ = ‖↑1 x‖ ^ 2

Tactic:
· simpa using f.le_of_opNorm_le hf x

Goal state after:
case hg_ker.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (↑f - 1).rangeᗮ
⊢ RCLike.re ⟪↑f x, ↑1 x⟫ = ‖↑1 x‖ ^ 2
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'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
⊢ ↑C * ∫⁻ (x : E), ‖fderiv ℝ v x‖ₑ ∂μ ≤ ↑C * ↑γ * ∫⁻ (x : E), ‖u x‖ₑ ^ (↑γ - 1) * ‖fderiv ℝ u x‖ₑ ∂μ

Tactic:
mul_assoc,

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'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
⊢ ↑C * ∫⁻ (x : E), ‖fderiv ℝ v x‖ₑ ∂μ ≤ ↑C * (↑γ * ∫⁻ (x : E), ‖u x‖ₑ ^ (↑γ - 1) * ‖fderiv ℝ u x‖ₑ ∂μ)
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
⊢ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U ↔ IsEmpty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)

Tactic:
have h := (f.normDet_ne_zero_tfae.out 2 3).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
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)
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
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
h : ¬(↑f).ker = ⊥
⊢ ↑((↑f).normDet ^ 2) = (ContinuousLinearMap.adjoint f ∘SL f).det

Tactic:
trans 0

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
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := ⋯
h : ¬(↑f).ker = ⊥
⊢ ↑((↑f).normDet ^ 2) = 0

𝕜 : 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
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := ⋯
h : ¬(↑f).ker = ⊥
⊢ 0 = (ContinuousLinearMap.adjoint f ∘SL f).det
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
b : OrthonormalBasis ι 𝕜 U
h : ¬f.ker = ⊥
⊢ ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 fun x ↦ f.rangeRestrict (b x)).det

Tactic:
trans 0

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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
h : ¬f.ker = ⊥
⊢ ↑(f.normDet ^ 2) = 0

𝕜 : 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
b : OrthonormalBasis ι 𝕜 U
h : ¬f.ker = ⊥
⊢ 0 = (Matrix.gram 𝕜 fun x ↦ f.rangeRestrict (b x)).det
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
x y z : E
h1 :
  ‖x + y + z + (x - z)‖ * ‖x + y + z + (x - z)‖ + ‖x + y + z - (x - z)‖ * ‖x + y + z - (x - z)‖ =
    2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)
h2 :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ 4⁻¹ *
      (𝓚 ‖x + y + z‖ * 𝓚 ‖x + y + z‖ - 𝓚 ‖x + y - z‖ * 𝓚 ‖x + y - z‖ + I * 𝓚 ‖I • (x + y) + z‖ * 𝓚 ‖I • (x + y) + z‖ -
        I * 𝓚 ‖I • (x + y) - z‖ * 𝓚 ‖I • (x + y) - z‖) =
    4⁻¹ *
        (𝓚 ‖x + z‖ * 𝓚 ‖x + z‖ - 𝓚 ‖x - z‖ * 𝓚 ‖x - z‖ + I * 𝓚 ‖I • x + z‖ * 𝓚 ‖I • x + z‖ -
          I * 𝓚 ‖I • x - z‖ * 𝓚 ‖I • x - z‖) +
      4⁻¹ *
        (𝓚 ‖y + z‖ * 𝓚 ‖y + z‖ - 𝓚 ‖y - z‖ * 𝓚 ‖y - z‖ + I * 𝓚 ‖I • y + z‖ * 𝓚 ‖I • y + z‖ -
          I * 𝓚 ‖I • y - z‖ * 𝓚 ‖I • y - z‖)

Tactic:
have h3 := parallelogram_identity (y + z) z

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h1 :
  ‖x + y + z + (x - z)‖ * ‖x + y + z + (x - z)‖ + ‖x + y + z - (x - z)‖ * ‖x + y + z - (x - z)‖ =
    2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)
h2 :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
h3 : ‖y + z + z‖ * ‖y + z + z‖ + ‖y + z - z‖ * ‖y + z - z‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖)
⊢ 4⁻¹ *
      (𝓚 ‖x + y + z‖ * 𝓚 ‖x + y + z‖ - 𝓚 ‖x + y - z‖ * 𝓚 ‖x + y - z‖ + I * 𝓚 ‖I • (x + y) + z‖ * 𝓚 ‖I • (x + y) + z‖ -
        I * 𝓚 ‖I • (x + y) - z‖ * 𝓚 ‖I • (x + y) - z‖) =
    4⁻¹ *
        (𝓚 ‖x + z‖ * 𝓚 ‖x + z‖ - 𝓚 ‖x - z‖ * 𝓚 ‖x - z‖ + I * 𝓚 ‖I • x + z‖ * 𝓚 ‖I • x + z‖ -
          I * 𝓚 ‖I • x - z‖ * 𝓚 ‖I • x - z‖) +
      4⁻¹ *
        (𝓚 ‖y + z‖ * 𝓚 ‖y + z‖ - 𝓚 ‖y - z‖ * 𝓚 ‖y - z‖ + I * 𝓚 ‖I • y + z‖ * 𝓚 ‖I • y + z‖ -
          I * 𝓚 ‖I • y - z‖ * 𝓚 ‖I • y - z‖)
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr
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
this : 0 < ↑c ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀✝ : 0 ≤ ↑r
hrc : ↑r < ↑c ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
⊢ ↑r ^ d₂ / ↑r ^ d₁ ≤ ↑c

Tactic:
have : (r : ℝ≥0∞) ≠ 0 := by simpa only [ENNReal.coe_eq_zero, Ne] using hr₀
    rw [← ENNReal.rpow_sub _ _ this ENNReal.coe_ne_top]
    refine (ENNReal.rpow_lt_rpow hrc (sub_pos.2 h)).le.trans ?_
    rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (sub_pos.2 h).ne', ENNReal.rpow_one]

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
⊢ μH[d] (⇑((AffineEquiv.homothetyUnitsMulHom x) (Units.mk0 c hc)).symm '' s) = ‖c‖₊⁻¹ ^ d • μH[d] s

Tactic:
AffineEquiv.coe_homothetyUnitsMulHom_apply_symm,

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
⊢ μH[d] (⇑(AffineMap.homothety x ↑(Units.mk0 c hc)⁻¹) '' s) = ‖c‖₊⁻¹ ^ d • μH[d] s
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x : F
⊢ ((map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x = φ (o.rightAngleRotation (φ.symm x))

Tactic:
by
  apply ext_inner_right ℝ
  intro y
  rw [inner_rightAngleRotation_left]
  trans ⟪J (φ.symm x), φ.symm y⟫
  · simp [o.areaForm_map]
  trans ⟪φ (J (φ.symm x)), φ (φ.symm y)⟫
  · rw [φ.inner_map_map]
  · simp

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)
⊢ (↑a * ↑a ^ (-s) * (↑a)⁻¹) • ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • f x =
    ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t

Tactic:
mul_assoc,

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)
⊢ (↑a * (↑a ^ (-s) * (↑a)⁻¹)) • ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • f x =
    ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
⊢ HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z

Tactic:
by
  induction n with
  | zero => simp [logTaylor_succ, logTaylor_zero, Pi.add_def, hasDerivAt_const]
  | succ n ih =>
    rw [logTaylor_succ]
    simp only [Nat.cast_add, Nat.cast_one,
      Finset.sum_range_succ]
    refine HasDerivAt.add ih ?_
    simp only [mul_div_assoc]
    have : HasDerivAt (fun x : ℂ ↦ (x ^ (n + 1) / (n + 1))) (z ^ n) z := by
      simp_rw [div_eq_mul_inv]
      convert! HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1
      simp [field]
    convert! HasDerivAt.const_mul _ this using 2
    ring

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: 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
⊢ ‖t ^ (s - 1)‖ * ‖f t‖ ≤ t ^ (s - 1) * ‖t ^ (-a)‖ * d

Tactic:
mul_assoc,

Goal state after:
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
⊢ ‖t ^ (s - 1)‖ * ‖f t‖ ≤ t ^ (s - 1) * (‖t ^ (-a)‖ * d)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: n : ℕ
ih : ContinuousAt Gamma (-↑(n + 1))
⊢ ContinuousAt Gamma (-↑n)

Tactic:
rw [Nat.cast_add, Nat.cast_one] at ih

Goal state after:
n : ℕ
ih : ContinuousAt Gamma (-(↑n + 1))
⊢ ContinuousAt Gamma (-↑n)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

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

Tactic:
mul_assoc,

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

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

Tactic:
mul_assoc,

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