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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x ↦ Real.exp (f x)) μ
⊢ 0 < μ (Function.support fun x ↦ Real.exp (f x))

Tactic:
suffices (Function.support fun x ↦ Real.exp (f x)) = Set.univ by simp [this, hμ.out]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x ↦ Real.exp (f x)) μ
⊢ (Function.support fun x ↦ Real.exp (f x)) = univ
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace P
inst✝² : AddTorsor V P
s t : AffineSubspace R P
inst✝¹ : Nonempty ↥s
inst✝ : Nonempty ↥t
h : s = t
⊢ Continuous (AffineEquiv.ofEq s t h).toFun

Tactic:
by subst h; exact continuous_id

Goal state after:
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace P
inst✝² : AddTorsor V P
s t : AffineSubspace R P
inst✝¹ : Nonempty ↥s
inst✝ : Nonempty ↥t
h : s = t
⊢ Continuous (AffineEquiv.ofEq s t h).invFun

Tactic:
by subst h; exact continuous_id

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst✝⁶ : NormedAddCommGroup G'
inst✝⁵ : PartialOrder G'
inst✝⁴ : IsOrderedAddMonoid G'
inst✝³ : NormedSpace ℝ G'
inst✝² : NormedAddCommGroup G''
inst✝¹ : PartialOrder G''
inst✝ : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x
f : ↥(α →₁ₛ[μ] G'')
hf : 0 ≤ f
f' : SimpleFunc α G''
hf' : 0 ≤ f'
hff' : ↑↑↑f =ᵐ[μ] ⇑f'
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
replace hff' : simpleFunc.toSimpleFunc f =ᵐ[μ] f' :=
    (Lp.simpleFunc.toSimpleFunc_eq_toFun f).trans hff'

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst✝⁶ : NormedAddCommGroup G'
inst✝⁵ : PartialOrder G'
inst✝⁴ : IsOrderedAddMonoid G'
inst✝³ : NormedSpace ℝ G'
inst✝² : NormedAddCommGroup G''
inst✝¹ : PartialOrder G''
inst✝ : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x
f : ↥(α →₁ₛ[μ] G'')
hf : 0 ≤ f
f' : SimpleFunc α G''
hf' : 0 ≤ f'
hff' : ⇑(toSimpleFunc f) =ᵐ[μ] ⇑f'
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
⊢ ‖c‖ / R < 1

Tactic:
div_lt_iff₀ Rpos

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
⊢ ‖c‖ < 1 * R
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case indicatorConst
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝⁵ : NormedAddCommGroup G''
inst✝⁴ : PartialOrder G''
inst✝³ : IsOrderedAddMonoid G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : CompleteSpace G''
inst✝ : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ (setToL1 hT) ↑(indicatorConst 1 hs ⋯ c) ≤ (setToL1 hT') ↑(indicatorConst 1 hs ⋯ c)

Tactic:
setToL1_simpleFunc_indicatorConst hT hs hμs,

Goal state after:
case indicatorConst
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝⁵ : NormedAddCommGroup G''
inst✝⁴ : PartialOrder G''
inst✝³ : IsOrderedAddMonoid G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : CompleteSpace G''
inst✝ : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ (T s) c ≤ (setToL1 hT') ↑(indicatorConst 1 hs ⋯ c)
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace R
inst✝¹ : Zero R
inst✝ : DecidableEq l
A : X → (i : l) → Matrix (m' i) (n' i) R
hA : Continuous A
x✝¹ : (i : l) × m' i
x✝ : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
⊢ Continuous fun a ↦ blockDiagonal' (A a) ⟨i₁, i₂⟩ ⟨j₁, j₂⟩

Tactic:
dsimp only [blockDiagonal'_apply']

Goal state after:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace R
inst✝¹ : Zero R
inst✝ : DecidableEq l
A : X → (i : l) → Matrix (m' i) (n' i) R
hA : Continuous A
x✝¹ : (i : l) × m' i
x✝ : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
⊢ Continuous fun a ↦ if h : i₁ = j₁ then A a i₁ i₂ (cast ⋯ j₂) else 0
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ENNReal.ofReal (∫ (x : X), ‖f x‖ ∂μ i)

Tactic:
rw [ofReal_integral_eq_lintegral_ofReal (hf i).norm]

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ∫⁻ (x : X), ENNReal.ofReal ‖f x‖ ∂μ i

ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
⊢ 0 ≤ᵐ[μ i] fun a ↦ ‖f a‖
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝² : Countable ι
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
inst✝ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
hc : ∀ (i : ι), c i ≠ ∞
h : Summable fun i ↦ (c i).toReal * ‖f (x i)‖
⊢ Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂c i • Measure.dirac (x i)

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Topology.Algebra.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∉ frontier s
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
rw [← Set.mem_compl_iff, compl_frontier_eq_union_interior] at hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∈ interior s ∪ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᵐ[μ] g
hF : CompleteSpace F
hfi : ¬Integrable f μ
hgi : ¬Integrable g μ
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
rw [setToFun_undef hT hfi, setToFun_undef hT hgi]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} = ↑(sInf {C | ∀ (x : α), nndist (f x) (g x) ≤ C})

Tactic:
val_eq_coe,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} = ↑(sInf {C | ∀ (x : α), nndist (f x) (g x) ≤ C})
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ ⨆ x, dist (f x) (g x) = ↑(⨆ x, nndist (f x) (g x))

Tactic:
val_eq_coe,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ ⨆ x, dist (f x) (g x) = ↑(⨆ x, nndist (f x) (g x))
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
x : α
⊢ ENNReal.ofReal (‖f x‖ ^ p) = ‖f x‖ₑ ^ p

Tactic:
rw [← ofReal_norm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.nonneg]

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:
val_eq_coe,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ⨆ x, ‖f x‖ = ↑(⨆ x, ‖f x‖₊)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ IsCompact (closedBall 0 (‖c‖ ^ n * r))

Tactic:
have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
⊢ IsCompact (closedBall 0 (‖c‖ ^ n * r))
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
x : α
hx : ∑' (i : ι), ‖f i x‖ₑ < ∞
⊢ Summable fun n ↦ ↑‖f n x‖₊

Tactic:
rw [← ENNReal.tsum_coe_ne_top_iff_summable_coe]

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
x : α
hx : ∑' (i : ι), ‖f i x‖ₑ < ∞
⊢ ∑' (a : ι), ↑‖f a x‖₊ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case neg
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)
⊢ ∫ (x : X) in t, f x ∂μ = 0

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)
⊢ ∫ (x : X) in t, f x ∂μ = 0

Tactic:
· rw [integral_undef]
    contrapose hf
    exact hf.1

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)
⊢ ∫ (x : X) in t, f x ∂μ = 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 : Compacts G
V : Set G
hV : (interior V).Nonempty
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V

Tactic:
obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V
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 z : F
⊢ (starRingEnd 𝕜) ⟪y, x⟫ + (starRingEnd 𝕜) ⟪z, x⟫ = ⟪x, y⟫ + ⟪x, z⟫

Tactic:
simp only [inner_conj_symm]

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 : F
⊢ ↑(re ⟪x, x⟫) = ⟪x, x⟫

Tactic:
norm_num [ext_iff, inner_self_im]

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 z : E
⊢ (starRingEnd 𝕜) ⟪y, x⟫ + (starRingEnd 𝕜) ⟪z, x⟫ = ⟪x, y⟫ + ⟪x, z⟫

Tactic:
simp only [inner_conj_symm]

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
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ (starRingEnd 𝕜) ((algebraMap 𝕝 𝕜) r) * ⟪x, y⟫ = (starRingEnd 𝕝) r • ⟪x, y⟫

Tactic:
starRingEnd_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ star ((algebraMap 𝕝 𝕜) r) * ⟪x, y⟫ = (starRingEnd 𝕝) r • ⟪x, 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
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ star ((algebraMap 𝕝 𝕜) r) * ⟪x, y⟫ = (starRingEnd 𝕝) r • ⟪x, y⟫

Tactic:
starRingEnd_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ star ((algebraMap 𝕝 𝕜) r) * ⟪x, y⟫ = star r • ⟪x, 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
𝕝 : Type u_4
inst✝⁶ : CommSemiring 𝕝
inst✝⁵ : StarRing 𝕝
inst✝⁴ : Algebra 𝕝 𝕜
inst✝³ : Module 𝕝 E
inst✝² : IsScalarTower 𝕝 𝕜 E
inst✝¹ : StarModule 𝕝 𝕜
inst✝ : TrivialStar 𝕝
x y : E
r : 𝕝
⊢ (starRingEnd 𝕝) r • ⟪x, y⟫ = r • ⟪x, y⟫

Tactic:
starRingEnd_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst✝⁶ : CommSemiring 𝕝
inst✝⁵ : StarRing 𝕝
inst✝⁴ : Algebra 𝕝 𝕜
inst✝³ : Module 𝕝 E
inst✝² : IsScalarTower 𝕝 𝕜 E
inst✝¹ : StarModule 𝕝 𝕜
inst✝ : TrivialStar 𝕝
x y : E
r : 𝕝
⊢ star r • ⟪x, y⟫ = r • ⟪x, 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
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ (starRingEnd 𝕜) ((starRingEnd 𝕝) r • ⟪y, x⟫) = r • ⟪x, y⟫

Tactic:
starRingEnd_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ star ((starRingEnd 𝕝) r • ⟪y, x⟫) = r • ⟪x, 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
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ star ((starRingEnd 𝕝) r • ⟪y, x⟫) = r • ⟪x, y⟫

Tactic:
starRingEnd_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ star (star r • ⟪y, x⟫) = r • ⟪x, 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 : E
⊢ re ⟪x, x⟫ = ‖x‖ ^ 2

Tactic:
rw [pow_two, inner_self_eq_norm_mul_norm]

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
h : re ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
⊢ ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖

Tactic:
simpa using h

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_ℝ + ‖y‖ ^ 2
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2

Tactic:
simpa using h

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Tactic:
simpa using h

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Tactic:
simpa using h

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / (↑‖x‖ * ↑‖y‖)‖ = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ ‖⟪x, y⟫‖ / (‖x‖ * ‖y‖) = 1

Tactic:
simpa using h

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

Goal state before:
pp: case e_f
𝕜 : 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
l₁ l₂ : (i : ι) → G i
s : Finset ι
i : ι
⊢ ∑ i_1 ∈ s, ⟪(V i_1) (l₁ i_1), (V i) (l₂ i)⟫ = ∑ i_1 ∈ s, if i_1 = i then ⟪(V i_1) (l₁ i_1), (V i) (l₂ i)⟫ else 0

Tactic:
congr with j

Goal state after:
case e_f.e_f
𝕜 : 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
l₁ l₂ : (i : ι) → G i
s : Finset ι
i j : ι
⊢ ⟪(V j) (l₁ j), (V i) (l₂ i)⟫ = if j = i then ⟪(V j) (l₁ j), (V i) (l₂ i)⟫ else 0
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set (Set E)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, Orthonormal 𝕜 fun x ↦ ↑x
⊢ ∀ (i : ↑s), Orthonormal 𝕜 fun x ↦ ↑x

Tactic:
simpa using h

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : ↥K
⊢ K.orthogonalProjectionOnto ↑v = v

Tactic:
by
  ext
  apply eq_starProjection_of_mem_of_inner_eq_zero <;> simp

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

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : p ≠ ∞
x y : WithLp p (α × β)
⊢ ↑(nndist x y) = ↑((nndist x.fst y.fst ^ p.toReal + nndist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal))

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

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 α)
x : n → α
⊢ (toLin' (A⁻¹ * A)) x = x

Tactic:
by rw [inv_mul_cancel, toLin'_one, id_apply]

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

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

Tactic:
by rw [← measure_congr Iio_ae_eq_Iic]; simp

Goal state after:
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 ((toLin' t.toMatrix) a) ∂volume =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i ↦ volume

Tactic:
volume_pi

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) ∂Measure.pi fun x ↦ volume) =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i ↦ volume
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
i : ι
⊢ x i = ((fun i ↦ x i / a i) • a) i

Tactic:
· specialize h i
      simp only [smul_eq_mul, Pi.mul_apply]
      rcases eq_or_ne (a i) 0 with hai | hai
      · rw [hai, inf_idem, sup_idem, ← le_antisymm_iff] at h
        rw [hai, ← h, zero_div, zero_mul]
      · rw [div_mul_cancel₀ _ hai]

Goal state after: