mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm) ν μ
e : H ≃ G
hef : ∀ (g : H), Semiconj (⇑f) (fun x ↦ e g • x) fun x ↦ g • x
⊢ IsFundamentalDomain H (⇑f '' s) ν

Tactic:
rw [f.image_eq_preimage_symm]

Goal state after:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm) ν μ
e : H ≃ G
hef : ∀ (g : H), Semiconj (⇑f) (fun x ↦ e g • x) fun x ↦ g • x
⊢ IsFundamentalDomain H (⇑f.symm ⁻¹' s) ν
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
this : ∀ x ∈ s ∩ k, f x = 0
⊢ ∫ (x : X) in s \ k, f x ∂μ = ∫ (x : X) in s ∩ k, f x ∂μ + ∫ (x : X) in s \ k, f x ∂μ

Tactic:
setIntegral_eq_zero_of_forall_eq_zero this,

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
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
this : ∀ x ∈ s ∩ k, f x = 0
⊢ ∫ (x : X) in s \ k, f x ∂μ = 0 + ∫ (x : X) in s \ k, f x ∂μ
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 : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ ∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ

Tactic:
by
  symm
  nth_rw 1 [← setIntegral_univ]
  apply setIntegral_eq_of_subset_of_ae_sdiff_eq_zero nullMeasurableSet_univ (subset_univ _)
  filter_upwards [h] with x hx h'x using hx h'x.2

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

Goal state before:

Tactic:
μ.measure ↑K ≤ μ.measure (interior ↑K') := measure_mono K'_hyp.1
      _ ≤ μ K' := by
        rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]
        exact μ.outerMeasure_interior_compacts K'
      _ ≤ μ K + ε := K'_hyp.right

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
V : Set G
hV : (interior V).Nonempty
⊢ 0 < index (↑K) V

Tactic:
rw [index, Nat.sInf_def, Nat.find_pos, mem_image]
  · rintro ⟨t, h1t, h2t⟩; rw [Finset.card_eq_zero] at h2t; subst h2t
    obtain ⟨g, hg⟩ := K.interior_nonempty
    change g ∈ (∅ : Set G)
    convert! h1t (interior_subset hg); symm
    simp only [Finset.notMem_empty, iUnion_of_empty, iUnion_empty]
  · exact index_defined K.isCompact hV

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 ≤ s.card + t.card

Tactic:
refine le_trans (Nat.sInf_le ⟨_, ?_, rfl⟩) (Finset.card_union_le _ _)

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
⊢ s ∪ t ∈ {t | K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
s : Set α
inst✝² : Group H
inst✝¹ : MulAction H α
inst✝ : SMulCommClass H G α
g : H
⊢ fundamentalInterior G (g • s) = g • fundamentalInterior G s

Tactic:
simp_rw [fundamentalInterior, smul_set_sdiff, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]

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

Goal state before:
pp: case inr.hq
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}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : f.measure (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) = ofReal (↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a))
⊢ 0 ≤ leftLim (↑f) b - ↑f a

Tactic:
simp only [f.mono.le_leftLim hab, sub_nonneg]

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
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
⊢ f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)

Tactic:
· have A : Disjoint {a} (Ioo a b) := by simp
    simp [← Icc_union_Ioo_eq_Ico le_rfl hab, -singleton_union, f.mono.leftLim_le,
      measure_union A measurableSet_Ioo, f.mono.le_leftLim hab, ← ENNReal.ofReal_add]

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✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : R
this : Nonempty R
⊢ f.measure (Iio x) = ofReal (leftLim (↑f) x - l)

Tactic:
rw [← Iic_sdiff_right, measure_sdiff _ (nullMeasurableSet_singleton x), measure_singleton,
    f.measure_Iic hf, ← ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)]

Goal state after:
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 : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : R
this : Nonempty R
⊢ ofReal (↑f x - l - (↑f x - leftLim (↑f) x)) = ofReal (leftLim (↑f) x - l)

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 : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : R
this : Nonempty R
⊢ f.measure {x} ≠ ∞

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 : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : R
this : Nonempty R
⊢ {x} ⊆ Iic x
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
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)
l : ℝ
hl : Tendsto (↑f) atBot (𝓝 l)
⊢ IsFiniteMeasure f.measure

Tactic:
exact f.isFiniteMeasure hl hu

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

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ lintegral μ (E.indicator fun x ↦ 1) ≤ lintegral μ (thickenedIndicatorAux δ E)

Tactic:
· apply lintegral_mono
    apply indicator_le_thickenedIndicatorAux

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ ^ 2 ≤ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2

Tactic:
simp only [sq]

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖ * ‖u - (θ • w + (1 - θ) • v)‖
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ ^ 2 - 2 * re (θ * ⟪u - v, w - v⟫_ℝ) + (‖θ‖ * ‖w - v‖) ^ 2 =
    ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2

Tactic:
simp only [sq]

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ - 2 * re (θ * ⟪u - v, w - v⟫_ℝ) + ‖θ‖ * ‖w - v‖ * (‖θ‖ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: 𝕜 : 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 := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K'
⊢ ⟪u - v, w⟫_ℝ = 0

Tactic:
real_inner_eq_re_inner,

Goal state after:
𝕜 : 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 := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K'
⊢ re ⟪u - v, w⟫_𝕜 = 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✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (Summable fun i ↦ (V i) (f i)) ↔ Summable fun i ↦ ‖f i‖ ^ 2

Tactic:
simp only [summable_iff_cauchySeq_finset, NormedAddCommGroup.cauchySeq_iff, norm_neg_add,
      Real.norm_eq_abs]

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
⊢ (∀ ε > 0,
      ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε) ↔
    ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ ∃ r, ⟪T x, x⟫ = ↑r

Tactic:
← conj_eq_iff_real

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ (starRingEnd 𝕜) ⟪T x, x⟫ = ⟪T x, x⟫
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : K₁.HasOrthogonalProjection
x : E
v : ↥K₁ := ⋯
hvm : x - ↑v ∈ K₁ᗮ
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) → x ∈ K₂

Tactic:
rintro ⟨y, hy, z, hz, rfl⟩
    exact K₂.add_mem (h hy) hz.2

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
x : E
S : Submodule 𝕜 E
inst✝ : S.HasOrthogonalProjection
⊢ ‖S.starProjection x + Sᗮ.starProjection x‖ ^ 2 =
    ‖S.orthogonalProjectionOnto x‖ ^ 2 + ‖Sᗮ.orthogonalProjectionOnto x‖ ^ 2

Tactic:
simp only [sq]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst✝ : S.HasOrthogonalProjection
⊢ ‖S.starProjection x + Sᗮ.starProjection x‖ * ‖S.starProjection x + Sᗮ.starProjection x‖ =
    ‖S.orthogonalProjectionOnto x‖ * ‖S.orthogonalProjectionOnto x‖ +
      ‖Sᗮ.orthogonalProjectionOnto x‖ * ‖Sᗮ.orthogonalProjectionOnto x‖
Module: Mathlib.Analysis.Normed.Operator.Banach

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

Tactic:
exact (hg y).1

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

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
⊢ Subgroup.closure (Set.range fun v ↦ (ℝ ∙ v)ᗮ.reflection) = ⊤

Tactic:
Subgroup.eq_top_iff'

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
⊢ ∀ (x : F ≃ₗᵢ[ℝ] F), x ∈ Subgroup.closure (Set.range fun v ↦ (ℝ ∙ v)ᗮ.reflection)
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
ENNReal.toReal_pos_iff_ne_top

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ p ≠ ∞
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 β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ dist x y = ‖-x + y‖

Tactic:
simp only [prod_dist_eq_add (zero_lt_one.trans_le h),
        prod_norm_eq_add (zero_lt_one.trans_le h), dist_eq_norm, ← norm_neg_add]
      rfl

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

Goal state before:
pp: case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp ∞ β
⊢ edist f g = edist g f

Tactic:
simp only [edist_eq_iSup, edist_comm]

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

Goal state before:
pp: 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
⊢ 0 < p.toReal

Tactic:
ENNReal.toReal_pos_iff_ne_top

Goal state after:
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
⊢ p ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a b : ℝ
⊢ volume (uIcc a b) = ofReal |b - a|

Tactic:
by
  rw [← Icc_min_max, volume_Icc, max_sub_min_eq_abs]

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

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t, ((∀ (i : ι), 0 ≤ t i) ∧ ∀ (i : ι), t i ≤ 1) ∧ ∀ (i : ι), (b.repr x) i = t i) ↔
    ∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1

Tactic:
← forall_and

Goal state after:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t, ∀ (x_1 : ι), (0 ≤ t x_1 ∧ t x_1 ≤ 1) ∧ (b.repr x) x_1 = t x_1) ↔ ∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
⊢ b.addHaar (⇑f ⁻¹' _root_.parallelepiped (⇑↑f ∘ ⇑b)) = b.addHaar (_root_.parallelepiped ⇑b)

Tactic:
← f.toEquiv.preimage_image (_root_.parallelepiped ⇑b)

Goal state after:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
⊢ b.addHaar (⇑f ⁻¹' _root_.parallelepiped (⇑↑f ∘ ⇑b)) =
    b.addHaar (⇑(↑f).toEquiv ⁻¹' ⇑(↑f).toEquiv '' _root_.parallelepiped ⇑b)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ μ (⋃ n, {u n} + s) = μ (range u + s)

Tactic:
← iUnion_add,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ μ ((⋃ i, {u i}) + s) = μ (range u + s)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : s ≠ ⊤
⊢ μ ↑s = 0

Tactic:
rcases s.eq_bot_or_nonempty with (rfl | hne)
  · rw [AffineSubspace.bot_coe, measure_empty]
  rw [Ne, ← AffineSubspace.direction_eq_top_iff_of_nonempty hne] at hs
  rcases hne with ⟨x, hx : x ∈ s⟩
  simpa only [AffineSubspace.coe_direction_eq_vsub_set_right hx, vsub_eq_sub, sub_eq_add_neg,
    image_add_right, neg_neg, measure_preimage_add_right] using addHaar_submodule μ s.direction hs

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
i : ι
hi : 0 ≤ (b.repr x) i → 1 ≤ (b.repr x) i
this : (b.repr x) i = 1
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Tactic:
rw [← b.sum_repr x, ← Finset.sum_erase_add _ _ (Finset.mem_univ i), this, one_smul, ← vadd_eq_add]

Goal state after:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
i : ι
hi : 0 ≤ (b.repr x) i → 1 ≤ (b.repr x) i
this : (b.repr x) i = 1
⊢ ∑ x_1 ∈ Finset.univ.erase i, (b.repr x) x_1 • b x_1 +ᵥ b i ∈
    ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
⊢ Disjoint ↑(I.splitCenterBox s) ↑(I.splitCenterBox t)

Tactic:
rw [disjoint_iff_inf_le]

Goal state after:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
⊢ ↑(I.splitCenterBox s) ⊓ ↑(I.splitCenterBox t) ⊆ ⊥
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Module ℚ E
this✝ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
⊢ ⊤ ≤ span K (Set.range Subtype.val)

Tactic:
simp [ht_span, h_spanE]

Goal state after: