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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
⊢ IsClosed {q | ⋯.extend (⇑f) (q.1 + q.2) = ⋯.extend (⇑f) q.1 + ⋯.extend (⇑f) q.2}

Tactic:
exact isClosed_eq (cont.comp continuous_add)
          ((cont.comp continuous_fst).add (cont.comp continuous_snd))

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

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ μ.real (⇑f ⁻¹' {y} ∩ s) • y = (μ.restrict s).real (⇑f ⁻¹' {y}) • y

pp: case refine_2.ht
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ 0 ∉ {y}

Tactic:
measureReal_restrict_apply (f.measurableSet_preimage _)

Goal state after:
case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ μ.real (⇑f ⁻¹' {y} ∩ s) • y = μ.real (⇑f ⁻¹' {y} ∩ s) • y

case refine_2.ht
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ 0 ∉ {y}
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
c : ℝ
f : α →ₛ F
⊢ setToSimpleFunc (fun s ↦ c • T s) f = c • setToSimpleFunc T f

Tactic:
simp_rw [setToSimpleFunc, _root_.smul_apply, smul_sum]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝
| (toSimpleFunc f).negPart a✝

Tactic:
← SimpleFunc.negPart_map_norm,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝
| (SimpleFunc.map norm (toSimpleFunc f).negPart) a✝
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, ((T (⇑(f.pair g) ⁻¹' {x})) x.1 + (T (⇑(f.pair g) ⁻¹' {x})) x.2) =
    ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2

Tactic:
rw [Finset.sum_add_distrib]

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ‖∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ‖ ≤ (∫⁻ (a : α), edist (f a) (g a) ∂μ).toReal

Tactic:
← integral_sub hf hg,

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ‖∫ (a : α), f a - g a ∂μ‖ ≤ (∫⁻ (a : α), edist (f a) (g a) ∂μ).toReal
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
| (fun x ↦ (u - v) x + (t - w) x) =o[l] fun x ↦ v x + w x

Tactic:
3,

Goal state after:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
| fun x ↦ v x + w x
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹⁸ : Ring R
inst✝¹⁷ : AddCommGroup V
inst✝¹⁶ : Module R V
inst✝¹⁵ : TopologicalSpace P
inst✝¹⁴ : AddTorsor V P
inst✝¹³ : AddCommGroup W
inst✝¹² : Module R W
inst✝¹¹ : TopologicalSpace Q
inst✝¹⁰ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝⁹ : AddCommGroup W₂
inst✝⁸ : Module R W₂
inst✝⁷ : TopologicalSpace Q₂
inst✝⁶ : AddTorsor W₂ Q₂
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalAddTorsor P
inst✝³ : TopologicalSpace W
inst✝² : IsTopologicalAddTorsor Q
inst✝¹ : TopologicalSpace W₂
inst✝ : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous ⇑(↑f).linear

Tactic:
rw [AffineMap.continuous_linear_iff]; exact f.cont

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ ‖f‖ ≤ c / r

Tactic:
by
  apply ContinuousLinearMap.opNorm_le_bound
  · apply div_nonneg _ r_pos.le
    exact
      (norm_nonneg _).trans
        (h 0 (by simp only [norm_zero, mem_closedBall, dist_zero_left, r_pos.le]))
  apply LinearMap.bound_of_ball_bound' r_pos
  exact fun z hz => h z hz

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✝⁵ : CompleteSpace G''
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : PartialOrder G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : ClosedIciTopology G''
inst✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(Lp G' 1 μ)
hfg : f ≤ g
⊢ (setToL1 hT) f ≤ (setToL1 hT) g

Tactic:
rw [← sub_nonneg] at hfg ⊢
  rw [← (setToL1 hT).map_sub]
  exact setToL1_nonneg hT hT_nonneg hfg

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ Isometry g

Tactic:
by
  convert! (vaddConst 𝕜 (f p)).symm.isometry.comp (hf.comp (vaddConst 𝕜 p).isometry)
  exact funext hg

Goal state after:
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
⊢ HasFiniteIntegral f (Measure.sum μ)

Tactic:
rw [HasFiniteIntegral, lintegral_sum_measure]
    convert! h.tsum_ofReal_lt_top with i
    rw [ofReal_integral_eq_lintegral_ofReal (hf i).norm]
    · simp_rw [ofReal_norm]
    · exact ae_of_all _ fun _ ↦ by positivity

Goal state after:
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α → E
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f

Tactic:
by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  by_cases hf : Integrable f μ
  · simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left' hT hT' c h_smul]
  · simp_rw [setToFun_undef _ hf, smul_zero]

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

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
inst✝ : Fintype X
f : X → E
⊢ ∫ (x : X), f x ∂Measure.count = ∑ a, f a

Tactic:
by simp [integral_fintype]

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ω

Goal state after:
α : 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
ω : α
hω : f ω ≤ 0
⊢ 0 ω ≤ (-f) ω
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.h_ae
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
hfg : f₂ =ᵐ[μ] g₂
a✝ : Integrable f₂ μ
⊢ setToFun μ T hT f₂ = setToFun μ' T hT' f₂ → setToFun μ T hT g₂ = setToFun μ' T hT' g₂

Tactic:
hf_eq

Goal state after:
case pos.h_ae
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
hfg : f₂ =ᵐ[μ] g₂
a✝ : Integrable f₂ μ
hf_eq : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂
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 α
f : α → E
ι : Type u_7
s : Finset ι
hs : s.Nonempty
μ : ι → Measure α
T : ι → Set α → E →L[ℝ] F
C : ι → ℝ
hTs : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
hf : ∀ i ∈ s, Integrable f (μ i)
⊢ setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i) ⋯ f = ∑ i ∈ s, setToFun (μ i) (T i) ⋯ f

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton i => simp
  | @cons i s his hs' ih =>
    simpa [his, ih fun j hj => hf j (Finset.mem_cons_of_mem hj)] using!
      setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μ T C hTs)
      (hf i (Finset.mem_cons_self i s))
      (integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_cons_of_mem hj))

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

Goal state before:
pp: case pos
α : 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
⊢ Tendsto (fun n ↦ Integrable.toL1 (fs n) ⋯) atTop (𝓝 (Integrable.toL1 f f_int))

Tactic:
tendsto_iff_norm_sub_tendsto_zero

Goal state after:
case pos
α : 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
⊢ Tendsto (fun e ↦ ‖Integrable.toL1 (fs e) ⋯ - Integrable.toL1 f f_int‖) atTop (𝓝 0)
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
hxy : x < y
⊢ leftLim f x ≤ leftLim f y

Tactic:
exact (hf.leftLim_le le_rfl).trans (hf.le_leftLim hxy)

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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∫ (x : X) in (s ∪ t) \ k, f x ∂μ = ∫ (x : X) in s \ k, f x ∂μ

Tactic:
union_sdiff_distrib,

Goal state after:
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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∫ (x : X) in s \ k ∪ t \ k, f x ∂μ = ∫ (x : X) in s \ k, f x ∂μ
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : x ∈ (fun g ↦ g • s) a
hxb : x ∈ (fun g ↦ g • s) b
⊢ False

Tactic:
mem_smul_set_iff_inv_smul_mem

Goal state after:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : a⁻¹ • x ∈ s
hxb : b⁻¹ • x ∈ s
⊢ False
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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in t ∩ k, f x ∂μ + ∫ (x : X) in t \ k, f x ∂μ

Tactic:
by
      rw [integral_inter_add_sdiff hk h'aux]

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
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₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
g₃ : G
hg₃ : g₃ ∈ t
h2V : g₁ * g₂ ∈ (fun h ↦ (fun h ↦ g₃ * h) ⁻¹' V) hg₃
⊢ g₂ ∈ ⋃ g ∈ t * s, (fun h ↦ g * h) ⁻¹' V

Tactic:
rw [mem_preimage, ← mul_assoc] at h2V

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₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
g₃ : G
hg₃ : g₃ ∈ t
h2V : g₃ * g₁ * g₂ ∈ V
⊢ g₂ ∈ ⋃ g ∈ t * s, (fun h ↦ g * h) ⁻¹' V
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: 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
a b : R
⊢ (let __OuterMeasure := f.outer;
      { toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ })
      (Ioc a b) =
    ofReal (↑f b - ↑f a)

Tactic:
exact f.outer_Ioc a b

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : μ ({x | a < f x} ∩ s) = 0
γ : G
x : α
⊢ x ∈ γ • {x | a < f x} ↔ x ∈ {x | a < f x}

Tactic:
mem_smul_set_iff_inv_smul_mem

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : μ ({x | a < f x} ∩ s) = 0
γ : G
x : α
⊢ γ⁻¹ • x ∈ {x | a < f x} ↔ x ∈ {x | a < f x}
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: 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
hf : Tendsto (↑f) atTop atTop
x : R
⊢ f.measure (Ioi x) = ∞

Tactic:
have : Nonempty R := ⟨x⟩
  refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_
  obtain ⟨N, hN⟩ := eventually_atTop.mp (tendsto_atTop.mp hf (r + f x))
  exact (f.measure_Ioc x (max x N) ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <|
    le_tsub_of_add_le_right <| hN _ (le_max_right x N))).trans (measure_mono Ioc_subset_Ioi_self)

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 z : F
⊢ ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫

Tactic:
by
  simp [sub_eq_add_neg, inner_add_right, inner_neg_right]

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

Goal state before:
pp: case h.refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens
h2U : IsOpen[inst✝¹] U
h3U : 1 ∈ U
⊢ U⁻¹ ⊆ V₁

Tactic:
exact Subset.trans (inv_subset.mpr h1U) inter_subset_left

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
K : Set G
hKE : K ⊆ E
hK : IsCompact K
K_closed : IsClosed[inst✝⁶] K
hKpos : 0 < μ K
g : G
hg : μ (g • K \ K) < μ K
hd : Disjoint (g • K) K
⊢ False

Tactic:
simp [hd.symm.sdiff_eq_right, measure_smul] at hg

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
⊢ Orthonormal 𝕜 (Matrix.vecCons v vs) ↔ ‖v‖ = 1 ∧ (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ Orthonormal 𝕜 vs

Tactic:
by
  simp_rw [Orthonormal, pairwise_fin_succ_iff_of_isSymm, Fin.forall_fin_succ]
  tauto

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
G : Type u_8
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E
y : F
f : E →L[𝕜] G
⊢ f ∘SL ((rankOne 𝕜) x) y = ((rankOne 𝕜) (f x)) y

Tactic:
by
  simp_rw [rankOne_def', ← comp_assoc, comp_toSpanSingleton]

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

Goal state before:
pp: case him
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := ⋯
K' : Submodule ℝ E := ⋯
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ im ⟪u - v, w⟫_𝕜 = im 0

Tactic:
· symm
      calc
        im (0 : 𝕜) = 0 := im.map_zero
        _ = re ⟪u - v, (-I : 𝕜) • w⟫ := (A _ (K.smul_mem (-I) hw)).symm
        _ = re (-I * ⟪u - v, w⟫) := by rw [inner_smul_right]
        _ = im ⟪u - v, w⟫ := by simp

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
v : E
hv : ‖v‖ = 1
w : E
⊢ (𝕜 ∙ v).starProjection w = ⟪v, w⟫ • v

Tactic:
rw [← smul_starProjection_singleton 𝕜 w]
  simp [hv]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝¹ : U.HasOrthogonalProjection
inst✝ : V.HasOrthogonalProjection
h : ∀ (x : E), U.orthogonalProjectionOnto ↑(V.orthogonalProjectionOnto x) = 0
x : ↥V
⊢ U.orthogonalProjectionOnto ↑x = 0

Tactic:
simpa using h (x : E)

Goal state after: