mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
h : χ ^ (orderOf χ - 1) = χ⁻¹
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * ↑(Fintype.card R)

Tactic:
rw [h, ← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm, gaussSum_mul_gaussSum_eq_card hχ hψ,
    MulChar.inv_apply', inv_neg_one]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
⊢ (χ (-1) * ↑(Fintype.card R)) ^ (p ^ n / 2) = χ (↑p ^ n)

Tactic:
by
  have : gaussSum χ ψ ≠ 0 := by
    intro hf
    rw [hf, zero_pow two_ne_zero, eq_comm, mul_eq_zero] at hg
    exact not_isUnit_prime_of_dvd_card
        ((CharP.cast_eq_zero_iff R' p _).mp <| hg.resolve_left (isUnit_one.neg.map χ).ne_zero) hp
  rw [← hg]
  apply mul_right_cancel₀ this
  rw [← hχ.gaussSum_frob_iter p n hp ψ, ← pow_mul, ← pow_succ,
    Nat.two_mul_div_two_add_one_of_odd (fp.1.eq_two_or_odd'.resolve_left hp').pow]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ counit = adjoint (↑↑(equiv n 𝕜).symm ∘ₗ Algebra.linearMap 𝕜 (n → 𝕜)) ∘ₗ ↑↑(equiv n 𝕜).symm

Tactic:
by
  ext
  simp [← toSpanSingleton_one_eq_algebraLinearMap, comp_toSpanSingleton,
    adjoint_toSpanSingleton, inner_eq_star_dotProduct]

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_6
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ (∫⁻ (t : A i), (∫⋯∫⁻_{j}, f ∂μ) (X t) ∂μ i) ^ p = (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p

Tactic:
have hi' : i ∉ ({j} : Finset ι) := by
                simp only [Finset.mem_singleton] at hj ⊢
                exact fun h ↦ hi (h ▸ hj)

Goal state after:
case e'_6
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
hi' : i ∉ {j}
⊢ (∫⁻ (t : A i), (∫⋯∫⁻_{j}, f ∂μ) (X t) ∂μ i) ^ p = (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p
Module: Mathlib.Analysis.InnerProductSpace.Semisimple

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ = ⊤

Tactic:
replace hp₂ : Module.Finite 𝕜 q := Submodule.finiteDimensional_of_le hq₂

Goal state after:
case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
hp₂ : Module.Finite 𝕜 ↥q
⊢ q ⊔ qᗮ = ⊤
Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
⊢ OrthogonalFamily 𝕜 (fun γ ↦ ↥(⨅ j, (T j).eigenspace (γ j))) fun γ ↦ (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ

Tactic:
by
  intro f g hfg Ef Eg
  obtain ⟨a, ha⟩ := Function.ne_iff.mp hfg
  have H := orthogonalFamily_eigenspaces (hT a) ha
  simp only [Submodule.coe_subtypeₗᵢ, Submodule.coe_subtype, Subtype.forall] at H
  apply H
  · exact (Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (f _)).mp Ef.2 _
  · exact (Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (g _)).mp Eg.2 _

Goal state after:
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 : E →ₗ.[R] F
hf : f.IsClosable
x✝¹ x✝ : E →ₗ.[R] F
hy₁ : f.graph.topologicalClosure = x✝¹.graph
hy₂ : f.graph.topologicalClosure = x✝.graph
⊢ x✝¹.graph = x✝.graph

Tactic:
← hy₁,

Goal state after:
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 : E →ₗ.[R] F
hf : f.IsClosable
x✝¹ x✝ : E →ₗ.[R] F
hy₁ : f.graph.topologicalClosure = x✝¹.graph
hy₂ : f.graph.topologicalClosure = x✝.graph
⊢ f.graph.topologicalClosure = x✝.graph
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
this : (↑n)⁻¹ < (↑p)⁻¹
⊢ ↑p < ↑n

Tactic:
inv_lt_inv₀ _ (zero_lt_one.trans_le (NNReal.coe_le_coe.mpr 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
this : ↑p < ↑n
⊢ ↑p < ↑n

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
this : (↑n)⁻¹ < (↑p)⁻¹
⊢ 0 < ↑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 y : E ⊗[𝕜] F
⊢ x = y ↔ ∀ (a : E) (b : F), inner 𝕜 (a ⊗ₜ[𝕜] b) x = inner 𝕜 (a ⊗ₜ[𝕜] b) y

Tactic:
by
  simpa only [← inner_conj_symm x, ← inner_conj_symm y, starRingEnd_apply, star_inj] using
    TensorProduct.ext_iff_inner_right (x := x) (y := y)

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) = ∞
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
suffices μ (⋃ n, S n) ≤ ⨆ n, μ (S n) by calc
    μ (s ∩ t) + μ (s \ t) = μ (s ∩ t) + μ (⋃ n, S n) := by rw [iUnion_S]
    _ ≤ μ (s ∩ t) + ⨆ n, μ (S n) := by gcongr
    _ = ⨆ n, μ (s ∩ t) + μ (S n) := ENNReal.add_iSup ..
    _ ≤ μ s := iSup_le hSs

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) = ∞
⊢ μ (⋃ n, S n) ≤ ⨆ n, μ (S n)
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
⊢ μHE[d₂] s = 0 ∨ μHE[d₁] s = ⊤

Tactic:
euclideanHausdorffMeasure_def

Goal state after:
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℕ
h : d₁ < d₂
s : Set X
⊢ (volume.addHaarScalarFactor μH[↑d₂] • μH[↑d₂]) s = 0 ∨ (volume.addHaarScalarFactor μH[↑d₁] • μH[↑d₁]) s = ⊤
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
f : X → Y
d : ℕ
hf : Isometry f
⊢ map f μHE[d] = μHE[d].restrict (Set.range f)

Tactic:
euclideanHausdorffMeasure_def

Goal state after:
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
f : X → Y
d : ℕ
hf : Isometry f
⊢ map f (volume.addHaarScalarFactor μH[↑d] • μH[↑d]) =
    (volume.addHaarScalarFactor μH[↑d] • μH[↑d]).restrict (Set.range f)
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
V : Type u_3
P : Type u_4
inst✝¹¹ : NormedAddCommGroup V
inst✝¹⁰ : InnerProductSpace ℝ V
inst✝⁹ : MeasurableSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : FiniteDimensional ℝ V
inst✝⁶ : MetricSpace P
inst✝⁵ : MeasurableSpace P
inst✝⁴ : BorelSpace P
inst✝³ : NormedAddTorsor V P
α : Type u_5
inst✝² : AddGroup α
inst✝¹ : AddAction α X
inst✝ : IsIsometricVAdd α X
d : ℕ
⊢ VAddInvariantMeasure α X μHE[d]

Tactic:
euclideanHausdorffMeasure_def

Goal state after:
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
V : Type u_3
P : Type u_4
inst✝¹¹ : NormedAddCommGroup V
inst✝¹⁰ : InnerProductSpace ℝ V
inst✝⁹ : MeasurableSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : FiniteDimensional ℝ V
inst✝⁶ : MetricSpace P
inst✝⁵ : MeasurableSpace P
inst✝⁴ : BorelSpace P
inst✝³ : NormedAddTorsor V P
α : Type u_5
inst✝² : AddGroup α
inst✝¹ : AddAction α X
inst✝ : IsIsometricVAdd α X
d : ℕ
⊢ VAddInvariantMeasure α X (volume.addHaarScalarFactor μH[↑d] • μH[↑d])
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
V : Type u_3
P : Type u_4
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace ℝ V
inst✝⁸ : MeasurableSpace V
inst✝⁷ : BorelSpace V
inst✝⁶ : FiniteDimensional ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : MeasurableSpace P
inst✝³ : BorelSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : AddGroup X
inst✝ : IsIsometricVAdd X X
d : ℕ
⊢ μHE[d].IsAddLeftInvariant

Tactic:
euclideanHausdorffMeasure_def

Goal state after:
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
V : Type u_3
P : Type u_4
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace ℝ V
inst✝⁸ : MeasurableSpace V
inst✝⁷ : BorelSpace V
inst✝⁶ : FiniteDimensional ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : MeasurableSpace P
inst✝³ : BorelSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : AddGroup X
inst✝ : IsIsometricVAdd X X
d : ℕ
⊢ (volume.addHaarScalarFactor μH[↑d] • μH[↑d]).IsAddLeftInvariant
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
V : Type u_3
P : Type u_4
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace ℝ V
inst✝⁸ : MeasurableSpace V
inst✝⁷ : BorelSpace V
inst✝⁶ : FiniteDimensional ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : MeasurableSpace P
inst✝³ : BorelSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : AddGroup X
inst✝ : IsIsometricVAdd Xᵃᵒᵖ X
d : ℕ
⊢ μHE[d].IsAddRightInvariant

Tactic:
euclideanHausdorffMeasure_def

Goal state after:
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
V : Type u_3
P : Type u_4
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace ℝ V
inst✝⁸ : MeasurableSpace V
inst✝⁷ : BorelSpace V
inst✝⁶ : FiniteDimensional ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : MeasurableSpace P
inst✝³ : BorelSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : AddGroup X
inst✝ : IsIsometricVAdd Xᵃᵒᵖ X
d : ℕ
⊢ (volume.addHaarScalarFactor μH[↑d] • μH[↑d]).IsAddRightInvariant
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
⊢ normDet 0 = 0 ^ finrank 𝕜 U

Tactic:
by
  nontriviality U
  simp [zero_pow finrank_pos.ne.symm, normDet_eq_zero_iff_ker_ne_bot]

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

Goal state before:
pp: case pos
𝕜 : 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 = ⊥
b : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(↑f).range
hf : f = (↑f).range.subtypeₗᵢ.toContinuousLinearMap ∘SL f.rangeRestrict
⊢ ↑((↑f).normDet ^ 2) = LinearMap.det (↑(ContinuousLinearMap.adjoint f.rangeRestrict) ∘ₗ ↑f.rangeRestrict)

Tactic:
← det_toMatrix bu.toBasis,

Goal state after:
case pos
𝕜 : 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 = ⊥
b : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(↑f).range
hf : f = (↑f).range.subtypeₗᵢ.toContinuousLinearMap ∘SL f.rangeRestrict
⊢ ↑((↑f).normDet ^ 2) =
    ((toMatrix bu.toBasis bu.toBasis) (↑(ContinuousLinearMap.adjoint f.rangeRestrict) ∘ₗ ↑f.rangeRestrict)).det
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), ediam (t n) ≤ 1
m : ℕ
hm : x ∈ t m
A : (t m).Nonempty
⊢ 1 = ⨆ (_ : (t m).Nonempty), 1

Tactic:
by simp only [A, ciSup_pos]

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

Goal state before:
pp: case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
y : H
hy : y ∈ S
⊢ ⟪y, x⟫.im = 0

Tactic:
have hiy := h (I • y)

Goal state after:
case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
y : H
hy : y ∈ S
hiy : -(I • I • y) ∈ S → inner ℝ (I • y) x = 0
⊢ ⟪y, x⟫.im = 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
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
⊢ Function.Injective ⇑(ContinuousLinearMap.pi fun x ↦ adjoint (kerFun K x))

Tactic:
refine (injective_iff_map_eq_zero _).mpr fun f h ↦ ?_
    refine UniformSpace.Completion.denseRange_coe.eq_zero_of_inner_right 𝕜 fun ff ↦ ?_
    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_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
⊢ Measure.map ⇑(AffineMap.homothety x c) μH[d] = ‖c‖₊⁻¹ ^ d • μH[d]

Tactic:
by
  ext s hs
  rw [Measure.map_apply (AffineMap.homothety_continuous x c).measurable hs,
    hausdorffMeasure_homothety_preimage hd x hc s, Measure.smul_apply]

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

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

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

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

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

Tactic:
· simp_all

Goal state after:
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

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

case «1».«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) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ ⟪![x, y] ((fun i ↦ i) ⟨1, ⋯⟩), ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩)⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

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

Tactic:
· 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)
x y : E
h : ⟪x, y⟫ = 0
⊢ |(o.areaForm x) y| = ‖x‖ * ‖y‖

Tactic:
by
  rw [o.areaForm_to_volumeForm, o.abs_volumeForm_apply_of_pairwise_orthogonal]
  · simp [Fin.prod_univ_succ]
  intro i j hij
  fin_cases i <;> fin_cases j
  · simp_all
  · simpa using h
  · simpa [real_inner_comm] using h
  · simp_all

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
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c) volume

Tactic:
by
  obtain ⟨d, hd'⟩ := hf.isBigOWith
  simp_rw [IsBigOWith, eventually_atTop] at hd'
  obtain ⟨e, he⟩ := hd'
  have he' : 0 < max e 1 := zero_lt_one.trans_le (le_max_right _ _)
  refine ⟨max e 1, he', ?_, ?_⟩
  · refine AEStronglyMeasurable.mul ?_ (hfc.mono_set (Ioi_subset_Ioi he'.le))
    refine (continuousOn_of_forall_continuousAt fun t ht => ?_).aestronglyMeasurable
      measurableSet_Ioi
    exact continuousAt_rpow_const _ _ (Or.inl <| (he'.trans ht).ne')
  · have : ∀ᵐ t : ℝ ∂volume.restrict (Ioi <| max e 1),
        ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d := by
      refine (ae_restrict_mem measurableSet_Ioi).mono fun t ht => ?_
      have ht' : 0 < t := he'.trans ht
      rw [norm_mul, rpow_add ht', ← norm_of_nonneg (rpow_nonneg ht'.le (-a)), mul_assoc,
        mul_comm _ d, norm_of_nonneg (rpow_nonneg ht'.le _)]
      gcongr
      exact he t ((le_max_left e 1).trans_lt ht).le
    refine (HasFiniteIntegral.mul_const ?_ _).mono' this
    exact (integrableOn_Ioi_rpow_of_lt (by linarith) he').hasFiniteIntegral

Goal state after: