mathlib-initiative/mathlib-tactics huggingface dataset:
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 ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal

Tactic:
have h_right_g : ∫⁻ a, .ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ a, ‖g a‖ₑ ^ q ∂μ := by
    refine lintegral_congr fun x => ?_
    rw [← ofReal_norm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.symm.nonneg]

Goal state after:
α : 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 ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
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 : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
this : Integrable (fs i - f) μ
⊢ f = fs i - (fs i - f)

Tactic:
abel

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

Goal state before:
pp: case hbc.a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist (f₁ x, g₁ x).1 (f₂ x, g₂ x).1 ≤ dist (f₁, g₁).1 (f₂, g₂).1

Tactic:
exact dist_coe_le_dist x

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

Goal state before:
pp: case a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist (f₁ x, g₁ x).2 (f₂ x, g₂ x).2 ≤ dist (f₁, g₁).2 (f₂, g₂).2

Tactic:
exact dist_coe_le_dist x

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ ENNReal.ofReal |(thickenedIndicatorAux δ E x).toReal - (thickenedIndicatorAux δ E y).toReal| ≤
    ↑δ.toNNReal⁻¹ * edist x y

Tactic:
rw [← ENNReal.toReal_sub_of_le (thickenedIndicatorAux_mono_infEDist _ h) (by finiteness)]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ ENNReal.ofReal |(thickenedIndicatorAux δ E x - thickenedIndicatorAux δ E y).toReal| ≤ ↑δ.toNNReal⁻¹ * edist x y
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun δ ↦ (cthickening δ E).mulIndicator f) (𝓝 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f))

Tactic:
by
  rw [tendsto_pi_nhds]
  intro x
  rw [tendsto_congr' (mulIndicator_cthickening_eventually_eq_mulIndicator_closure f E x)]
  apply tendsto_const_nhds

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

Goal state before:
pp: case hbc
α : 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 : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖Integrable.toL1 f hf‖ ≤ (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
apply le_of_eq

Goal state after:
case hbc
α : 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 : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖Integrable.toL1 f hf‖ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
⊢ leftLim f a = f a

Tactic:
by
  rcases eq_or_neBot (𝓝[<] a) with h' | h'
  · simp [leftLim_eq_of_eq_bot f h']
  apply leftLim_eq_of_tendsto
  exact hf.tendsto.mono_left (nhdsWithin_mono _ Iio_subset_Iic_self)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝ : LinearOrder R
a b : R
⊢ Ioc a b \ botSet = Ioc a b

Tactic:
rw [sdiff_eq_left, disjoint_iff_forall_ne]

Goal state after:
R : Type u_1
inst✝ : LinearOrder R
a b : R
⊢ ∀ ⦃a_1 : R⦄, a_1 ∈ Ioc a b → ∀ ⦃b : R⦄, b ∈ botSet → a_1 ≠ b
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
μ : Measure X
ι : Type u_5
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ s✝, s i, f x ∂μ = ∑ i ∈ s✝, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : IntegrableOn f (s a✝) μ ∧ ∀ x ∈ s✝, IntegrableOn f (s x) μ
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ MeasurableSet (⋃ i ∈ s✝, s i)

Tactic:
· exact Finset.measurableSet_biUnion _ hs.2

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
s : Set R
hR : Nonempty R
⊢ f.length (s \ botSet) = f.length s

Tactic:
simp [length_eq]

Goal state after:
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
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i)
ab : a ≤ b
⊢ ∃ i ∈ s, b ∈ Iotop (c i) (d i)

Tactic:
simpa only [SetLike.mem_coe, mem_iUnion, exists_prop] using cv ⟨ab, le_rfl⟩

Goal state after:
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✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
A : Icc a' b ∩ s i ⊆ Ioc p q'
⊢ ∃ p, Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)

Tactic:
by_cases htq' : IsTop q'

Goal state after:
case pos
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : IsTop q'
⊢ ∃ p, Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)

case neg
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
⊢ ∃ p, Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K', K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε

Tactic:
by
  by_contra hc
  simp only [not_exists, not_and, not_le] at hc
  have lower_bound_iInf : μ K + ε ≤
      ⨅ (K' : TopologicalSpace.Compacts G) (_ : (K : Set G) ⊆ interior (K' : Set G)), μ K' :=
    le_iInf fun K' => le_iInf fun K'_hyp => le_of_lt (hc K' K'_hyp)
  rw [← H] at lower_bound_iInf
  exact (lt_self_iff_false (μ K)).mp (lt_of_le_of_lt' lower_bound_iInf
    (ENNReal.lt_add_right (ne_top_of_lt (μ.lt_top K)) (ENNReal.coe_ne_zero.mpr hε)))

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V

Tactic:
rw [← h2s, ← h2t]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + t.card
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
hab : a < b
A : Disjoint (Ioo a b) {b}
⊢ ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)

Tactic:
abel

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 α
ν : Measure α
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ covolume G α ν = ν s

Tactic:
by
  dsimp [covolume]
  simp only [(fund_dom_s.hasFundamentalDomain ν), ↓reduceDIte]
  rw [fund_dom_s.measure_eq]
  exact (fund_dom_s.hasFundamentalDomain ν).ExistsIsFundamentalDomain.choose_spec

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 α
ν : Measure α
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
this : HasFundamentalDomain G α ν
⊢ Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = μ

Tactic:
h𝓕.projection_respects_measure (μ := μ)

Goal state after:
G : Type u_1
α : Type u_3
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace α
ν : Measure α
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
this : HasFundamentalDomain G α ν
⊢ Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕)
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ∞
hA' : ⋃ i, A i = univ
⊢ ⋃ i, Quotient.mk α_mod_G '' A i = univ

Tactic:
· rw [← image_iUnion, hA']
    refine image_univ_of_surjective (by convert! Quotient.mk'_surjective)

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 α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ IsFiniteMeasure μ

Tactic:
h𝓕.projection_respects_measure (μ := μ)

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ IsFiniteMeasure (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: case neg
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : ¬HasFundamentalDomain G α ν
⊢ covolume G α ν < ∞

Tactic:
· simp [covolume, hasFun]

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
⊢ 0 ≤ chaar K₀ K

Tactic:
have := chaar_mem_haarProduct K₀ K (mem_univ _)

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : chaar K₀ K ∈ (fun K ↦ Icc 0 ↑(index ↑K ↑K₀)) K
⊢ 0 ≤ chaar K₀ K
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ⟪0, x⟫ = 0

Tactic:
← zero_smul 𝕜 (0 : E),

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ⟪0 • 0, x⟫ = 0
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)
eq₁ : wp - wq = a - b
⊢ u + u - (wq + wp) = u - wq + (u - wp)

Tactic:
abel

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
this : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2
⊢ ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)

Tactic:
abel

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:
simp_rw [Orthonormal, pairwise_fin_succ_iff_of_isSymm, Fin.forall_fin_succ]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
⊢ ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun i j ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) ↔
    ‖v‖ = 1 ∧ (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun i j ↦ ⟪vs i, vs j⟫ = 0
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✝ : DecidableEq ι
i j : ι
v : G i
w : G j
⊢ ⟪(V i) v, (V j) w⟫ = if i = j then ⟪(V i) v, (V j) w⟫ else 0

Tactic:
split_ifs with h
  · rfl
  · exact hV h v w

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⟩
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : ↑K
this : ⟪u - v, ↑w - v⟫_ℝ ≤ 0
⊢ u - v - (↑w - v) = u - ↑w

Tactic:
abel

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
s : Set (Set E)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, Orthonormal 𝕜 fun x ↦ ↑x
⊢ Orthonormal 𝕜 fun x ↦ ↑x

Tactic:
exact orthonormal_iUnion_of_directed hs.directed_val (by simpa using h)

Goal state after:
Module: Mathlib.Topology.Baire.CompleteMetrizable

Goal state before:
pp: case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
x✝ : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n ↦ 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → X → ℝ≥0∞ → X
radius : ℕ → X → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ := fun n ↦ Nat.recOn n (x, min ε (B 0)) fun n p ↦ (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun n ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun n ↦ (F n).2
n : ℕ
hn : 0 < r n
⊢ 0 < r (n + 1)

Tactic:
| succ n hn =>

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Module R M
S : Set (ClosedSubmodule R M)
⊢ ↑(sInf S) = ⨅ s ∈ S, ↑s

Tactic:
by
  simp [← coe_toSubmodule]

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

Goal state before:
pp: ι : Sort u_1
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Module R M
f : ι → ClosedSubmodule R M
⊢ ↑(⨅ i, f i) = ⨅ i, ↑(f i)

Tactic:
by
  simp [← coe_toSubmodule]

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

Goal state before:
pp: case e'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
w : ↥K := K.orthogonalProjectionOnto x
v : E := x - ↑w
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 2 • K.starProjection x - x = K.starProjection x - (x - K.starProjection x)

Tactic:
abel

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ 2 • (v - K.starProjection v) - v = v - 2 • K.starProjection v

Tactic:
abel

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

Goal state before:
pp: case e'_3
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := (ℝ ∙ (v - w))ᗮ.reflection
h₁ : R (v - w) = -(v - w)
h₂ : R (v + w) = v + w
⊢ w + w = v + w + -(v - w)

Tactic:
abel

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
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := x₁ - x₂
⊢ f x₁ - f x₂ - d • y = f x₁ - (a + d • y) - (f x₂ - a)

Tactic:
abel

Goal state after: