mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
⊢ span 𝕜 v = ⊤ ↔ ∃ b, ⇑b = Subtype.val

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
⊢ span 𝕜 v = ⊤ → ∃ b, ⇑b = Subtype.val

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
⊢ (∃ b, ⇑b = Subtype.val) → span 𝕜 v = ⊤
Module: Mathlib.Analysis.Normed.Lp.Matrix

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
p : ℝ≥0∞
⊢ (toLpLin p p) 1 = LinearMap.id

Tactic:
ext

Goal state after:
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
p : ℝ≥0∞
x✝ : WithLp p (n → R)
i✝ : n
⊢ (((toLpLin p p) 1) x✝).ofLp i✝ = (LinearMap.id x✝).ofLp i✝
Module: Mathlib.Analysis.Normed.Lp.Matrix

Goal state before:
pp: m : Type u_1
n : Type u_2
o : Type u_3
R : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
p q r : ℝ≥0∞
inst✝¹ : Fintype o
inst✝ : DecidableEq o
A : Matrix m n R
B : Matrix n o R
⊢ (toLpLin p r) (A * B) = (toLpLin q r) A ∘ₗ (toLpLin p q) B

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
o : Type u_3
R : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
p q r : ℝ≥0∞
inst✝¹ : Fintype o
inst✝ : DecidableEq o
A : Matrix m n R
B : Matrix n o R
x✝ : WithLp p (o → R)
i✝ : m
⊢ (((toLpLin p r) (A * B)) x✝).ofLp i✝ = (((toLpLin q r) A ∘ₗ (toLpLin p q) B) x✝).ofLp i✝
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ A.det ∈ unitary α

Tactic:
constructor

Goal state after:
case left
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ star A.det * A.det = 1

case right
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ A.det * star A.det = 1
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₁ᴴ).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

Tactic:
constructor

Goal state after:
case left
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

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)
⊢ 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 left
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

Tactic:
ext

Goal state after:
case left
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
⊢ ((kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap *
        kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂)
      i✝ j✝ =
    1 i✝ j✝
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)
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ *
      (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap =
    1

Tactic:
ext

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
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ *
        (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap)
      i✝ j✝ =
    1 i✝ j✝
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
h : 0 < p.toReal
⊢ edist f g = edist g f

Tactic:
· simp only [edist_eq_sum h, edist_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : ↥(unitaryGroup n α)
⊢ (map_star U)⁻¹ = transpose U

Tactic:
ext

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : ↥(unitaryGroup n α)
i✝ j✝ : n
⊢ ↑(map_star U)⁻¹ i✝ j✝ = ↑(transpose U) i✝ j✝
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
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
f : E →SL[σ] F
hinj : (↑f).ker = ⊥
hsurj : (↑f).range = ⊤
⊢ ↑(ofBijective f hinj hsurj) = f

Tactic:
ext

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
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
f : E →SL[σ] F
hinj : (↑f).ker = ⊥
hsurj : (↑f).range = ⊤
x✝ : E
⊢ ↑(ofBijective f hinj hsurj) x✝ = f x✝
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ IsUnit f ↔ Bijective ⇑f

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ IsUnit f → Bijective ⇑f

case mpr
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ Bijective ⇑f → IsUnit f
Module: Mathlib.Analysis.Normed.Lp.PiLp

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

Tactic:
ext

Goal state after:
ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
hp : p ≠ ∞
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ↑‖f‖₊ = ↑((∑ i, ‖f.ofLp i‖₊ ^ p.toReal) ^ (1 / p.toReal))
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
⊢ ‖f‖₊ = ⨆ i, ‖f.ofLp i‖₊

Tactic:
ext

Goal state after:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
⊢ ↑‖f‖₊ = ↑(⨆ i, ‖f.ofLp i‖₊)
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed[instTopologicalSpaceProd] ↑g.graph
⊢ ↑(ofIsClosedGraph hg) = g

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed[instTopologicalSpaceProd] ↑g.graph
x✝ : E
⊢ ↑(ofIsClosedGraph hg) x✝ = g x✝
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x
⊢ ↑(ofSeqClosedGraph hg) = g

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x
x✝ : E
⊢ ↑(ofSeqClosedGraph hg) x✝ = g x✝
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 β
⊢ 2 = ↑2

Tactic:
by norm_cast

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

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

Tactic:
simp [measureReal_def]

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
hp : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : Semiring 𝕜
ι' : Type u_5
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
⊢ (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e).symm = LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm

Tactic:
ext

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
hp : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : Semiring 𝕜
ι' : Type u_5
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
x✝ : PiLp p fun x ↦ E
i✝ : ι
⊢ ((LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e).symm x✝).ofLp i✝ =
    ((LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm) x✝).ofLp i✝
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: 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 : 𝕜
e : (i : ι) → α i ≃ₗᵢ[𝕜] β i
x : (i : ι) → α i
hp : 1 ≤ p.toReal
⊢ 1 ≤ p.toReal

Tactic:
by norm_cast

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
v : ι → E
⊢ parallelepiped v = ∑ i, segment ℝ 0 (v i)

Tactic:
ext

Goal state after:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ x✝ ∈ parallelepiped v ↔ x✝ ∈ ∑ i, segment ℝ 0 (v i)
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
v : ι → E
x✝ : E
⊢ (∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i, t i • v i) ↔
    ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a ↦ a • v i) '' Icc 0 1), ∑ i, g i = x✝

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i, t i • v i) →
    ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a ↦ a • v i) '' Icc 0 1), ∑ i, g i = x✝

case mpr
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a ↦ a • v i) '' Icc 0 1), ∑ i, g i = x✝) →
    ∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i, t i • v i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∃ t, (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a) ↔ ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∃ t, (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a) → ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)

case mpr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)) → ∃ t, (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a
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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
⊢ (∃ t ∈ Icc 0 1, x = ∑ i, t i • (v.prod w) i) ↔
    (∃ t ∈ Icc 0 1, x.1 = ∑ i, t i • v i) ∧ ∃ t ∈ Icc 0 1, x.2 = ∑ i, t i • w i

Tactic:
constructor

Goal state after:
case mp
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
⊢ (∃ t ∈ Icc 0 1, x = ∑ i, t i • (v.prod w) i) →
    (∃ t ∈ Icc 0 1, x.1 = ∑ i, t i • v i) ∧ ∃ t ∈ Icc 0 1, x.2 = ∑ i, t i • w i

case mpr
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
⊢ ((∃ t ∈ Icc 0 1, x.1 = ∑ i, t i • v i) ∧ ∃ t ∈ Icc 0 1, x.2 = ∑ i, t i • w i) →
    ∃ t ∈ Icc 0 1, x = ∑ i, t i • (v.prod w) i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mp
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x = ∑ i, t i • (v.prod w) i
⊢ (∃ t ∈ Icc 0 1, x.1 = ∑ i, t i • v i) ∧ ∃ t ∈ Icc 0 1, x.2 = ∑ i, t i • w i

Tactic:
constructor

Goal state after:
case mp.left
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x = ∑ i, t i • (v.prod w) i
⊢ ∃ t ∈ Icc 0 1, x.1 = ∑ i, t i • v i

case mp.right
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x = ∑ i, t i • (v.prod w) i
⊢ ∃ t ∈ Icc 0 1, x.2 = ∑ i, t i • w i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x = ∑ i, t i • (v.prod w) i
⊢ t ∘ Sum.inl ∈ Icc 0 1 ∧ x.1 = ∑ i, (t ∘ Sum.inl) i • v i

Tactic:
constructor

Goal state after:
case h.left
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x = ∑ i, t i • (v.prod w) i
⊢ t ∘ Sum.inl ∈ Icc 0 1

case h.right
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x = ∑ i, t i • (v.prod w) i
⊢ x.1 = ∑ i, (t ∘ Sum.inl) i • v i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x = ∑ i, t i • (v.prod w) i
⊢ t ∘ Sum.inr ∈ Icc 0 1 ∧ x.2 = ∑ i, (t ∘ Sum.inr) i • w i

Tactic:
constructor

Goal state after:
case h.left
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x = ∑ i, t i • (v.prod w) i
⊢ t ∘ Sum.inr ∈ Icc 0 1

case h.right
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x = ∑ i, t i • (v.prod w) i
⊢ x.2 = ∑ i, (t ∘ Sum.inr) i • w i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ Sum.elim t s ∈ Icc 0 1 ∧ x = ∑ i, Sum.elim t s i • (v.prod w) i

Tactic:
constructor

Goal state after:
case h.left
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ Sum.elim t s ∈ Icc 0 1

case h.right
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ x = ∑ i, Sum.elim t s i • (v.prod w) i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h.left
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ Sum.elim t s ∈ Icc 0 1

Tactic:
constructor

Goal state after:
case h.left.left
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ 0 ≤ Sum.elim t s

case h.left.right
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ Sum.elim t s ≤ 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h.right
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ x = ∑ i, Sum.elim t s i • (v.prod w) i

Tactic:
ext

Goal state after:
case h.right.fst
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ x.1 = (∑ i, Sum.elim t s i • (v.prod w) i).1

case h.right.snd
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ x.2 = (∑ i, Sum.elim t s i • (v.prod w) i).2
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Icc (f p.1) (g p.1)}

Tactic:
dsimp only [regionBetween, Icc, mem_ofPred_eq, ofPred_and]
  refine
    MeasurableSet.inter ?_
      ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_le measurable_snd (hg.comp measurable_fst)))
  exact measurable_fst hs

Goal state after: