mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
⊢ ∃ C > 0, ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M

Tactic:
obtain ⟨C, hC, h⟩ := v.exists_opNNNorm_le (F := F)
  refine ⟨C, hC, ?_⟩
  intro u M hM H
  simpa using! h ⟨M, hM⟩ H

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ⨆ x, ‖f x‖ = ↑(⨆ x, ‖f x‖₊)

Tactic:
simp_rw [val_eq_coe, NNReal.coe_iSup, coe_nnnorm]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i ↦ ‖restrict (↑K) (F i)‖
K : Compacts X
A : ∀ (s : Finset ι), restrict (↑K) (∑ i ∈ s, F i) = ∑ i ∈ s, restrict (↑K) (F i)
⊢ ∃ f, Filter.Tendsto (fun i ↦ restrict (↑K) (∑ b ∈ i, F b)) (SummationFilter.unconditional ι).filter (nhds f)

Tactic:
simpa only [HasSum, A] using! (hF K).of_norm

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

Goal state before:
pp: case pos.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
⊢ 0 ≤ᵐ[μ] -f

Tactic:
filter_upwards [hf] with ω hω
      rwa [Pi.zero_apply, Pi.neg_apply, Right.nonneg_neg_iff]

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : ¬infEDist y E * (↑δ.toNNReal)⁻¹ ≤ 1
⊢ 1 ≤ (↑δ.toNNReal)⁻¹ * edist x y + (1 - infEDist y E * (↑δ.toNNReal)⁻¹) + infEDist x E * (↑δ.toNNReal)⁻¹

Tactic:
rw [tsub_eq_zero_of_le (not_le.mp h_le).le, add_zero, mul_comm]

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : ¬infEDist y E * (↑δ.toNNReal)⁻¹ ≤ 1
⊢ 1 ≤ edist x y * (↑δ.toNNReal)⁻¹ + infEDist x E * (↑δ.toNNReal)⁻¹
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst✝⁴] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
⊢ ∀ᶠ (x : α) in 𝓝 a, f x ∈ s

Tactic:
filter_upwards [Ici_mem_nhds ha] with y hy using (hu y hy).2

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

Goal state before:
pp: case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
this : ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ = 0
⊢ ∫ (x : X) in t, f x ∂μ = 0

Tactic:
rw [← this]

Goal state after:
case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
this : ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ = 0
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : R1Space G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
h : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun x ↦ g * x) ⋯ K) = μ K
g : G
A : Set G
⊢ μ.outerMeasure ((fun x ↦ g * x) ⁻¹' A) = μ.outerMeasure A

Tactic:
by
  convert! μ.outerMeasure_preimage (Homeomorph.mulLeft g) (fun K => h g) A

Goal state after:
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
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
by_cases h : IntegrableOn f t μ; swap
  · have : ¬IntegrableOn f s μ := fun H => h (H.of_ae_sdiff_eq_zero ht h't)
    rw [integral_undef h, integral_undef this]
  let f' := h.1.mk f
  calc
    ∫ x in t, f x ∂μ = ∫ x in t, f' x ∂μ := integral_congr_ae h.1.ae_eq_mk
    _ = ∫ x in s, f' x ∂μ := by
      apply
        setIntegral_eq_of_subset_of_ae_sdiff_eq_zero_aux hts _ h.1.stronglyMeasurable_mk
          (h.congr h.1.ae_eq_mk)
      filter_upwards [h't, ae_imp_of_ae_restrict h.1.ae_eq_mk] with x hx h'x h''x
      rw [← h'x h''x.1, hx h''x]
    _ = ∫ x in s, f x ∂μ := by
      apply integral_congr_ae
      apply ae_restrict_of_ae_restrict_of_subset hts
      exact h.1.ae_eq_mk.symm

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 - ↑f ⊥) = ofReal (↑f x - l)

Tactic:
tendsto_nhds_unique hf (tendsto_pure_nhds f ⊥)

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 - ↑f ⊥)
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
C : ℝ
h : ∀ (x : R), |↑f x| ≤ C
h✝ : Nonempty R
u : ℝ
hu : Tendsto (↑f) atTop (𝓝 u)
H : Tendsto (↑f) atBot atBot
⊢ ∃ l, Tendsto (↑f) atBot (𝓝 l)

Tactic:
obtain ⟨x, hx⟩ : ∃ x, f x ≤ - C - 1 := (tendsto_atBot.1 H (-C - 1)).exists

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
C : ℝ
h : ∀ (x : R), |↑f x| ≤ C
h✝ : Nonempty R
u : ℝ
hu : Tendsto (↑f) atTop (𝓝 u)
H : Tendsto (↑f) atBot atBot
x : R
hx : ↑f x ≤ -C - 1
⊢ ∃ l, Tendsto (↑f) atBot (𝓝 l)
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
this : Classical.choose ⋯ ∈ ⋂ V, clPrehaar (↑K₀) V
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V

Tactic:
rw [mem_iInter] at this

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
this : ∀ (i : OpenNhdsOf 1), Classical.choose ⋯ ∈ clPrehaar (↑K₀) i
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V
Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: case pos
𝕜 : 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⟩
⊢ ⟪(fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, v⟩, (fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, w⟩⟫ = 0

Tactic:
have : v ≠ w := fun h => by
      subst h
      exact hvw rfl

Goal state after:
case pos
𝕜 : 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⟩
this : v ≠ w
⊢ ⟪(fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, v⟩, (fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, w⟩⟫ = 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
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∑' (i : ι), ‖⟪v i, x⟫‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
refine tsum_le_of_sum_le' ?_ fun s => hv.sum_inner_products_le x

Goal state after:
𝕜 : 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
⊢ 0 ≤ ‖x‖ ^ 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
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ⊆ m → ∀ (n : Finset ι), a ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ⊆ s₁
s₂ : Finset ι
hs₂ : a ⊆ s₂
has : a ⊆ s₁ ⊓ s₂
this : s₁ ⊓ s₂ ⊆ s₁
⊢ ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 = |∑ i ∈ s₁, ‖f i‖ ^ 2 - ∑ i ∈ s₁ ⊓ s₂, ‖f i‖ ^ 2|

Tactic:
← Finset.sum_sdiff this,

Goal state after:
𝕜 : 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✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ⊆ m → ∀ (n : Finset ι), a ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ⊆ s₁
s₂ : Finset ι
hs₂ : a ⊆ s₂
has : a ⊆ s₁ ⊓ s₂
this : s₁ ⊓ s₂ ⊆ s₁
⊢ ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 = |∑ x ∈ s₁ \ (s₁ ⊓ s₂), ‖f x‖ ^ 2 + ∑ x ∈ s₁ ⊓ s₂, ‖f x‖ ^ 2 - ∑ i ∈ s₁ ⊓ s₂, ‖f i‖ ^ 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
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ⊆ m → ∀ (n : Finset ι), a ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ⊆ s₁
s₂ : Finset ι
hs₂ : a ⊆ s₂
has : a ⊆ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 = |∑ i ∈ s₂, ‖f i‖ ^ 2 - ∑ i ∈ s₁ ⊓ s₂, ‖f i‖ ^ 2|

Tactic:
← Finset.sum_sdiff this,

Goal state after:
𝕜 : 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✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ⊆ m → ∀ (n : Finset ι), a ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ⊆ s₁
s₂ : Finset ι
hs₂ : a ⊆ s₂
has : a ⊆ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 = |∑ x ∈ s₂ \ (s₁ ⊓ s₂), ‖f x‖ ^ 2 + ∑ x ∈ s₁ ⊓ s₂, ‖f x‖ ^ 2 - ∑ i ∈ s₁ ⊓ s₂, ‖f i‖ ^ 2|
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    ((starRingEnd ℂ) ⟪T (x + y), x + y⟫_ℂ - (starRingEnd ℂ) ⟪T (x - y), x - y⟫_ℂ +
          (starRingEnd ℂ) ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I -
        (starRingEnd ℂ) ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I) /
      (starRingEnd ℂ) 4

Tactic:
rw [h (x + y), h (x - y), h (x + Complex.I • y), h (x - Complex.I • y)]

Goal state after:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ +
          ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I -
        ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I) /
      (starRingEnd ℂ) 4
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : ¬FiniteDimensional 𝕜 ↥Kᗮ
⊢ LinearMap.det ↑K.reflection.toLinearEquiv = 1

Tactic:
LinearMap.det_eq_one_of_finrank_eq_zero

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : ¬FiniteDimensional 𝕜 ↥Kᗮ
⊢ 1 = 1

case neg.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : ¬FiniteDimensional 𝕜 ↥Kᗮ
⊢ finrank 𝕜 E = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

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

Tactic:
rw [← this]

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : ¬finrank ℝ ↥Wᗮ ≤ n
this✝ : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
H₂V : W ≤ V
this : ρ ↑v = φ ↑v
⊢ ρ (ρ ↑v) = ↑v
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ edist x y = edist x.fst y.fst + edist x.snd y.snd

Tactic:
by
  simp [prod_edist_eq_add]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ edist x y = (edist x.fst y.fst ^ 2 + edist x.snd y.snd ^ 2) ^ (1 / 2)

Tactic:
by
  simp [prod_edist_eq_add]

Goal state after:
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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : f (x + w) = z
⊢ z ∈ ⇑f '' s

Tactic:
rw [← this]

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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : f (x + w) = z
⊢ f (x + w) ∈ ⇑f '' s
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
⊢ (single p i a).ofLp i' = 0

Tactic:
by
  rw [ofLp_single, Pi.single_eq_of_ne h]

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

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal

Tactic:
smul_fst,

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖c • f.fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
have : 0 < p.toReal := by rw [ENNReal.toReal_pos_iff_ne_top]; rintro rfl; norm_num at h
      simp only [edist_eq_sum, edist_dist, dist_eq_sum, this]
      rw [← ENNReal.ofReal_rpow_of_nonneg (by simp [Finset.sum_nonneg, Real.rpow_nonneg]) (by simp)]
      simp [Real.rpow_nonneg, ENNReal.ofReal_sum_of_nonneg, ← ENNReal.ofReal_rpow_of_nonneg]

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

Goal state before:
pp: a : ℝ
⊢ volume (Iic a) = ∞

Tactic:
← measure_congr Iio_ae_eq_Iic

Goal state after:
a : ℝ
⊢ volume (Iio a) = ∞
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.map (⇑(toLin' t.toMatrix)) volume =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i ↦ volume

Tactic:
lintegral_map (measurable_one.indicator h2s) ht,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) a) ∂volume =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i ↦ volume
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case mk
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
x : ι → ℝ
t_i t_j : ι
t_hij : t_i ≠ t_j
t_c : ℝ
ht : Measurable ⇑(toLin' { i := t_i, j := t_j, hij := t_hij, c := t_c }.toMatrix)
⊢ ∫⁻ (xᵢ : ℝ),
      (univ.pi s).indicator 1
        ((toLin' { i := t_i, j := t_j, hij := t_hij, c := t_c }.toMatrix)
          (Function.update x { i := t_i, j := t_j, hij := t_hij, c := t_c }.i xᵢ)) =
    ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 (Function.update x { i := t_i, j := t_j, hij := t_hij, c := t_c }.i xᵢ)

Tactic:
| mk t_i t_j t_hij t_c =>

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
e : ι ≃ ι'
⊢ (b.reindex e).addHaar = b.addHaar

Tactic:
Basis.addHaar,

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
e : ι ≃ ι'
⊢ addHaarMeasure (b.reindex e).parallelepiped = b.addHaar
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
⊢ addHaarMeasure (piIcc01 ι) = volume ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)

Tactic:
simp only [piIcc01, volume_pi_pi fun _ => Icc (0 : ℝ) 1, PositiveCompacts.coe_mk,
    Compacts.coe_mk, Finset.prod_const_one, ENNReal.ofReal_one, Real.volume_Icc, one_smul, sub_zero]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ Measure.map (⇑(toLin' M)) volume = ofReal |M.det⁻¹| • volume

Tactic:
apply map_matrix_volume_pi_eq_smul_volume_pi

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := ⋯
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ M.det ≠ 0