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
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ ∀ᵐ (x : X) ∂μ.restrict s, f x ≤ g x

Tactic:
ae_restrict_iff' hs

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x
⊢ ∀ᵐ (x : X) ∂μ.restrict s, 0 x ≤ f x

Tactic:
ae_restrict_iff' hs

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → 0 x ≤ f x
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0
⊢ ∀ᵐ (x : X) ∂μ.restrict s, f x ≤ 0 x

Tactic:
ae_restrict_iff' hs

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0 x
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ ∫ (x : X), {a | f a ≤ 0}.indicator f x ∂μ ≤ ∫ (x : X), s.indicator f x ∂μ

Tactic:
exact
    integral_mono (hfi.indicator (hf.measurableSet_le stronglyMeasurable_const))
      (hfi.indicator hs) (indicator_nonpos_le_indicator s f)

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

Tactic:
rw [← inner_conj_symm, mul_comm]
  exact re_eq_norm_of_mul_conj ⟪y, x⟫

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 : E
⊢ ↑(re ⟪x, x⟫) = ↑‖x‖ ^ 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
x : E
⊢ ↑(‖x‖ ^ 2) = ↑‖x‖ ^ 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
c : PreInnerProductSpace.Core 𝕜 F
r : 𝕜
x : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case hx
𝕜 : 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
⊢ 0 ≤ ‖r‖ ^ 2

Tactic:
← ofReal_normSq_eq_inner_self,

Goal state after:
𝕜 : 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) * √(re ↑(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
c : PreInnerProductSpace.Core 𝕜 F
r : 𝕜
x : F
⊢ 0 ≤ ‖r‖ ^ 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⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖

Tactic:
rw [← inner_conj_symm, mul_comm]
  exact re_eq_norm_of_mul_conj ⟪y, x⟫

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✝³ : 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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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_normSq_eq_inner_self,

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) * √(re ↑(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.Basic

Goal state before:
pp: case convert_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
j : ι
_hj : j ∈ s
⊢ j ≠ i → ⟪v i, g j • v j⟫ = 0

Tactic:
hji

Goal state after:
case convert_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
j : ι
_hj : j ∈ s
hji : j ≠ i
⊢ ⟪v i, g j • v j⟫ = 0
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
K₁ K₂ : Compacts G
h : Disjoint ↑K₁ ↑K₂
_h₁ : IsClosed[inst✝¹] ↑K₁
h₂ : IsClosed[inst✝¹] ↑K₂
⊢ ⟨chaar K₀ (K₁ ⊔ K₂), ⋯⟩ = ⟨chaar K₀ K₁, ⋯⟩ + ⟨chaar K₀ K₂, ⋯⟩

Tactic:
simp only [chaar_sup_eq h]; rfl

Goal state after:
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)
this : 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ = 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖)
⊢ δ ≤ ‖u - half • (wq + wp)‖

Tactic:
rw [smul_add]

Goal state after:
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)
this : 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ = 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖)
⊢ δ ≤ ‖u - (half • wq + half • wp)‖
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, y⟫ = 0
⊢ re ⟪x, y⟫ = 0

Tactic:
simp only [h, zero_re]

Goal state after:
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_1‖ * (‖v₁ x - v₂ x_1‖ / 2))) =
    -∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * w₂ x_1 * (‖v₁ x - v₂ x_1‖ * (‖v₁ x - v₂ x_1‖ / 2))

Tactic:
mul_assoc

Goal state after:
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
⊢ ⟪∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

Tactic:
by
  simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
    real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, ← div_sub_div_same,
    add_div, mul_sub_left_distrib, left_distrib, Finset.sum_sub_distrib,
    Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul, h₁, h₂, zero_mul,
    mul_zero, Finset.sum_const_zero, zero_add, zero_sub, Finset.mul_sum, neg_div,
    Finset.sum_div, mul_div_assoc, mul_assoc]

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‖)‖ = 1 ↔ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x

Tactic:
by
  constructor
  · intro h
    have hx₀ : x ≠ 0 := fun h₀ => by simp [h₀] at h
    have hy₀ : y ≠ 0 := fun h₀ => by simp [h₀] at h
    refine ⟨hx₀, (norm_inner_eq_norm_iff hx₀ hy₀).1 <| eq_of_div_eq_one ?_⟩
    simpa using h
  · rintro ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩
    simp only [norm_div, norm_mul, norm_ofReal, abs_norm]
    exact norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr

Goal state after:
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 + (v - θ • v)) = u - v - (θ • w - θ • v)

Tactic:
simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev]

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
x : E
h : ‖T x‖⁻¹ * re ⟪T x, T x⟫_𝕜 ≤ C
hx : ‖x‖ = 1
hTx : ¬‖T x‖ = 0
⊢ ‖T x‖ ≤ C

Tactic:
← norm_sq_eq_re_inner,

Goal state after:
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
x : E
h : ‖T x‖⁻¹ * ‖T x‖ ^ 2 ≤ C
hx : ‖x‖ = 1
hTx : ¬‖T x‖ = 0
⊢ ‖T x‖ ≤ C
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ 1 / 2 * ‖h^[n] y‖ ≤ 1 / 2 * (1 / 2) ^ n * ‖y‖

Tactic:
mul_assoc

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ 1 / 2 * ‖h^[n] y‖ ≤ 1 / 2 * ((1 / 2) ^ n * ‖y‖)
Module: Mathlib.Analysis.Normed.Operator.Banach

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

Tactic:
mul_assoc

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
⊢ 2 * (C * ‖y‖) = 2 * (C * ‖y‖)
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_1
𝕜 : 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
a : E
ha' : a ∈ insert e v
⊢ ‖↑⟨a, ha'⟩‖ = 1

Tactic:
rcases eq_or_mem_of_mem_insert ha' with ha | ha

Goal state after:
case mp.refine_1.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
a : E
ha' : a ∈ insert e v
ha : a = e
⊢ ‖↑⟨a, ha'⟩‖ = 1

case mp.refine_1.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
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ‖↑⟨a, ha'⟩‖ = 1
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_2
𝕜 : 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
⊢ ∀ ⦃j : { x // x ∈ insert e v }⦄, ⟨a, ha'⟩ ≠ j → (fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0) ⟨a, ha'⟩ j

Tactic:
rcases eq_or_mem_of_mem_insert ha' with ha | ha

Goal state after:
case mp.refine_2.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 = e
⊢ ∀ ⦃j : { x // x ∈ insert e v }⦄, ⟨a, ha'⟩ ≠ j → (fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0) ⟨a, ha'⟩ j

case mp.refine_2.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
⊢ ∀ ⦃j : { x // x ∈ insert e v }⦄, ⟨a, ha'⟩ ≠ j → (fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0) ⟨a, ha'⟩ j
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : Norm α
inst✝ : Norm β
n : ℕ
h : p = ↑n
f : WithLp p (α × β)
this : 0 < p.toReal
⊢ ‖f‖ = (‖f.fst‖ ^ n + ‖f.snd‖ ^ n) ^ (1 / ↑n)

Tactic:
simp only [one_div, h, Real.rpow_natCast, ENNReal.toReal_natCast,
    prod_norm_eq_add this]

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
⊢ ∑ y, ∑ x, star U₂ i✝.2 y * (star U₁ i✝.1 x * U₁ x j✝.1) * U₂ y j✝.2 = 1 i✝ j✝

Tactic:
simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ← Matrix.mul_apply, hU₁.1, Matrix.one_apply,
      mul_boole, ite_mul, zero_mul, Finset.sum_ite_irrel, ← Matrix.mul_apply, hU₂.1,
      Matrix.one_apply, Finset.sum_const_zero, ← ite_and, Prod.eq_iff_fst_eq_snd_eq]

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

Goal state before:
pp: this : StieltjesFunction.id.measure.IsAddLeftInvariant
A : StieltjesFunction.id.measure ↑(stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1
⊢ volume = 1 • addHaarMeasure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped

Tactic:
simp only [volume, Module.Basis.addHaar, one_smul]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
⊢ ofReal |(Matrix.diagonal D).det| • Measure.map (⇑(toLin' (Matrix.diagonal D))) volume = volume

Tactic:
by
  refine (Measure.pi_eq fun s hs => ?_).symm
  simp only [det_diagonal, Measure.coe_smul, smul_eq_mul, Pi.smul_apply]
  rw [Measure.map_apply _ (MeasurableSet.univ_pi hs)]
  swap; · exact Continuous.measurable (LinearMap.continuous_on_pi _)
  have :
    (Matrix.toLin' (diagonal D) ⁻¹' Set.pi Set.univ fun i : ι => s i) =
      Set.pi Set.univ fun i : ι => (D i * ·) ⁻¹' s i := by
    ext f
    simp only [LinearMap.coe_proj, smul_eq_mul, LinearMap.smul_apply, mem_univ_pi,
      mem_preimage, LinearMap.pi_apply, diagonal_toLin']
  have B : ∀ i, ofReal (abs (D i)) * volume ((D i * ·) ⁻¹' s i) = volume (s i) := by
    intro i
    have A : D i ≠ 0 := by
      simp only [det_diagonal, Ne] at h
      exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)
    rw [volume_preimage_mul_left A, ← mul_assoc, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul,
      mul_inv_cancel₀ A, abs_one, ENNReal.ofReal_one, one_mul]
  rw [this, volume_pi_pi, Finset.abs_prod,
    ENNReal.ofReal_prod_of_nonneg fun i _ => abs_nonneg (D i), ← Finset.prod_mul_distrib]
  simp only [B]

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

Goal state before:
pp: case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
j : ι
hij : j ≠ i
⊢ ‖(single (↑p) i b).ofLp j‖₊ ^ ↑p = 0

Tactic:
single_eq_of_ne _ hij,

Goal state after:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
j : ι
hij : j ≠ i
⊢ ‖0‖₊ ^ ↑p = 0
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case intro
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✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
⊢ ‖x‖ ≤ ∑ j, ‖b j‖

Tactic:
rw [← fract_eq_self.mpr hx]

Goal state after:
case intro
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✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
⊢ ‖fract b x‖ ≤ ∑ j, ‖b j‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case left
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
this✝ : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
this : μ.restrict (s \ u) = 0
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x

Tactic:
simp only [this, ae_zero, eventually_bot]

Goal state after: