mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ ↑(thickenedIndicatorAux δ E x).toNNReal + |↑(thickenedIndicatorAux δ E y).toNNReal| ≤ 2

Tactic:
NNReal.abs_eq,

Goal state after:
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ ↑(thickenedIndicatorAux δ E x).toNNReal + ↑(thickenedIndicatorAux δ E y).toNNReal ≤ 2
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:

Tactic:
1
    _ ≤ infEDist y E * (↑δ.toNNReal)⁻¹ := (not_le.mp h_le).le
    _ ≤ edist x y * (↑δ.toNNReal)⁻¹ + infEDist x E * (↑δ.toNNReal)⁻¹ := by
      rw [← add_mul, edist_comm]
      gcongr
      exact infEDist_le_edist_add_infEDist

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (∞ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : (∞ • μ) s ≠ ∞
⊢ (∞ • μ) s = 0

Tactic:
simp only [true_and, Measure.smul_apply, ENNReal.mul_eq_top,
    top_ne_zero, Ne, not_false_iff, not_or, Classical.not_not, smul_eq_mul] at hμs

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (∞ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : ¬μ s = ∞ ∧ μ s = 0
⊢ (∞ • μ) s = 0
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero : Tendsto (fun n ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
⊢ (fun a ↦ ‖↑↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) a‖ₑ) =ᵐ[μ] fun a ↦ ENNReal.ofReal ‖fs n a - f a‖

Tactic:
← Integrable.toL1_sub

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero : Tendsto (fun n ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
⊢ (fun a ↦ ‖↑↑(Integrable.toL1 (fs n - f) ⋯) a‖ₑ) =ᵐ[μ] fun a ↦ ENNReal.ofReal ‖fs n a - f a‖
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h✝ : {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}
⊢ ∀ (a : α), Tendsto (fun n ↦ fs n a) l (𝓝 (f a)) → Tendsto (fun n ↦ fs (x (n + k)) a) atTop (𝓝 (f a))

Tactic:
refine fun a h_lin => @Tendsto.comp _ _ _ (fun n => x (n + k)) (fun n => fs n a) _ _ _ h_lin ?_

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h✝ : {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}
a : α
h_lin : Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
⊢ Tendsto (fun n ↦ x (n + k)) atTop l
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
⊢ f.outer (Ioc a b) ≤ ofReal (↑f b - ↑f a)

pp: case refine_2
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
⊢ ofReal (↑f b - ↑f a) ≤ f.outer (Ioc a b)

Tactic:
· rw [← f.length_Ioc]
    apply outer_le_length

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
⊢ ofReal (↑f b - ↑f a) ≤ f.outer (Ioc a b)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case refine_2
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ IntegrableOn f (⋃ n, s i₀ \ s n) μ

Tactic:
rw [← sdiff_iInter]
    exact hi₀.mono_set sdiff_subset

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

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
⊢ f.length (t \ botSet ∩ Ioi c) + f.length (t \ Ioi c) ≤ ofReal (↑f b - ↑f a)

Tactic:
← length_sdiff_botSet (s := t \ Ioi c),

Goal state after:
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
⊢ f.length (t \ botSet ∩ Ioi c) + f.length ((t \ Ioi c) \ botSet) ≤ ofReal (↑f b - ↑f a)
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t = t
hts : μ (t ∩ s) = 0
⊢ μ t = 0

Tactic:
rw [measure_eq_tsum h]; simp [ht, hts]

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
U : Set G
hUo : IsOpen U
hAU : A ⊆ U
hr : μ.innerContent { carrier := U, is_open' := ⋯ } < r
⊢ ∃ U ⊇ A, IsOpen U ∧ μ.measure U < r

Tactic:
rw [← μ.outerMeasure_of_isOpen U hUo, ← μ.measure_apply hUo.measurableSet] at hr

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
U : Set G
hUo : IsOpen U
hAU : A ⊆ U
hr : μ.measure U < r
⊢ ∃ U ⊇ A, IsOpen U ∧ μ.measure U < r
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ¬∃ K', K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
⊢ False

Tactic:
simp only [not_exists, not_and, not_le] at hc

Goal state after:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → μ K + ↑ε < μ x
⊢ False
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:

Tactic:
∫ x in s, f x ∂μ = ∑' g : G, ∫ x in s ∩ g • t, f x ∂μ := ht.setIntegral_eq_tsum hfs
      _ = ∑' g : G, ∫ x in g • t ∩ s, f (g⁻¹ • x) ∂μ := by simp only [hf, inter_comm]
      _ = ∫ x in t, f x ∂μ := (hs.setIntegral_eq_tsum' hft).symm

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : R
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
this : a ≤ x
⊢ x ∈ {a}

Tactic:
simp [le_antisymm this (hx 0).2]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
⊢ index ((fun h ↦ g * h) '' K) V ≤ index K V

Tactic:
rcases index_elim hK hV with ⟨s, h1s, h2s⟩

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ index ((fun h ↦ g * h) '' K) V ≤ index K V
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
r : 𝕜
⊢ ⟪x, r • y⟫ = r * ⟪x, y⟫

Tactic:
by
  rw [← inner_conj_symm, inner_smul_left]
  simp only [conj_conj, inner_conj_symm, map_mul]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋯
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ haarProduct ↑K₀

pp: case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋯
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ ⋂ i ∈ t, clPrehaar (↑K₀) i

Tactic:
· apply prehaar_mem_haarProduct K₀; use 1; rwa [h1V₀.interior_eq]

Goal state after:
case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋯
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ ⋂ i ∈ t, clPrehaar (↑K₀) i
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
this : discrim (normSq x) (2 * ‖⟪x, y⟫‖) (normSq y) ≤ 0
⊢ ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖ ≤ re ⟪x, x⟫ * re ⟪y, y⟫

Tactic:
rw [norm_inner_symm y x]

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
this : discrim (normSq x) (2 * ‖⟪x, y⟫‖) (normSq y) ≤ 0
⊢ ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ ≤ re ⟪x, x⟫ * re ⟪y, y⟫
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_6
f : X → ℝ
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable (⇑g * f) μ

Tactic:
rw [← SimpleFunc.coe_toLargerSpace_eq hm g]

Goal state after:
X : Type u_6
f : X → ℝ
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable (⇑(SimpleFunc.toLargerSpace hm g) * f) μ
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ⟪x, 0⟫ = 0

Tactic:
rw [← inner_conj_symm, inner_zero_left, map_zero]

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

Goal state before:
pp: case ha
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : ⟪x, y⟫ • x = ⟪x, x⟫ • y
⊢ ⟪x, x⟫ ≠ 0

Tactic:
inner_self_ne_zero

Goal state after:
case ha
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : ⟪x, y⟫ • x = ⟪x, x⟫ • y
⊢ x ≠ 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst✝¹ : K₀.HasOrthogonalProjection
inst✝ : K₁.HasOrthogonalProjection
⊢ K₀ᗮ ≤ K₁ ↔ K₁ᗮ ≤ K₀

Tactic:
← orthogonal_le_orthogonal_iff,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst✝¹ : K₀.HasOrthogonalProjection
inst✝ : K₁.HasOrthogonalProjection
⊢ K₁ᗮ ≤ K₀ᗮᗮ ↔ K₁ᗮ ≤ K₀
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst✝¹ : K₀.HasOrthogonalProjection
inst✝ : K₁.HasOrthogonalProjection
⊢ K₀ ≤ K₁ᗮ ↔ K₁ ≤ K₀ᗮ

Tactic:
← orthogonal_le_orthogonal_iff,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst✝¹ : K₀.HasOrthogonalProjection
inst✝ : K₁.HasOrthogonalProjection
⊢ K₁ᗮᗮ ≤ K₀ᗮ ↔ K₁ ≤ K₀ᗮ
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
v : E
⊢ v ∈ U ↔ ‖U.starProjection v‖ = ‖v‖

Tactic:
refine ⟨fun h => norm_starProjection_apply _ h, fun h => ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
v : E
h : ‖U.starProjection v‖ = ‖v‖
⊢ v ∈ U
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := x₁ - x₂
I : ‖f x - d • y‖ ≤ 2 * δ
J : dist (f (σ' d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖d‖⁻¹ * ‖x₁ - x₂‖ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖ * (↑n + ↑n)

Tactic:
gcongr
          · simpa using dinv
          · exact le_trans (norm_sub_le _ _) (by gcongr)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

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
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ (DirectSum.coeAddMonoidHom V) (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) = x

Tactic:
DirectSum.coeAddMonoidHom,

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
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ (toAddMonoid fun i ↦ AddSubmonoidClass.subtype (V i))
      (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) =
    x
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n ↦ y - h^[n] y) atTop (𝓝 (f x))
L₂ : Tendsto (fun n ↦ y - h^[n] y) atTop (𝓝 (y - 0))
feq : f x = y
⊢ ∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖

Tactic:
exact ⟨x, feq, x_ineq⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Ring 𝕜
⊢ LinearIndependent 𝕜 fun i ↦ Pi.single i 1

Tactic:
exact Pi.linearIndependent_single_one ι 𝕜

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g : PiLp ∞ α
h✝ : Nonempty ι
r : ℝ≥0
this : BddAbove (range fun i ↦ dist (f.ofLp i) (g.ofLp i))
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) ≤ ↑r ↔ ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i)) ≤ ↑r

Tactic:
simp [ciSup_le_iff this]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α✝ : Type u_2
β✝ : Type u_3
hp : Fact (1 ≤ p)
inst✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : α × β
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖

Tactic:
toLp_add,

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
α✝ : Type u_2
β✝ : Type u_3
hp : Fact (1 ≤ p)
inst✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : α × β
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α✝ : Type u_2
β✝ : Type u_3
hp : Fact (1 ≤ p)
inst✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedAddCommGroup β
x y : α × β
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖

Tactic:
toLp_add,

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
α✝ : Type u_2
β✝ : Type u_3
hp : Fact (1 ≤ p)
inst✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedAddCommGroup β
x y : α × β
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1✝ x2✝ : WithLp p (α × β)
⊢ edist (WithLp.map p (Prod.map f g) x1✝) (WithLp.map p (Prod.map f g) x2✝) = edist x1✝ x2✝

Tactic:
rcases p.trichotomy with rfl | rfl | hp

Goal state after:
case inl
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
hp : Fact (1 ≤ 0)
x1✝ x2✝ : WithLp 0 (α × β)
⊢ edist (WithLp.map 0 (Prod.map f g) x1✝) (WithLp.map 0 (Prod.map f g) x2✝) = edist x1✝ x2✝

case inr.inl
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
hp : Fact (1 ≤ ∞)
x1✝ x2✝ : WithLp ∞ (α × β)
⊢ edist (WithLp.map ∞ (Prod.map f g) x1✝) (WithLp.map ∞ (Prod.map f g) x2✝) = edist x1✝ x2✝

case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1✝ x2✝ : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist (WithLp.map p (Prod.map f g) x1✝) (WithLp.map p (Prod.map f g) x2✝) = edist x1✝ x2✝