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

Goal state before:
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 : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hfi : IntegrableOn f (⋃ n, s n) μ
hne : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))

Tactic:
have hfi' : ∫⁻ x in ⋃ n, s n, ‖f x‖₊ ∂μ < ∞ := hfi.2

Goal state after:
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 : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hfi : IntegrableOn f (⋃ n, s n) μ
hne : atTop.NeBot
this : IsDirectedOrder ι
hfi' : ∫⁻ (x : X) in ⋃ n, s n, ↑‖f x‖₊ ∂μ < ∞
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono'✝¹ : ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → μ K₁ ≤ μ K₂
sup_disjoint'✝¹ : ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le'✝¹ : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'✝ : ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → v K₁ ≤ v K₂
sup_disjoint'✝ : ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'✝ : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  (fun μ s ↦ ↑(μ.toFun s)) { toFun := μ, mono' := mono'✝¹, sup_disjoint' := sup_disjoint'✝¹, sup_le' := sup_le'✝¹ } =
    (fun μ s ↦ ↑(μ.toFun s)) { toFun := v, mono' := mono'✝, sup_disjoint' := sup_disjoint'✝, sup_le' := sup_le'✝ }
s : Compacts G
⊢ μ s = v s

Tactic:
exact ENNReal.coe_injective <| congr_fun h s

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

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ μ K ≤ ⨅ t, ⨅ (ht : IsOpen t), ⨅ (_ : ↑K ⊆ t), μ.innerContent { carrier := t, is_open' := ht }

pp: case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ i, f i)

pp: case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ i, f i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }

pp: case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → μ.innerContent { carrier := s₁, is_open' := hs₁ } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }

Tactic:
· exact le_iInf fun U => le_iInf fun hU => le_iInf <| μ.le_innerContent K ⟨U, hU⟩

Goal state after:
case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ i, f i)

case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ i, f i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }

case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → μ.innerContent { carrier := s₁, is_open' := hs₁ } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }
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✝² : SecondCountableTopology R
inst✝¹ : DenselyOrdered R
_s : ℕ → Set R
i : ℕ
inst✝ : BorelSpace R
hs : ∀ (i : ℕ), MeasurableSet (_s i)
this✝ : MeasurableSpace R := borel R
⊢ MeasurableSet (_s i)

Tactic:
exact hs i

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

Goal state before:
pp: case inl
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
l : ℝ
x : R
this✝ : Nonempty R
val✝ : OrderBot R
hf : Tendsto (↑f) (pure ⊥) (𝓝 l)
this : Iic x = Icc ⊥ x
⊢ ofReal (↑f x - leftLim ↑f ⊥) = ofReal (↑f x - l)

Tactic:
leftLim_eq_of_isBot isBot_bot,

Goal state after:
case inl
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
l : ℝ
x : R
this✝ : Nonempty R
val✝ : OrderBot R
hf : Tendsto (↑f) (pure ⊥) (𝓝 l)
this : Iic x = Icc ⊥ x
⊢ ofReal (↑f x - ↑f ⊥) = ofReal (↑f x - l)
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
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : R
⊢ f.measure (Iio x) = ofReal (leftLim (↑f) x - l)

Tactic:
by
  have : Nonempty R := ⟨x⟩
  rw [← Iic_sdiff_right, measure_sdiff _ (nullMeasurableSet_singleton x), measure_singleton,
    f.measure_Iic hf, ← ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)]
    <;> simp

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₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ prehaar (↑K₀) U K₁ ≤ prehaar (↑K₀) U K₂

Tactic:
simp only [prehaar]; rw [div_le_div_iff_of_pos_right]
  · exact mod_cast index_mono K₂.2 h hU
  · exact mod_cast index_pos K₀ hU

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
h : ∀ (v : E), ⟪v, x⟫ = ⟪v, y⟫
⊢ ⟪x - y, x⟫ = ⟪x - y, y⟫

Tactic:
h (x - y)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ∀ (v : E), ⟪v, x⟫ = ⟪v, y⟫
⊢ ⟪x - y, y⟫ = ⟪x - y, y⟫
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
h : ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫
⊢ ⟪x, x - y⟫ = ⟪y, x - y⟫

Tactic:
h (x - y)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫
⊢ ⟪y, x - y⟫ = ⟪y, x - y⟫
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n ↦ ‖u - ↑(w n)‖) atTop (𝓝 δ)
b✝ : ℕ → ℝ := fun n ↦ 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
wq : F := ↑(w q)
a : F := u - wq
b : F := u - wp
half : ℝ := 1 / 2
div : ℝ := 1 / (↑N + 1)
⊢ 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ =
    2 * ‖u - half • (wq + wp)‖ * (2 * ‖u - half • (wq + wp)‖) + ‖wp - wq‖ * ‖wp - wq‖

Tactic:
by
            ring

Goal state after:
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
⊢ r * (‖x‖ * ‖x‖) / (‖x‖ * |r| * ‖x‖) = 1

Tactic:
mul_comm _ |r|,

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
⊢ r * (‖x‖ * ‖x‖) / (|r| * ‖x‖ * ‖x‖) = 1
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 : r < 0
⊢ r * (‖x‖ * ‖x‖) / (‖x‖ * |r| * ‖x‖) = -1

Tactic:
mul_comm _ |r|,

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ r * (‖x‖ * ‖x‖) / (|r| * ‖x‖ * ‖x‖) = -1
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ (x ≠ 0 ∧ ∃ x_1, 0 < -x_1 ∧ -y = -x_1 • x) ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Tactic:
refine Iff.rfl.and (exists_congr fun r => ?_)

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
r : ℝ
⊢ 0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
r : ℝ
⊢ 0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x

Tactic:
rw [neg_pos, neg_smul, neg_inj]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
⊢ Orthonormal 𝕜 v → ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0

Tactic:
intro hv

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
⊢ ‖v i‖ ^ 2 = 1 ^ 2

Tactic:
@norm_sq_eq_re_inner 𝕜,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
⊢ re ⟪v i, v i⟫ = 1 ^ 2
Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: 𝕜 : 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v w : α i
hvw : ⟨i, v⟩ ≠ ⟨i, w⟩
h : v = w
⊢ False

Tactic:
subst h
      exact hvw rfl

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ ≤ ‖(innerSL 𝕜) x‖

Tactic:
refine (mul_le_mul_iff_left₀ h).mp ?_

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ * ‖x‖ ≤ ‖(innerSL 𝕜) x‖ * ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: case e'_2.e'_6
𝕜 : 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, LinearIsometry.map_neg]

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

Goal state before:
pp: case neg
𝕜 : 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
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → re ⟪T x, y⟫_𝕜 ≤ C
x : E
hx : ‖x‖ = 1
hTx : ¬‖T x‖ = 0
⊢ ‖T x‖ ≤ C

Tactic:
specialize h x (((‖T x‖⁻¹ : ℝ) : 𝕜) • T x) hx (by simp [norm_smul, hTx])
    rwa [inner_smul_right, re_ofReal_mul, ← norm_sq_eq_re_inner,
      inv_mul_eq_div, sq, mul_self_div_self] at h

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
⊢ ⟪u, v⟫ = 0 → v ∈ (𝕜 ∙ u)ᗮ

Tactic:
intro hv

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
hv : ⟪u, v⟫ = 0
⊢ v ∈ (𝕜 ∙ u)ᗮ
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
⊢ y + z ∈ Kᗮᗮ → y + z ∈ K

Tactic:
intro hv

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ y + z ∈ K
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ v ∈ K → v ∈ Kᗮᗮ

Tactic:
intro hv

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
hv : v ∈ K
⊢ v ∈ Kᗮᗮ
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ 0
⊢ (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker = ⊤

Tactic:
le_zero_iff,

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ = 0
⊢ (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker = ⊤
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case pos
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:
obtain ⟨V, hV₁, hV₂⟩ := IH φ hn'
      exact ⟨V, hV₁.trans n.le_succ, 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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ K.starProjection v = 0 ↔ v ∈ Kᗮ

Tactic:
refine ⟨fun h w hw => ?_, fun hv => ?_⟩

Goal state after:
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.starProjection v = 0
w : E
hw : w ∈ K
⊢ ⟪w, v⟫ = 0

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
hv : v ∈ Kᗮ
⊢ K.starProjection v = 0
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)
⊢ ∑ x_1, ↑((V x_1).orthogonalProjectionOnto x) = x

Tactic:
exact hV.sum_projection_of_mem_iSup _ ((h.ge :) Submodule.mem_top)

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

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
⊢ LipschitzWith 1 ofLp

Tactic:
by
  intro x y
  change max _ _ ≤ _
  rw [ENNReal.coe_one, one_mul, sup_le_iff]
  exact edist_proj_le_edist_aux p x y

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:
#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:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ∞
x y : PiLp p β
⊢ ↑(nndist x y) = ↑((∑ i, nndist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal))

Tactic:
by
    push_cast
    exact dist_eq_sum (p.toReal_pos_iff_ne_top.mpr hp) _ _

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ edist x y = ∑ i, edist (x.ofLp i) (y.ofLp i)

Tactic:
simp [PiLp.edist_eq_sum]

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ edist x y = (∑ i, edist (x.ofLp i) (y.ofLp i) ^ 2) ^ (1 / 2)

Tactic:
simp [PiLp.edist_eq_sum]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case e_f
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
⊢ ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))

Tactic:
have : 0 < r := by
    by_contra hr
    have := div_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 <| J.lower_le_upper i) (not_lt.1 hr)
    rw [← h] at this
    exact this.not_gt (sub_pos.2 <| I.lower_lt_upper i)

Goal state after:
case e_f
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
⊢ ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: case succ
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun m ↦ (fun J ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
i : ι
m : ℕ
ihm : (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m
⊢ (J (m + 1)).upper i - (J (m + 1)).lower i = (I.upper i - I.lower i) / 2 ^ (m + 1)

Tactic:
| succ m ihm =>

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝¹³ : NormedField K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsStrictOrderedRing K
inst✝¹⁰ : HasSolidNorm K
inst✝⁹ : FloorRing K
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace K E✝
inst✝⁶ : FiniteDimensional K E✝
inst✝⁵ : ProperSpace E✝
L✝ : Submodule ℤ E✝
inst✝⁴ : DiscreteTopology ↥L✝
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
f : ↥(span ℝ ↑L) →ₗ[ℝ] E := (span ℝ ↑L).subtype
L₀ : Submodule ℤ ↥(span ℝ ↑L) := comap (↑ℤ f) L
⊢ L ≤ (↑ℤ f).range

Tactic:
exact fun x hx ↦ LinearMap.mem_range.mpr ⟨⟨x, Submodule.subset_span hx⟩, rfl⟩

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
⊢ InjOn (fun J ↦ {i | J.lower i = x i}) {J | J ∈ π ∧ x ∈ Box.Icc J}

Tactic:
rintro J₁ ⟨h₁, hx₁⟩ J₂ ⟨h₂, hx₂⟩ (H : { i | J₁.lower i = x i } = { i | J₂.lower i = x i })
  suffices ∀ i, (Ioc (J₁.lower i) (J₁.upper i) ∩ Ioc (J₂.lower i) (J₂.upper i)).Nonempty by
    choose y hy₁ hy₂ using this
    exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂
  intro i
  simp only [Set.ext_iff, mem_ofPred] at H
  rcases (hx₁.1 i).eq_or_lt with hi₁ | hi₁
  · have hi₂ : J₂.lower i = x i := (H _).1 hi₁
    have H₁ : x i < J₁.upper i := by simpa only [hi₁] using J₁.lower_lt_upper i
    have H₂ : x i < J₂.upper i := by simpa only [hi₂] using J₂.lower_lt_upper i
    rw [Set.Ioc_inter_Ioc, hi₁, hi₂, sup_idem, Set.nonempty_Ioc]
    exact lt_min H₁ H₂
  · have hi₂ : J₂.lower i < x i := (hx₂.1 i).lt_of_ne (mt (H _).2 hi₁.ne)
    exact ⟨x i, ⟨hi₁, hx₁.2 i⟩, ⟨hi₂, hx₂.2 i⟩⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t = 0
r : ℝ
H : μ (s ∩ ({x} + r • t)) = 0
⊢ μ (s ∩ ({x} + r • t)) / μ ({x} + r • t) < ε

Tactic:
H

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t = 0
r : ℝ
H : μ (s ∩ ({x} + r • t)) = 0
⊢ 0 / μ ({x} + r • t) < ε