mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_1
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
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
⊢ ¬LinearIndepOn ℚ id (insert v (Set.range ⇑e))

Tactic:
linearIndepOn_id_insert (Set.notMem_of_mem_sdiff hv),

Goal state after:
case refine_1
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
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
⊢ ¬(LinearIndepOn ℚ id (Set.range ⇑e) ∧ v ∉ span ℚ (Set.range ⇑e))
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq ι
i : ι
a : 𝕜
j : ι
⊢ (single i a).ofLp j = if j = i then a else 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq ι
i : ι
a : 𝕜
⊢ single i a = 0 ↔ a = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a : 𝕜
⊢ ‖single i a‖ = ‖a‖

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a : 𝕜
⊢ ‖single i a‖₊ = ‖a‖₊

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a b : 𝕜
⊢ dist (single i a) (single i b) = dist a b

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a b : 𝕜
⊢ nndist (single i a) (single i b) = nndist a b

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a b : 𝕜
⊢ edist (single i a) (single i b) = edist a b

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
I J : Box ι
x : ι → ℝ
p : (ι → ℝ) → Box ι → Prop
hJ : J ≤ I
h : x ∈ Box.Icc I
⊢ (∀ J' ∈ single I J hJ x h, p ((single I J hJ x h).tag J') J') ↔ p x J

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
I✝ J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I✝
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
I J : Box ι
h : I ≤ J
⊢ Injective fun π ↦ { boxes := π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯, tag := π.tag, tag_mem_Icc := ⋯ }

Tactic:
rintro ⟨⟨b₁, h₁le, h₁d⟩, t₁, ht₁⟩ ⟨⟨b₂, h₂le, h₂d⟩, t₂, ht₂⟩ H

Goal state after:
ι : Type u_1
I✝ J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I✝
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
I J : Box ι
h : I ≤ J
t₁ : Box ι → ι → ℝ
ht₁ : ∀ (J : Box ι), t₁ J ∈ Box.Icc I
b₁ : Finset (Box ι)
h₁le : ∀ J ∈ b₁, J ≤ I
h₁d : (↑b₁).Pairwise (Disjoint on Box.toSet)
t₂ : Box ι → ι → ℝ
ht₂ : ∀ (J : Box ι), t₂ J ∈ Box.Icc I
b₂ : Finset (Box ι)
h₂le : ∀ J ∈ b₂, J ≤ I
h₂d : (↑b₂).Pairwise (Disjoint on Box.toSet)
H :
  (fun π ↦ { boxes := π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯, tag := π.tag, tag_mem_Icc := ⋯ })
      { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d, tag := t₁, tag_mem_Icc := ht₁ } =
    (fun π ↦ { boxes := π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯, tag := π.tag, tag_mem_Icc := ⋯ })
      { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d, tag := t₂, tag_mem_Icc := ht₂ }
⊢ { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d, tag := t₁, tag_mem_Icc := ht₁ } =
    { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d, tag := t₂, tag_mem_Icc := ht₂ }
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ ⟪b i, b i⟫ = 1

Tactic:
simp

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

Goal state before:
pp: case e'_2.a
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1, ((innerSL 𝕜) x) ((b.repr y).ofLp x_1 • b x_1) = ((innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ⟪b x✝, y⟫ * ⟪x, b x✝⟫ = ⟪b x✝, y⟫ • ((innerSL 𝕜) x) (b x✝)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
x : E
⊢ ∑ i, ⟪b i, x⟫ ^ 2 = ∑ i, ‖⟪b i, x⟫‖ ^ 2

Tactic:
simp

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

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ Box.Icc J
HIcc : Box.Icc J ⊆ Box.Icc I ∧ Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ n
i : ι
⊢ J.upper i - J.lower i = (J.upper i - J.lower i) / 2 ^ 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
a✝ : i ∈ Finset.univ
⊢ BddAbove (range fun j ↦ ‖⟪b j, x⟫‖)

Tactic:
simp

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

Goal state before:
pp: case e_a.inl
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
h✝ : IsEmpty ι
⊢ 0 ≤ ⨆ j, ‖⟪b j, x⟫‖

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
h✝ : Nonempty ι
⊢ BddAbove (range fun j ↦ ‖⟪b j, x⟫‖)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ↑(I.splitLower i x) ⊆ ↑↑I

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ↑(I.splitUpper i x) ⊆ ↑↑I

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
⊢ ⇑(v.toOrthonormalBasis hv).toBasis = ⇑v

Tactic:
simp

Goal state after:
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 ι✝
ι : Type u_7
𝕜 : Type u_8
inst✝¹ : Unique ι
inst✝ : RCLike 𝕜
⊢ Orthonormal 𝕜 ⇑(Basis.singleton ι 𝕜)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_7
𝕜 : Type u_8
inst✝¹ : Unique ι
inst✝ : RCLike 𝕜
x✝ : ι
⊢ (OrthonormalBasis.singleton ι 𝕜) x✝ = 1 x✝

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π ⊓ splitMany I ∅ = π.biUnion fun J ↦ splitMany J ∅

Tactic:
simp

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

Goal state before:
pp: case inl
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
i : η
j : ι i
⊢ (B i).repr.symm (toLp 2 (Pi.single i (Pi.single j 1) i)) = Pi.single i ((B i) j) i

Tactic:
simp

Goal state after:
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✝ : E
⊢ x✝ ∈ Set.range ⇑(ofZLatticeBasis K L b) ↔ x✝ ∈ ⇑L.subtype '' Set.range ⇑b

Tactic:
simp

Goal state after:
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
inst✝³ : Fintype ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
i : ι
j : ι'
⊢ ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) (EuclideanSpace.single i 1)).ofLp j =
    (EuclideanSpace.single (e i) 1).ofLp j

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ ∀ (i : ι), (b.equiv b (Equiv.refl ι)) (b.toBasis i) = (LinearIsometryEquiv.refl 𝕜 E) (b.toBasis i)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π₁ : TaggedPrepartition I
hπ₁ : l.MemBaseSet I c r₁ π₁
hle : ∀ x ∈ Box.Icc I, r₂ x ≤ r₁ x
π₂ : Prepartition I
hU : π₂.iUnion = ↑I \ π₁.iUnion
hc : l.bDistortion = true → π₂.distortion ≤ c
x✝ : l.bDistortion = true
⊢ ⊥.iUnion = ↑I \ (π₁.unionComplToSubordinate π₂ hU r₂).iUnion ∧ ⊥.distortion ≤ c

Tactic:
simp

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

Goal state before:
pp: case «0»
ι : 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 ι
⊢ ∀ (j : Fin 2), inner ℝ (basisOneI ((fun i ↦ i) ⟨0, ⋯⟩)) (basisOneI j) = if (fun i ↦ i) ⟨0, ⋯⟩ = j then 1 else 0

Tactic:
intro j

Goal state after:
case «0»
ι : 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 ι
j : Fin 2
⊢ inner ℝ (basisOneI ((fun i ↦ i) ⟨0, ⋯⟩)) (basisOneI j) = if (fun i ↦ i) ⟨0, ⋯⟩ = j then 1 else 0
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case «1»
ι : 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 ι
⊢ ∀ (j : Fin 2), inner ℝ (basisOneI ((fun i ↦ i) ⟨1, ⋯⟩)) (basisOneI j) = if (fun i ↦ i) ⟨1, ⋯⟩ = j then 1 else 0

Tactic:
intro j

Goal state after:
case «1»
ι : 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 ι
j : Fin 2
⊢ inner ℝ (basisOneI ((fun i ↦ i) ⟨1, ⋯⟩)) (basisOneI j) = if (fun i ↦ i) ⟨1, ⋯⟩ = j then 1 else 0
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
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace K F
inst✝³ : FiniteDimensional K F
inst✝² : ProperSpace F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
ι : Type u_4
b : Basis ι ℤ ↥L
i✝ : ι
⊢ (ofZLatticeBasis K (ZLattice.comap K L ↑↑e) (ofZLatticeComap K L (↑e) b)) i✝ =
    ((ofZLatticeBasis K L b).map ↑e.symm) i✝

Tactic:
simp

Goal state after:
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 ι
v : Set E
A : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(A i)) fun i ↦ (A i).subtypeₗᵢ
inst✝¹ : DecidableEq ι
hV_sum : IsInternal fun i ↦ A i
α : ι → Type u_7
inst✝ : (i : ι) → Fintype (α i)
v_family : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)
⊢ ∀ (i : ι), Orthonormal 𝕜 ⇑(v_family i).toBasis

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
⊢ ∑ J ∈ (splitMany I ∅).boxes, f J = f I

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : ⊤.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ⊤.compl.distortion ≤ c

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case refine_3
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset
fu : ↥u ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm
hu : Orthonormal 𝕜 Subtype.val
⊢ ⇑(OrthonormalBasis.mkOfOrthogonalEqBot hu ⋯) = Subtype.val

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.domRestrict v)
hsv : Injective (s.domRestrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.domRestrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s ↑Y
⊢ InjOn v s

Tactic:
Set.injOn_iff_injective

Goal state after:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.domRestrict v)
hsv : Injective (s.domRestrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.domRestrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s ↑Y
⊢ Injective (s.domRestrict v)
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : r = ∞
⊢ 2 > 1

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝³ : RCLike 𝕜
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L : ↥S →ₗᵢ[𝕜] V
s : ↥S
⊢ (L.toLinearMap ∘ₗ ↑S.orthogonalProjectionOnto +
        (L.rangeᗮ.subtypeₗᵢ.comp
              ((stdOrthonormalBasis 𝕜 ↥Sᗮ).repr.trans
                  ((stdOrthonormalBasis 𝕜 ↥L.rangeᗮ).reindex (finCongr ⋯)).repr.symm).toLinearIsometry).toLinearMap ∘ₗ
          ↑Sᗮ.orthogonalProjectionOnto)
      ↑s =
    L.toLinearMap s

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
x : ι → ℝ
hx : x ∈ Box.Icc I \ s
⊢ ∃ r, closedBall x ↑r ⊆ Fᶜ

Tactic:
obtain ⟨r, hr₀, hr⟩ :=
      nhds_basis_closedBall.mem_iff.1 (hFc.isOpen_compl.mem_nhds fun hx' => hx.2 (hFs hx').1)

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
x : ι → ℝ
hx : x ∈ Box.Icc I \ s
r : ℝ
hr₀ : 0 < r
hr : closedBall x r ⊆ Fᶜ
⊢ ∃ r, closedBall x ↑r ⊆ Fᶜ
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
⊢ range ⇑(orthonormalBasisSingleton ι 𝕜 h v hv) = {v}

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ 0 < 1 / ↑n ^ card ι

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
n : ι
⊢ 0 n - ∑ i < n, (𝕜 ∙ gramSchmidt 𝕜 0 i).starProjection (0 n) = 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
⊢ ∀ {j i : ι}, i ≤ j → gramSchmidt 𝕜 f i ∈ span 𝕜 (f '' Set.Iic j)

Tactic:
intro j

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
j : ι
⊢ ∀ {i : ι}, i ≤ j → gramSchmidt 𝕜 f i ∈ span 𝕜 (f '' Set.Iic j)
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i : ι
⊢ ∀ x ∈ Finset.Iio i, (𝕜 ∙ gramSchmidt 𝕜 f x).starProjection (f i) = 0

Tactic:
intro j

Goal state after:
case e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i j : ι
⊢ j ∈ Finset.Iio i → (𝕜 ∙ gramSchmidt 𝕜 f j).starProjection (f i) = 0
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i : ι
⊢ f i - 0 = f i

Tactic:
simp

Goal state after: