mathlib-initiative/mathlib-tactics huggingface dataset:
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)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ ∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖

Tactic:
let u n := g (h^[n] y)

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
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)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
⊢ ∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
Module: Mathlib.Analysis.Normed.Lp.ProdLp

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

Tactic:
exact prod_norm_eq_of_L1 x

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ ∈ unitary (Matrix (n × m) (n × m) R)

Tactic:
simp_rw [Unitary.mem_iff, star_eq_conjTranspose, conjTranspose_kronecker']

Goal state after:
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap *
        kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ =
      1 ∧
    kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ *
        (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap =
      1
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case right
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ ∑ j, U₁ i✝.1 j.1 * U₂ i✝.2 j.2 * star U₂ j.2 j✝.2 * star U₁ j.1 j✝.1 = 1 i✝ j✝

Tactic:
mul_assoc _ _ (star U₂ _ _),

Goal state after:
case right
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ ∑ x, U₁ i✝.1 x.1 * (U₂ i✝.2 x.2 * star U₂ x.2 j✝.2) * star U₁ x.1 j✝.1 = 1 i✝ j✝
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
i : ι
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x y

Tactic:
by
  rcases p.dichotomy with (rfl | h)
  · simpa only [edist_eq_iSup] using le_iSup (fun i => edist (x i) (y i)) i
  · have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (zero_lt_one.trans_le h).ne'
    rw [edist_eq_sum (zero_lt_one.trans_le h)]
    calc
      edist (x i) (y i) = (edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) := by
        simp [← ENNReal.rpow_mul, cancel, -one_div]
      _ ≤ (∑ i, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) := by
        gcongr
        exact Finset.single_le_sum (fun i _ => (bot_le : (0 : ℝ≥0∞) ≤ _)) (Finset.mem_univ i)

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

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
this : ↑(Fintype.card ι) = ↑↑(Fintype.card ι)
⊢ ↑(Fintype.card ι) ^ (1 / p.toReal) * edist x.ofLp y.ofLp = ↑(↑(Fintype.card ι) ^ (1 / p.toReal)) * edist x.ofLp y.ofLp

Tactic:
this,

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
this : ↑(Fintype.card ι) = ↑↑(Fintype.card ι)
⊢ ↑↑(Fintype.card ι) ^ (1 / p.toReal) * edist x.ofLp y.ofLp =
    ↑(↑(Fintype.card ι) ^ (1 / p.toReal)) * edist x.ofLp y.ofLp
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = ↑n
f : PiLp p β
this : 0 < p.toReal
⊢ ‖f‖ = (∑ i, ‖f.ofLp i‖ ^ n) ^ (1 / ↑n)

Tactic:
simp only [one_div, h, Real.rpow_natCast, ENNReal.toReal_natCast,
    norm_eq_sum this]

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i, ‖x.ofLp i‖ ^ 2) ^ (1 / ↑2) = √(∑ i, ‖x.ofLp i‖ ^ 2)

Tactic:
rw [Real.sqrt_eq_rpow]

Goal state after:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i, ‖x.ofLp i‖ ^ 2) ^ (1 / ↑2) = (∑ i, ‖x.ofLp i‖ ^ 2) ^ (1 / 2)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inl
a : ℝ
⊢ volume (eball a ∞) = 2 * ∞

pp: case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (eball a r) = 2 * r

Tactic:
· rw [Metric.eball_top, volume_univ, two_mul, _root_.top_add]

Goal state after:
case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (eball a r) = 2 * r
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
this : Icc 0 1 = ⇑K '' Icc 0 1
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) '' Icc 0 1

Tactic:
this,

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
this : Icc 0 1 = ⇑K '' Icc 0 1
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) '' ⇑K '' Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * volume ((fun x ↦ D i * x) ⁻¹' s i) = volume (s i)
⊢ ofReal |∏ i, D i| * volume (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi s) = ∏ x, volume (s x)

Tactic:
this,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * volume ((fun x ↦ D i * x) ⁻¹' s i) = volume (s i)
⊢ ofReal |∏ i, D i| * volume (univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i) = ∏ x, volume (s x)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
p : ℝ≥0∞
𝕜 : Type u_1
ι✝ : Type u_2
α✝ : ι✝ → Type u_3
β : ι✝ → Type u_4
hp : Fact (1 ≤ p)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : Type u_6
α : ι ⊕ κ → Type u_7
inst✝⁴ : Fintype ι
inst✝³ : Fintype κ
inst✝² : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)
inst✝¹ : (i : ι ⊕ κ) → Module 𝕜 (α i)
x : (i : ι ⊕ κ) → α i
inst✝ : Fact (1 ≤ ∞)
__LinearEquiv✝ : WithLp ∞ ((i : ι ⊕ κ) → α i) ≃ₗ[𝕜]
  WithLp ∞ (WithLp ∞ ((i : ι) → α (Sum.inl i)) × WithLp ∞ ((i : κ) → α (Sum.inr i))) :=
  WithLp.linearEquiv ∞ 𝕜 ((i : ι ⊕ κ) → α i) ≪≫ₗ LinearEquiv.sumPiEquivProdPi 𝕜 ι κ α ≪≫ₗ
      (WithLp.linearEquiv ∞ 𝕜 ((s : ι) → α (Sum.inl s))).symm.prodCongr
        (WithLp.linearEquiv ∞ 𝕜 ((t : κ) → α (Sum.inr t))).symm ≪≫ₗ
    (WithLp.linearEquiv ∞ 𝕜 (WithLp ∞ ((s : ι) → α (Sum.inl s)) × WithLp ∞ ((t : κ) → α (Sum.inr t)))).symm
⊢ ‖(WithLp.linearEquiv ∞ 𝕜 ((i : ι ⊕ κ) → α i) ≪≫ₗ LinearEquiv.sumPiEquivProdPi 𝕜 ι κ α ≪≫ₗ
            (WithLp.linearEquiv ∞ 𝕜 ((s : ι) → α (Sum.inl s))).symm.prodCongr
              (WithLp.linearEquiv ∞ 𝕜 ((t : κ) → α (Sum.inr t))).symm ≪≫ₗ
          (WithLp.linearEquiv ∞ 𝕜 (WithLp ∞ ((s : ι) → α (Sum.inl s)) × WithLp ∞ ((t : κ) → α (Sum.inr t)))).symm)
        ((WithLp.linearEquiv ∞ 𝕜 ((i : ι ⊕ κ) → α i)).symm x)‖ =
    ‖(WithLp.linearEquiv ∞ 𝕜 ((i : ι ⊕ κ) → α i)).symm x‖

Tactic:
simp [← Finset.univ_disjSum_univ, Finset.sup_disjSum, Pi.norm_def]

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

Goal state before:
pp: case mpr.refine_2.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ≤ x i ∧ x i ≤ 0
hai : a i = 0
⊢ x i = x i / a i * a i

Tactic:
← le_antisymm_iff

Goal state after:
case mpr.refine_2.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 = x i
hai : a i = 0
⊢ x i = x i / a i * a i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ SigmaFinite b.addHaar

Tactic:
have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
  rw [Basis.addHaar_def]; exact sigmaFinite_addHaarMeasure

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∉ s
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0

Tactic:
· have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = Ioo (f x) (g x) := by simp [h, Ioo]
          simp only [hx, Real.volume_Ioo]

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∉ s
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
val✝ : Fintype ι
this : μ = μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
this,

Goal state after:
case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
val✝ : Fintype ι
this : μ = μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
⊢ map (⇑f) (μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)) =
    ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
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
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det g ≠ 0
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
gdet : LinearMap.det g = LinearMap.det f
fg : f = ↑e.symm ∘ₗ g ∘ₗ ↑e
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
Cg : Continuous ⇑g
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑e.symm
this : (map (⇑e) μ).IsAddHaarMeasure
x : E
⊢ (⇑e.symm ∘ ⇑e) x = id x

Tactic:
simp only [id, Function.comp_apply, LinearEquiv.symm_apply_apply]

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

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
y : ℤ
hy : ↑y = ↑x i
⊢ |↑y| < 1 ↔ ↑y = 0

Tactic:
← Int.cast_abs,

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
y : ℤ
hy : ↑y = ↑x i
⊢ ↑|y| < 1 ↔ ↑y = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
this : ball 0 r = (fun x_1 ↦ x + x_1) ⁻¹' ball x r
⊢ μ (ball x r) = μ (ball 0 r)

Tactic:
this,

Goal state after:
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
this : ball 0 r = (fun x_1 ↦ x + x_1) ⁻¹' ball x r
⊢ μ (ball x r) = μ ((fun x_1 ↦ x + x_1) ⁻¹' ball x r)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
this : closedBall 0 r = (fun x_1 ↦ x + x_1) ⁻¹' closedBall x r
⊢ μ (closedBall x r) = μ (closedBall 0 r)

Tactic:
this,

Goal state after:
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
this : closedBall 0 r = (fun x_1 ↦ x + x_1) ⁻¹' closedBall x r
⊢ μ (closedBall x r) = μ ((fun x_1 ↦ x + x_1) ⁻¹' closedBall x r)
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_1 ∈ Finset.univ.erase i, (b.repr x) x_1 • b x_1 + (b.repr x) i • b i ∈
    ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Tactic:
this,

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 + 1 • b i ∈
    ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case neg
ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
h : ¬∀ (i : ι), l i < u i
⊢ ⊥ = ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper

Tactic:
suffices l = lI → u ≠ uI by simpa
    rintro rfl rfl
    exact h hI

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case mpr
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : ∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J'
HU : π₁.iUnion ⊆ π₂.iUnion
J : Box ι
hJ : J ∈ π₁
⊢ ∃ I' ∈ π₂, J ≤ I'

Tactic:
simp only [Set.subset_def, mem_iUnion] at HU

Goal state after:
case mpr
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : ∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J ∈ π₁, x ∈ J) → ∃ J ∈ π₂, x ∈ J
⊢ ∃ I' ∈ π₂, J ≤ I'
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h : π₂.iUnion = ↑I \ π₁.iUnion
⊢ π₁.iUnion ∪ π₂.iUnion = ↑I

Tactic:
by simp [h, π₁.iUnion_subset]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: case refine_1
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
inst✝ : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ Box.Icc J ⊆ closedBall ((π₁.disjUnion π₂ h).tag J) ↑(r ((π₁.disjUnion π₂ h).tag J))

Tactic:
rw [disjUnion_tag_of_mem_left _ hJ]

Goal state after:
case refine_1
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
inst✝ : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ Box.Icc J ⊆ closedBall (π₁.tag J) ↑(r (π₁.tag J))
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: case refine_1
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ (π₁.disjUnion π₂ h).tag J ∈ Box.Icc J

Tactic:
rw [disjUnion_tag_of_mem_left _ hJ]

Goal state after:
case refine_1
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ π₁.tag J ∈ Box.Icc J
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b b' : OrthonormalBasis ι 𝕜 E
h : (fun b i ↦ b.repr.symm (EuclideanSpace.single i 1)) b = (fun b i ↦ b.repr.symm (EuclideanSpace.single i 1)) b'
i : ι
k : 𝕜
this : k = k • 1
⊢ (↑b.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm) (Pi.single i k) =
    (↑b'.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm) (Pi.single i k)

Tactic:
this,

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b b' : OrthonormalBasis ι 𝕜 E
h : (fun b i ↦ b.repr.symm (EuclideanSpace.single i 1)) b = (fun b i ↦ b.repr.symm (EuclideanSpace.single i 1)) b'
i : ι
k : 𝕜
this : k = k • 1
⊢ (↑b.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm) (Pi.single i (k • 1)) =
    (↑b'.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm) (Pi.single i (k • 1))
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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x : ↥L
i : ι
⊢ ((ofZLatticeBasis K L b).repr ↑x) i = ↑((b.repr x) i)

Tactic:
by
  suffices ((b.ofZLatticeBasis K L).repr.toLinearMap.restrictScalars ℤ) ∘ₗ L.subtype
      = Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ b.repr.toLinearMap by
    exact DFunLike.congr_fun (LinearMap.congr_fun this x) i
  refine Basis.ext b fun i ↦ ?_
  simp_rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, coe_subtype, ← b.ofZLatticeBasis_apply K, repr_self,
    Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply, map_one]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop, π ⊓ splitMany I t = (splitMany I t).filter fun J ↦ ↑J ⊆ π.iUnion

Tactic:
by
  refine (eventually_not_disjoint_imp_le_of_mem_splitMany π.boxes).mono fun t ht => ?_
  refine le_antisymm ((biUnion_le_iff _).2 fun J hJ => ?_) (le_inf (fun J hJ => ?_) (filter_le _ _))
  · refine ofWithBot_mono ?_
    simp only [Finset.mem_image, mem_boxes, mem_filter]
    rintro _ ⟨J₁, h₁, rfl⟩ hne
    refine ⟨_, ⟨J₁, ⟨h₁, Subset.trans ?_ (π.subset_iUnion hJ)⟩, rfl⟩, le_rfl⟩
    exact ht I J hJ J₁ h₁ (mt disjoint_iff.1 hne)
  · rw [mem_filter] at hJ
    rcases Set.mem_iUnion₂.1 (hJ.2 J.upper_mem) with ⟨J', hJ', hmem⟩
    refine ⟨J', hJ', ht I _ hJ' _ hJ.1 <| Box.not_disjoint_coe_iff_nonempty_inter.2 ?_⟩
    exact ⟨J.upper, hmem, J.upper_mem⟩

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

Goal state before:
pp: case e'_1
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
x✝ : E
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

pp: case e'_3
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
e_1✝ : ↥L = ↥(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)))
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

pp: case e'_4
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
e_1✝ : ↥L = ↥(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)))
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

Tactic:
all_goals exact (b.ofZLatticeBasis_span ℝ).symm

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : NormedField K
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
x✝ : E
h : x✝ ∈ L
⊢ (↑ℤ ↑e.symm) x✝ ∈ ZLattice.comap K L ↑e

Tactic:
by simpa [← SetLike.mem_coe] using h

Goal state after: