mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
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 fun U hU => isOpen_iUnion hU

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

Goal state before:
pp: case neg
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s μ
⊢ ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

Tactic:
integral_undef hfs,

Goal state after:
case neg
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s μ
⊢ 0 = ∫ (x : α) in t, f x ∂μ
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
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
⊢ ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ μ.real sᶜ * C

Tactic:
have h2 : ∫ _ in sᶜ, C ∂μ = μ.real sᶜ * C := by
    rw [setIntegral_const C, smul_eq_mul]

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
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
h2 : ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C
⊢ ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ μ.real sᶜ * C
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
ν : Measure α
inst✝² : SMulInvariantMeasure G α ν
inst✝¹ : Countable G
inst✝ : MeasurableConstSMul G α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
t : Set α
fund_dom_t : IsFundamentalDomain G t ν
⊢ Measure.map (Quotient.mk α_mod_G) (ν.restrict s) = Measure.map (Quotient.mk α_mod_G) (ν.restrict t)

Tactic:
rw [fund_dom_s.quotientMeasure_eq _ fund_dom_t]

Goal state after:
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✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : R
this✝ : Nonempty R
val✝ : NoBotOrder R
this : NoMinOrder R
⊢ Tendsto (fun x_1 ↦ ofReal (↑f x - ↑f x_1)) atBot (𝓝 (ofReal (↑f x - l)))

Tactic:
exact ENNReal.tendsto_ofReal (Tendsto.const_sub _ hf)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : NormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
⊢ 0 ≤ re ⟪x, x⟫_𝕜

Tactic:
by
      rw [← InnerProductSpace.norm_sq_eq_re_inner]
      apply sq_nonneg

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

Goal state before:
pp: case pos
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : X → ℝ := fun x ↦ max (f x) 0
g_int : Integrable g μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s

Tactic:
have : ENNReal.ofReal (∫ x, f x ∂μ) ≤ ENNReal.ofReal (∫ x, g x ∂μ) := by
    apply ENNReal.ofReal_le_ofReal
    exact integral_mono H g_int (fun x ↦ le_max_left _ _)

Goal state after:
case pos
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : X → ℝ := fun x ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s
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
⊢ ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫

Tactic:
by
  simp only [inner_add_left, inner_add_right]; ring

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
V : OpenNhdsOf 1
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V

Tactic:
have := (Classical.choose_spec (nonempty_iInter_clPrehaar K₀)).2; rw [mem_iInter] at this
  exact this V

Goal state after:
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 y : E
⊢ ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫

Tactic:
by
  simp only [inner_add_left, inner_add_right]; ring

Goal state after:
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 y : E
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖
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 y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖
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 y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫ + ‖y‖ ^ 2
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 y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫ + ‖y‖ ^ 2

Tactic:
rw [← sq (M := ℝ)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫ + ‖y‖ ^ 2
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 y : E
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖
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 y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖
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 y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ ^ 2
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 y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ ^ 2

Tactic:
rw [← sq (M := ℝ)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ ^ 2
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 y : E
⊢ re ⟪x, y⟫ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2

Tactic:
rw [@norm_sub_mul_self 𝕜]
  ring

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
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
K₀ : PositiveCompacts G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
h : μ ↑K₀ = 1
⊢ haarMeasure K₀ = μ

Tactic:
haarMeasure_unique μ K₀,

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
K₀ : PositiveCompacts G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
h : μ ↑K₀ = 1
⊢ haarMeasure K₀ = μ ↑K₀ • haarMeasure K₀
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:
by
  let K := span 𝕜 S
  have hK : Dense (K : Set E) := hS.mono subset_span
  have : (⟪x, ·⟫) = 0 := (continuous_const.inner continuous_id).ext_on
    hK continuous_const fun v ↦ Submodule.span_induction h (by simp)
      (by simp +contextual [inner_add_right]) (by simp +contextual [inner_smul_right])
  simpa using congr_fun this x

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
⊢ ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x

Tactic:
refine fun h => or_iff_not_imp_left.2 fun hx₀ => ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: 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 := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ - 2 * re (θ * ⟪u - v, w - v⟫_ℝ) + ‖θ‖ * ‖w - v‖ * (‖θ‖ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)

Tactic:
change
              ‖u - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) +
                absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
              ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)

Goal state after:
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 := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) + |θ| * ‖w - v‖ * (|θ| * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

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
K : Submodule 𝕜 E
f : E →ₗᵢ[𝕜] F
⊢ map f.toLinearMap Kᗮ = (map f.toLinearMap K)ᗮ ⊓ f.range

Tactic:
by
  simp only [Submodule.ext_iff, mem_map, mem_orthogonal, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, mem_inf, mem_map, LinearMap.mem_range,
    LinearIsometry.coe_toLinearMap]
  grind [LinearIsometry.inner_map_map]

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:
rw [← 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.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp p (α × β)
⊢ edist f g = edist g f

Tactic:
by
  rcases p.trichotomy with (rfl | rfl | h)
  · simp only [prod_edist_eq_card, edist_comm]
  · simp only [prod_edist_eq_sup, edist_comm]
  · simp only [prod_edist_eq_add h, edist_comm]

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

Goal state before:
pp: case succ
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
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod

Tactic:
let W := (ContinuousLinearMap.id ℝ F - φ).ker
    have hW : ∀ w ∈ W, φ w = w := fun w hw => (sub_eq_zero.mp hw).symm
    by_cases hn' : finrank ℝ Wᗮ ≤ n
    · obtain ⟨V, hV₁, hV₂⟩ := IH φ hn'
      exact ⟨V, hV₁.trans n.le_succ, hV₂⟩
    -- Take a nonzero element `v` of the orthogonal complement of `W`.
    have : Nontrivial Wᗮ := nontrivial_of_finrank_pos (by lia : 0 < finrank ℝ Wᗮ)
    obtain ⟨v, hv⟩ := exists_ne (0 : Wᗮ)
    have hφv : φ v ∈ Wᗮ := by
      intro w hw
      rw [← hW w hw, LinearIsometryEquiv.inner_map_map]
      exact v.prop w hw
    have hv' : (v : F) ∉ W := by
      intro h
      exact hv ((mem_left_iff_eq_zero_of_disjoint W.orthogonal_disjoint).mp h)
    -- Let `ρ` be the reflection in `v - φ v`; this is designed to swap `v` and `φ v`
    let x : F := v - φ v
    let ρ := (ℝ ∙ x)ᗮ.reflection
    -- Notation: Let `V` be the fixed subspace of `φ.trans ρ`
    let V := (ContinuousLinearMap.id ℝ F - φ.trans ρ).ker
    have hV : ∀ w, ρ (φ w) = w → w ∈ V := by
      intro w hw
      change w - ρ (φ w) = 0
      rw [sub_eq_zero, hw]
    -- Everything fixed by `φ` is fixed by `φ.trans ρ`
    have H₂V : W ≤ V := by
      intro w hw
      apply hV
      rw [hW w hw]
      refine reflection_mem_subspace_eq_self ?_
      rw [mem_orthogonal_singleton_iff_inner_left]
      exact Submodule.sub_mem _ v.prop hφv _ hw
    -- `v` is also fixed by `φ.trans ρ`
    have H₁V : (v : F) ∈ V := by
      apply hV
      have : ρ v = φ v := reflection_sub (φ.norm_map v).symm
      rw [← this]
      exact reflection_reflection _ _
    -- By dimension-counting, the complement of the fixed subspace of `φ.trans ρ` has dimension at
    -- most `n`
    have : finrank ℝ Vᗮ ≤ n := by
      change finrank ℝ Wᗮ ≤ n + 1 at hn
      have : finrank ℝ W + 1 ≤ finrank ℝ V :=
        finrank_lt_finrank_of_lt ((SetLike.lt_iff_le_and_exists (B := F)).2 ⟨H₂V, v, H₁V, hv'⟩)
      have : finrank ℝ V + finrank ℝ Vᗮ = finrank ℝ F := V.finrank_add_finrank_orthogonal
      have : finrank ℝ W + finrank ℝ Wᗮ = finrank ℝ F := W.finrank_add_finrank_orthogonal
      lia
    -- So apply the inductive hypothesis to `φ.trans ρ`
    obtain ⟨l, hl, hφl⟩ := IH (ρ * φ) this
    -- Prepend `ρ` to the factorization into reflections obtained for `φ.trans ρ`; this gives a
    -- factorization into reflections for `φ`.
    refine ⟨x::l, Nat.succ_le_succ hl, ?_⟩
    rw [List.map_cons, List.prod_cons]
    have := congr_arg (ρ * ·) hφl
    rwa [← mul_assoc, reflection_mul_reflection, one_mul] at this

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

Goal state before:
pp: case mp.refine_2.inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b = e
⊢ ⟪↑⟨a, ha'⟩, ↑⟨b, hb'⟩⟫_𝕜 = 0

pp: case mp.refine_2.inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b ∈ v
⊢ ⟪↑⟨a, ha'⟩, ↑⟨b, hb'⟩⟫_𝕜 = 0

Tactic:
· simpa [hb] using h_end a ha

Goal state after:
case mp.refine_2.inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b ∈ v
⊢ ⟪↑⟨a, ha'⟩, ↑⟨b, hb'⟩⟫_𝕜 = 0
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A ∈ unitaryGroup n α ↔ star A * A = 1

Tactic:
refine ⟨And.left, fun hA => ⟨hA, ?_⟩⟩
  rwa [mul_eq_one_comm] at hA

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

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i' ≠ i
a : β i
⊢ Pi.single i a i' = 0

Tactic:
Pi.single_eq_of_ne h

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i' ≠ i
a : β i
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : ↥(unitaryGroup n α)
⊢ (transpose U)⁻¹ = map_star U

Tactic:
simp [← map_star_inv_eq_transpose]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑g

Tactic:
refine g.continuous_of_isClosed_graph (IsSeqClosed.isClosed ?_)
  rintro φ ⟨x, y⟩ hφg hφ
  refine hg (Prod.fst ∘ φ) x y ((continuous_fst.tendsto _).comp hφ) ?_
  have : g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ := by
    ext n
    exact (hφg n).symm
  rw [this]
  exact (continuous_snd.tendsto _).comp hφ

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

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t ∈ Icc 0 1, ∀ (i : ι), (b.repr x) i = (b.repr (∑ i, t i • b i)) i) ↔ ∀ (i : ι), (b.repr x) i ∈ Icc 0 1

Tactic:
_root_.map_sum,

Goal state after:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t ∈ Icc 0 1, ∀ (i : ι), (b.repr x) i = (∑ x, b.repr (t x • b x)) i) ↔ ∀ (i : ι), (b.repr x) i ∈ Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
val✝ : Fintype ι
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
have := addHaarMeasure_unique μ (piIcc01 ι)

Goal state after:
case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
val✝ : Fintype ι
this : μ = μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
s : Set E
h : r ≠ 0
⊢ ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹⁻¹| * μ s = ENNReal.ofReal |r ^ finrank ℝ E| * μ s

Tactic:
inv_inv

Goal state after:
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
s : Set E
h : r ≠ 0
⊢ ENNReal.ofReal |r ^ finrank ℝ E| * μ s = ENNReal.ofReal |r ^ finrank ℝ E| * μ s