mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case e'_5
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₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ ∫ (x : X) in ⋂ n, s n, f x ∂μ =
    ∫ (x : X) in s i₀, f x ∂μ - (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋂ i, s i, f x ∂μ)

pp: 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₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ MeasurableSet (⋂ i, s i)

Tactic:
sub_sub_cancel

Goal state after:
case e'_5
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₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ ∫ (x : X) in ⋂ n, s n, f x ∂μ = ∫ (x : X) in ⋂ i, s i, f x ∂μ

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₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ MeasurableSet (⋂ i, s i)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case convert_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₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
i : ι
hi : i₀ ≤ i
⊢ ∫ (x : X) in s i₀, f x ∂μ - (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i, f x ∂μ) = ∫ (x : X) in s i, f x ∂μ

Tactic:
sub_sub_cancel

Goal state after:
case convert_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₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
i : ι
hi : i₀ ≤ i
⊢ ∫ (x : X) in s i, f x ∂μ = ∫ (x : X) in s i, f x ∂μ
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun x ↦ g * x) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' ↑U
⊢ ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap ↑(Homeomorph.mulLeft g)) U)

Tactic:
simpa only [Opens.iSup_def, Opens.coe_comap, Subtype.coe_mk]

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
⊢ borel G ≤ μ.outerMeasure.caratheodory

Tactic:
refine MeasurableSpace.generateFrom_le ?_

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ ∀ t ∈ {s | IsOpen s}, MeasurableSet t
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
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✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
hl : ⨅ a, ⨅ b, ⨅ (_ : t i \ botSet ⊆ Ioc a b), ofReal (↑f b - ↑f a) < f.length (t i) + ↑(ε' i)
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ f.outer s ≤ f.length (t i) + ofReal ↑(ε' i)

Tactic:
simp only [iInf_lt_iff] at hl

Goal state after:
case inr
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✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
hl : ∃ i_1 i_2, ∃ (_ : t i \ botSet ⊆ Ioc i_1 i_2), ofReal (↑f i_2 - ↑f i_1) < f.length (t i) + ↑(ε' i)
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ f.outer s ≤ f.length (t i) + ofReal ↑(ε' i)
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✝ : SecondCountableTopology R
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ f.outer.caratheodory

Tactic:
refine MeasurableSpace.generateFrom_le ?_

Goal state after:
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : SecondCountableTopology R
⊢ ∀ t ∈ range Ioi, MeasurableSet t
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ (Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}).Nonempty

Tactic:
· exact index_defined K.isCompact hV

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ (E.indicator fun x ↦ 1) ≤ thickenedIndicatorAux δ E

Tactic:
apply indicator_le_thickenedIndicatorAux

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

Goal state before:
pp: case e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * ⟪v i, v i⟫ = ⟪v i, g i • v i⟫

Tactic:
rw [inner_smul_right]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case h_cont
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖uncurry f x‖) '' U ×ˢ s)
⊢ ∀ᵐ (a : Y) ∂μ.restrict s, ContinuousAt (fun x ↦ f x a) x₀

Tactic:
filter_upwards using (by fun_prop)

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Tactic:
rw [← norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq,
    eq_comm]

Goal state after:
case hx
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ 0 ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

case hy
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ 0 ≤ ‖x - y‖
Module: Mathlib.Analysis.InnerProductSpace.Continuous

Goal state before:
pp: E : Type u_4
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
⊢ x = 0

Tactic:
let K := span 𝕜 S

Goal state after:
E : Type u_4
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
⊢ x = 0
Module: Mathlib.Analysis.InnerProductSpace.Continuous

Goal state before:
pp: E : Type u_4
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
⊢ x = 0

Tactic:
have hK : Dense (K : Set E) := hS.mono subset_span

Goal state after:
E : Type u_4
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
hK : Dense ↑K
⊢ x = 0
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖ - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖) / 2)) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

Tactic:
← div_sub_div_same,

Goal state after:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂,
        w₁ x * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖) / 2 - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2)) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1

Tactic:
rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|,
    mul_assoc, abs_of_nonneg hr.le, div_self]
  exact mul_ne_zero hr.ne' (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫ = ‖y‖ ^ 2
⊢ re ⟪x - y, x - y⟫ ≤ 0

Tactic:
have H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2 := by gcongr

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫ = ‖y‖ ^ 2
H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2
⊢ re ⟪x - y, x - y⟫ ≤ 0
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
G : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
r : ℝ
⊢ ⟪r • x, y⟫_ℝ = (starRingEnd ℝ) r * ⟪x, y⟫_ℝ

Tactic:
by
      let := NormedSpace.restrictScalars ℝ 𝕜 E
      have : r • x = (r : 𝕜) • x := rfl
      simp +instances only [Inner.rclikeToReal, this, conj_trivial, inner_smul_left, conj_ofReal,
        re_ofReal_mul]

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

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := ⋯
⊢ (∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0) → ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
intro h
    apply le_antisymm
    · apply le_ciInf
      intro w
      apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _)
      have := h w w.2
      calc
        ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, w - v⟫_ℝ := by linarith
        _ ≤ ‖u - v‖ ^ 2 - 2 * ⟪u - v, w - v⟫_ℝ + ‖w - v‖ ^ 2 := by
          rw [sq]
          refine le_add_of_nonneg_right ?_
          exact sq_nonneg _
        _ = ‖u - v - (w - v)‖ ^ 2 := (@norm_sub_sq ℝ _ _ _ _ _ _).symm
        _ = ‖u - w‖ * ‖u - w‖ := by
          have : u - v - (w - v) = u - w := by abel
          rw [this, sq]
    · change ⨅ w : K, ‖u - w‖ ≤ (fun w : K => ‖u - w‖) ⟨v, hv⟩
      apply ciInf_le
      use 0
      rintro y ⟨z, rfl⟩
      exact norm_nonneg _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ re ⟪u - v, -I • w⟫_𝕜 = re (-I * ⟪u - v, w⟫_𝕜)

Tactic:
rw [inner_smul_right]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ re ⟪u - v, -I • w⟫_𝕜 = re (-I * ⟪u - v, w⟫_𝕜)

Tactic:
by rw [inner_smul_right]

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

Goal state before:
pp: case e'_2.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun i ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2
⊢ ∑ x ∈ s₁ \ s₂, (V x) (f x) = ∑ i ∈ s₁ \ s₂, (V i) (F i)

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_
    simp only [hF₁ i hi]

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

Goal state before:
pp: R : Type u_2
N : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
inst✝² : Module R N
inst✝¹ : ContinuousAdd N
inst✝ : ContinuousConstSMul R N
s t : ClosedSubmodule R N
⊢ ↑(s ⊔ t) = closure (↑s ⊔ ↑t).carrier

Tactic:
by
  simp only [← coe_toSubmodule, toSubmodule_sup]
  simp only [coe_toSubmodule, Submodule.coe_closure, Submodule.carrier_eq_coe]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n : ℕ
⊢ (T ^ n).IsSymmetric

Tactic:
refine Nat.le_induction (by simp [Module.End.one_eq_id]) (fun k _ ih ↦ ?_) n n.zero_le
  rw [Module.End.iterate_succ, ← Module.End.mul_eq_comp]
  exact ih.mul_of_commute hT <| .pow_left rfl k

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

Goal state before:
pp: case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), (U i).HasOrthogonalProjection
inst✝ : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
y : E := (⨆ i, U i).topologicalClosure.starProjection x
proj_x : ∀ (i : ι), (U i).orthogonalProjectionOnto x = (U i).orthogonalProjectionOnto y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ‖(U i).starProjection y - y‖ < ε

Tactic:
norm_sub_rev,

Goal state after:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), (U i).HasOrthogonalProjection
inst✝ : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
y : E := (⨆ i, U i).topologicalClosure.starProjection x
proj_x : ∀ (i : ι), (U i).orthogonalProjectionOnto x = (U i).orthogonalProjectionOnto y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ‖y - (U i).starProjection y‖ < ε
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

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
inst✝ : K.HasOrthogonalProjection
v w : E
hwK : w ∈ K
hw : v - w ∈ Kᗮ
⊢ v - (v - w) ∈ Kᗮᗮ

Tactic:
sub_sub_cancel

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
inst✝ : K.HasOrthogonalProjection
v w : E
hwK : w ∈ K
hw : v - w ∈ Kᗮ
⊢ w ∈ 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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.starProjection u - v ∈ K
houv : ⟪K.starProjection u - v, K.starProjection u - v⟫ = 0
⊢ K.starProjection u = v

Tactic:
inner_self_eq_zero,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.starProjection u - v ∈ K
houv : K.starProjection u - v = 0
⊢ K.starProjection u = v
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.orthogonalProjectionOnto v = 0
⊢ v ∈ Kᗮ

Tactic:
rw [← sub_zero v, ← coe_zero (p := K), ← h]
    exact sub_starProjection_mem_orthogonal (K := K) v

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

Goal state before:
pp: case neg
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : ¬finrank ℝ ↥Wᗮ ≤ n
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod

Tactic:
have : Nontrivial Wᗮ := nontrivial_of_finrank_pos (by lia : 0 < finrank ℝ Wᗮ)

Goal state after:
case neg
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : ¬finrank ℝ ↥Wᗮ ≤ n
this : Nontrivial ↥Wᗮ
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
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
v : E
hv : ‖v‖ = 1
w : E
⊢ (𝕜 ∙ v).starProjection w = ⟪v, w⟫ • v

Tactic:
by
  rw [← smul_starProjection_singleton 𝕜 w]
  simp [hv]

Goal state after:
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 V : Submodule 𝕜 E
inst✝¹ : U.HasOrthogonalProjection
inst✝ : V.HasOrthogonalProjection
h : U.starProjection ∘SL V.starProjection = 0
⊢ U ⟂ V

Tactic:
← orthogonalProjectionOnto_comp_subtypeL_eq_zero_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝¹ : U.HasOrthogonalProjection
inst✝ : V.HasOrthogonalProjection
h : U.starProjection ∘SL V.starProjection = 0
⊢ U.orthogonalProjectionOnto ∘SL V.subtypeL = 0
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ ‖v‖ * ‖v‖ =
    ‖v - orthogonalProjectionFn v‖ * ‖v - orthogonalProjectionFn v‖ +
      ‖orthogonalProjectionFn v‖ * ‖orthogonalProjectionFn v‖

Tactic:
by
  simpa [sq, add_comm] using K.norm_sq_eq_add_norm_sq_starProjection v

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

Goal state before:
pp: case hf
𝕜 : 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)
i : ι
⊢ (AddSubmonoidClass.subtype (V i)) 0 = 0

Tactic:
exact map_zero _

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ A.etaExpand = A

Tactic:
by
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was: `grind` -/
  simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of]
  rfl

Goal state after: