mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
r : 𝕜
x : F
⊢ √(‖r‖ ^ 2) * √(normSq x) ≤ ‖r‖ * ‖x‖

Tactic:
simp [sqrt_normSq_eq_norm]

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 : E
⊢ ‖x‖ = 0 ↔ x = 0

Tactic:
norm_eq_zero

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ x = 0 ↔ x = 0
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
⊢ √(‖r‖ ^ 2) * √(re ↑(normSq x)) ≤ ‖r‖ * ‖x‖

pp: case hx
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
⊢ 0 ≤ ‖r‖ ^ 2

Tactic:
ofReal_re

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
⊢ √(‖r‖ ^ 2) * √(normSq x) ≤ ‖r‖ * ‖x‖

case hx
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
⊢ 0 ≤ ‖r‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
⊢ √(‖r‖ ^ 2) * √(normSq x) ≤ ‖r‖ * ‖x‖

Tactic:
simp [sqrt_normSq_eq_norm]

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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f (Compacts.map (fun x ↦ g * x) ⋯ K) - f K
⊢ chaar K₀ (Compacts.map (fun x ↦ g * x) ⋯ K) = chaar K₀ K

Tactic:
have : Continuous eval := (continuous_apply (K.map _ _)).sub (continuous_apply K)

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f (Compacts.map (fun x ↦ g * x) ⋯ K) - f K
this : Continuous eval
⊢ chaar K₀ (Compacts.map (fun x ↦ g * x) ⋯ K) = chaar K₀ K
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
h : ‖x‖ = 0
⊢ ⟪x, y⟫ = 0

Tactic:
rw [← norm_eq_zero]
  refine le_antisymm ?_ (by positivity)
  exact norm_inner_le_norm _ _ |>.trans <| by simp [h]

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
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ 0 < μ K
⊢ E / E ∈ 𝓝 1

Tactic:
obtain ⟨K, hKE, hK, K_closed, hKpos⟩ : ∃ K ⊆ E, IsCompact K ∧ IsClosed K ∧ 0 < μ K := by
    obtain ⟨K, hKE, hK_comp, hK_meas⟩ := hEapprox
    exact ⟨closure K, hK_comp.closure_subset_measurableSet hE hKE, hK_comp.closure,
      isClosed_closure, by rwa [hK_comp.measure_closure]⟩

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ 0 < μ K
K : Set G
hKE : K ⊆ E
hK : IsCompact K
K_closed : IsClosed[inst✝⁶] K
hKpos : 0 < μ K
⊢ E / E ∈ 𝓝 1
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₁, 0 + 0 - ∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x - v₂ i‖ * ‖v₁ x - v₂ i‖ / 2) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

Tactic:
Finset.sum_const_zero,

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
⊢ 0 + 0 - ∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x - v₂ i‖ * ‖v₁ x - v₂ i‖ / 2) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2
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 - (θ • w + (1 - θ) • v)‖ ^ 2 = ‖u - v - θ • (w - v)‖ ^ 2

Tactic:
have : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v) := by
              rw [smul_sub, sub_smul, one_smul]
              simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev]
            rw [this]

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

Goal state before:
pp: case inr.ha
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ ¬‖x‖ = 0

Tactic:
norm_eq_zero

Goal state after:
case inr.ha
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ ¬x = 0
Module: Mathlib.Analysis.InnerProductSpace.Basic

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

Tactic:
rintro ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩
    exact real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx hr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝ : RCLike 𝕜
x : 𝕜
⊢ ‖x‖ ^ 2 = re ↑(‖x‖ ^ 2)

Tactic:
ofReal_re

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝ : RCLike 𝕜
x : 𝕜
⊢ ‖x‖ ^ 2 = ‖x‖ ^ 2
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
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι →₀ 𝕜
⊢ ⟪(linearCombination 𝕜 v) l₁, (linearCombination 𝕜 v) l₂⟫ = l₂.sum fun i y ↦ (starRingEnd 𝕜) (l₁ i) * y

Tactic:
simp [l₂.linearCombination_apply, Finsupp.inner_sum, hv.inner_left_finsupp, mul_comm,
    inner_smul_right]

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E
y : F
⊢ ((rankOne 𝕜) x) y = 0 ↔ x = 0 ∨ y = 0

Tactic:
simp [ContinuousLinearMap.ext_iff, rankOne_apply, forall_or_right, or_comm,
    ext_iff_inner_right 𝕜 (E := F)]

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

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ‖x‖ ^ 2 ∈ upperBounds (Set.range fun s ↦ ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2)

Tactic:
rintro y ⟨s, rfl⟩

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
s : Finset ι
⊢ (fun s ↦ ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2) s ≤ ‖x‖ ^ 2
Module: Mathlib.Analysis.RCLike.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ Submodule.span ℝ {1, I} = ⊤

Tactic:
suffices ∀ x : K, ∃ a b : ℝ, a • 1 + b • I = x by
    simpa [Submodule.eq_top_iff', Submodule.mem_span_pair]
  exact fun x ↦ ⟨re x, im x, by simp [real_smul_eq_coe_mul]⟩

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
⊢ v ∈ (𝕜 ∙ u)ᗮ ↔ ⟪u, v⟫ = 0

Tactic:
by
  refine ⟨inner_right_of_mem_orthogonal (mem_span_singleton_self u), ?_⟩
  intro hv w hw
  rw [mem_span_singleton] at hw
  obtain ⟨c, rfl⟩ := hw
  simp [inner_smul_left, hv]

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
x : E
⊢ x = 0 → ∀ u ∈ ⊤, ⟪u, x⟫ = 0

Tactic:
by
      rintro rfl
      simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊥.reflection = LinearIsometryEquiv.neg 𝕜

Tactic:
ext; simp [reflection_apply]

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 : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
v : E
⊢ v ∈ U ↔ ‖U.starProjection v‖ = ‖v‖

Tactic:
by
  refine ⟨fun h => norm_starProjection_apply _ h, fun h => ?_⟩
  simpa [h, sub_eq_zero, eq_comm (a := v), starProjection_eq_self_iff] using
    U.norm_sq_eq_add_norm_sq_starProjection v

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

Goal state before:
pp: case top
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : α
hp : Fact (1 ≤ ∞)
⊢ ‖toLp ∞ (x, 0)‖₊ = ‖x‖₊

Tactic:
| top =>

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

Goal state before:
pp: case top
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y : β
hp : Fact (1 ≤ ∞)
⊢ ‖toLp ∞ (0, y)‖₊ = ‖y‖₊

Tactic:
| top =>

Goal state after:
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 α ↔ A * star A = 1

Tactic:
by
  refine ⟨And.right, fun hA => ⟨?_, hA⟩⟩
  simpa only [mul_eq_one_comm] using hA

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case left
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ (if i✝.1 = j✝.1 then if i✝.2 = j✝.2 then 1 else 0 else ∑ x, 0) = if i✝ = j✝ then 1 else 0

Tactic:
Finset.sum_const_zero,

Goal state after:
case left
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ (if i✝.1 = j✝.1 then if i✝.2 = j✝.2 then 1 else 0 else 0) = if i✝ = j✝ then 1 else 0
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case left
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ (if i✝.1 = j✝.1 then if i✝.2 = j✝.2 then 1 else 0 else 0) = if i✝ = j✝ then 1 else 0

Tactic:
← ite_and,

Goal state after:
case left
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ (if i✝.1 = j✝.1 ∧ i✝.2 = j✝.2 then 1 else 0) = if i✝ = j✝ then 1 else 0
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case right
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ (if i✝.2 = j✝.2 then if i✝.1 = j✝.1 then 1 else 0 else ∑ x, 0) = if i✝ = j✝ then 1 else 0

Tactic:
Finset.sum_const_zero,

Goal state after:
case right
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ (if i✝.2 = j✝.2 then if i✝.1 = j✝.1 then 1 else 0 else 0) = if i✝ = j✝ then 1 else 0
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case right
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ (if i✝.2 = j✝.2 then if i✝.1 = j✝.1 then 1 else 0 else 0) = if i✝ = j✝ then 1 else 0

Tactic:
← ite_and,

Goal state after:
case right
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ (if i✝.2 = j✝.2 ∧ i✝.1 = j✝.1 then 1 else 0) = if i✝ = j✝ then 1 else 0
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Ring 𝕜
inst✝³ : IsDomain 𝕜
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module 𝕜 M
inst✝ : IsTorsionFree 𝕜 M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent 𝕜 fun i ↦ single p i (v i)

Tactic:
suffices LinearIndependent 𝕜 ((WithLp.linearEquiv p 𝕜 _).symm.toLinearMap ∘
      fun i : ι ↦ Pi.single i (v i)) by
    simpa

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Ring 𝕜
inst✝³ : IsDomain 𝕜
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module 𝕜 M
inst✝ : IsTorsionFree 𝕜 M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent 𝕜 (⇑↑(WithLp.linearEquiv p 𝕜 (ι → M)).symm ∘ fun i ↦ Pi.single i (v i))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: s : Set ℝ
⊢ volume s = StieltjesFunction.id.measure s

Tactic:
by
  simp [volume_eq_stieltjes_id]

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

Goal state before:
pp: case inl
p : ℝ≥0∞
𝕜 : Type u_1
ι✝ : Type u_2
α✝ : ι✝ → Type u_3
β : ι✝ → Type u_4
hp : Fact (1 ≤ p)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝² : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝¹ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
inst✝ : Fact (1 ≤ ∞)
__LinearEquiv✝ : (PiLp ∞ fun i ↦ α i.fst i.snd) ≃ₗ[𝕜] PiLp ∞ fun i ↦ PiLp ∞ (α i) :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : Sigma κ) → (fun i ↦ α i.fst i.snd) i) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
      LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv ∞ 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
    (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → WithLp ∞ ((j : κ i) → α i j))).symm
⊢ ‖((WithLp.linearEquiv ∞ 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
            LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv ∞ 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
          (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → WithLp ∞ ((j : κ i) → α i j))).symm)
        ((WithLp.addEquiv ∞ ((i : Sigma κ) → α i.fst i.snd)).invFun x)‖₊ =
    ‖(WithLp.addEquiv ∞ ((i : Sigma κ) → α i.fst i.snd)).invFun x‖₊

Tactic:
simp [Pi.nnnorm_def, ← Finset.univ_sigma_univ, Finset.sup_sigma, Sigma.curry]

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

Goal state before:
pp: case top
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ∞)
⊢ ‖single ∞ i b‖₊ = ‖b‖₊

Tactic:
| top =>

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

Goal state before:
pp: ⊢ (Ioo 0 1).Nonempty

Tactic:
nonempty_Ioo,

Goal state after:
⊢ 0 < 1
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
𝕜 : Type u_5
inst✝ : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp p fun x ↦ 𝕜)
A : Matrix ι ι 𝕜
⊢ b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j ↦ (b.repr (toLp p (Aᵀ j))) i

Tactic:
by
  have := basis_toMatrix_basisFun_mul (b.map (WithLp.linearEquiv _ 𝕜 _)) A
  simp_rw [← PiLp.basisFun_map p, Basis.map_repr, LinearEquiv.trans_apply,
    WithLp.linearEquiv_symm_apply, Basis.toMatrix_map, Function.comp_def, Basis.map_apply,
    LinearEquiv.symm_apply_apply] at this
  exact this

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

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁷ : NormedField K
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace K E
b : Basis ι K E
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ = ‖∑ i, (b.repr (fract b m)) i • b i‖

Tactic:
by rw [b.sum_repr]

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
r : ℝ
s : Set E
⊢ μ (r • s) = ENNReal.ofReal |r ^ finrank ℝ E| * μ s

Tactic:
rcases ne_or_eq r 0 with (h | rfl)
  · rw [← preimage_smul_inv₀ h, addHaar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv]
  rcases eq_empty_or_nonempty s with (rfl | hs)
  · simp only [measure_empty, mul_zero, smul_set_empty]
  rw [zero_smul_set hs, ← singleton_zero]
  by_cases h : finrank ℝ E = 0
  · have : Subsingleton E := finrank_zero_iff.1 h
    simp only [h, one_mul, ENNReal.ofReal_one, abs_one, Subsingleton.eq_univ_of_nonempty hs,
      pow_zero, Subsingleton.eq_univ_of_nonempty (singleton_nonempty (0 : E))]
  · have : Nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h)
    simp only [h, zero_mul, ENNReal.ofReal_zero, abs_zero, Ne, not_false_iff,
      zero_pow, measure_singleton]

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
⊢ Tendsto (fun r ↦ ENNReal.ofReal (r ^ finrank ℝ E)) (𝓝[<] 1) (𝓝 (ENNReal.ofReal (1 ^ finrank ℝ E)))

Tactic:
exact ENNReal.tendsto_ofReal ((tendsto_id'.2 nhdsWithin_le_nhds).pow _)

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ Box.Icc J₂
H : {i | J₁.lower i = x i} = {i | J₂.lower i = x i}
this : ∀ (i : ι), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
⊢ J₁ = J₂

Tactic:
choose y hy₁ hy₂ using this
    exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂

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

Goal state before:
pp: case mpr
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : ∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J ∈ π₁, x ∈ J) → ∃ J ∈ π₂, x ∈ J
⊢ ∃ I' ∈ π₂, J ≤ I'

Tactic:
rcases HU J.upper ⟨J, hJ, J.upper_mem⟩ with ⟨J₂, hJ₂, hx⟩

Goal state after:
case mpr
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : ∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J ∈ π₁, x ∈ J) → ∃ J ∈ π₂, x ∈ J
J₂ : Box ι
hJ₂ : J₂ ∈ π₂
hx : J.upper ∈ J₂
⊢ ∃ I' ∈ π₂, J ≤ I'
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
H : Disjoint π₁.iUnion π₂.iUnion
⊢ J ∈ π₁.disjUnion π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂

Tactic:
by
  classical exact Finset.mem_union

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
w : PiLp 2 fun i ↦ ↥(V i)
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
⊢ (hV.isometryL2OfOrthogonalFamily hV').symm w = ∑ i, ↑(w.ofLp i)

Tactic:
suffices ∀ v : ⨁ i, V i, e₂ v = ∑ i, e₁ v i by exact this (e₁.symm w)

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
w : PiLp 2 fun i ↦ ↥(V i)
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
⊢ ∀ (v : ⨁ (i : ι), ↥(V i)), e₂ v = ∑ i, ↑(e₁ v i)