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

Tactic:
mul_smul,

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

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
u : ↥K
v : E
⊢ (starRingEnd 𝕜) ⟪K.orthogonalProjectionOnto v, u⟫ = ⟪↑u, v⟫
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ A.transposeᵣ i j = Aᵀ i j

Tactic:
by
      simp_rw [transposeᵣ, transposeᵣ_eq]
      refine i.cases ?_ fun i => ?_
      · dsimp
        rw [FinVec.map_eq, Function.comp_apply]
      · simp only [of_apply, Matrix.cons_val_succ]
        rfl

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝¹³ : DecidableEq n
inst✝¹² : Fintype n
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra R B
inst✝⁶ : StarRing A
inst✝⁵ : StarRing B
inst✝⁴ : StarRing R
inst✝³ : StarModule R A
inst✝² : StarModule R B
m : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U : Matrix m m A
V : Matrix n n B
hU : U ∈ unitary (Matrix m m A)
hV : V ∈ unitary (Matrix n n B)
⊢ U ⊗ₖₜ[R] V ∈ unitary (Matrix (m × n) (m × n) (A ⊗[R] B))

Tactic:
simp_rw [Unitary.mem_iff, star_eq_conjTranspose] at hU hV ⊢

Goal state after:
n : Type u
inst✝¹³ : DecidableEq n
inst✝¹² : Fintype n
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra R B
inst✝⁶ : StarRing A
inst✝⁵ : StarRing B
inst✝⁴ : StarRing R
inst✝³ : StarModule R A
inst✝² : StarModule R B
m : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U : Matrix m m A
V : Matrix n n B
hU : Uᴴ * U = 1 ∧ U * Uᴴ = 1
hV : Vᴴ * V = 1 ∧ V * Vᴴ = 1
⊢ (U ⊗ₖₜ[R] V)ᴴ * U ⊗ₖₜ[R] V = 1 ∧ U ⊗ₖₜ[R] V * (U ⊗ₖₜ[R] V)ᴴ = 1
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 α
A : ↥(unitaryGroup n α)
x : n → α
⊢ (toLin' (A⁻¹ * A)) x = x

Tactic:
inv_mul_cancel,

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ (toLin' 1) x = x
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
a b c d : R
⊢ !![a, b; c, d] ∈ specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1

Tactic:
by
  trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧
    c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
  · simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff,
      ← Matrix.ext_iff, Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
  grind

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 α
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
by
    rcases p.dichotomy with (rfl | h)
    · rw [edist_eq_iSup, dist_eq_iSup]
      cases isEmpty_or_nonempty ι
      · simp
      · refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_
        have : BddAbove <| .range fun i ↦ dist (f i) (g i) := Finite.bddAbove_range _
        simp [ciSup_le_iff this]
    · have : 0 < p.toReal := by rw [ENNReal.toReal_pos_iff_ne_top]; rintro rfl; norm_num at h
      simp only [edist_eq_sum, edist_dist, dist_eq_sum, this]
      rw [← ENNReal.ofReal_rpow_of_nonneg (by simp [Finset.sum_nonneg, Real.rpow_nonneg]) (by simp)]
      simp [Real.rpow_nonneg, ENNReal.ofReal_sum_of_nonneg, ← ENNReal.ofReal_rpow_of_nonneg]

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

Goal state before:
pp: case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
x✝¹ x✝ : WithLp p (WithLp p (α × β) × γ)
hp : 0 < p.toReal
⊢ edist ((fun x ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x✝¹)
      ((fun x ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x✝) =
    edist x✝¹ x✝

Tactic:
simp [WithLp.prod_edist_eq_add hp, ENNReal.rpow_inv_rpow hp.ne', add_assoc]

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 β
⊢ ‖x‖ = √(∑ i, ‖x.ofLp i‖ ^ 2)

Tactic:
norm_eq_of_nat 2 (by norm_cast) _

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)
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 ∈ Icc 0 1, ∀ (i : ι), (b.repr x) i = ∑ x, if x = i then t x else 0) ↔ ∀ (i : ι), (b.repr x) i ∈ Icc 0 1

Tactic:
Finset.sum_ite_eq',

Goal state after:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t ∈ Icc 0 1, ∀ (i : ι), (b.repr x) i = if i ∈ Finset.univ then t i else 0) ↔ ∀ (i : ι), (b.repr x) i ∈ Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case neg
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ volume s ≤ ediam s

Tactic:
rw [Metric.ediam_of_unbounded hs]; exact le_top

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✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
h : dist x y = 0
⊢ x = y

Tactic:
by
    rw [dist_pseudoMetricSpaceToPi] at h
    apply eq_of_dist_eq_zero at h
    exact WithLp.toLp_injective p h

Goal state after:
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
r : ℝ
hr : r ≠ 0
s : Set E
⊢ (map (fun x ↦ r • x) μ) s = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| * μ s

Tactic:
by
      rw [map_addHaar_smul μ hr, coe_smul, Pi.smul_apply, smul_eq_mul]

Goal state after:
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
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
⊢ (↑(Submodule.map (span ℤ s).mkQ L)).Finite

Tactic:
show span ℤ s = span ℤ (Set.range b) by simp [b, Basis.coe_mk, Subtype.range_coe_subtype]

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
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
⊢ (↑(Submodule.map (span ℤ (Set.range ⇑b)).mkQ L)).Finite
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
a b : ι → ℕ → ℝ
ha_anti : ∀ (i : ι), StrictAnti (a i)
hb_mono : ∀ (i : ι), StrictMono (b i)
ha_mem : ∀ (i : ι) (k : ℕ), a i k ∈ Ioo (I.lower i) (I.upper i)
hb_mem : ∀ (i : ι) (l : ℕ), b i l ∈ Ioo (I.lower i) (I.upper i)
hab : ∀ (i : ι) (k l : ℕ), a i k < b i l
ha_tendsto : ∀ (i : ι), Tendsto (a i) atTop (𝓝 (I.lower i))
hb_tendsto : ∀ (i : ι), Tendsto (b i) atTop (𝓝 (I.upper i))
⊢ ∃ J,
    (∀ (n : ℕ), Box.Icc (J n) ⊆ Box.Ioo I) ∧
      Tendsto (lower ∘ ⇑J) atTop (𝓝 I.lower) ∧ Tendsto (upper ∘ ⇑J) atTop (𝓝 I.upper)

Tactic:
exact
    ⟨⟨fun k ↦ ⟨flip a k, flip b k, fun i ↦ hab _ _ _⟩, fun k l hkl ↦
        le_iff_bounds.2 ⟨fun i ↦ (ha_anti i).antitone hkl, fun i ↦ (hb_mono i).monotone hkl⟩⟩,
      fun n x hx i _ ↦ ⟨(ha_mem _ _).1.trans_le (hx.1 _), (hx.2 _).trans_lt (hb_mem _ _).2⟩,
      tendsto_pi_nhds.2 ha_tendsto, tendsto_pi_nhds.2 hb_tendsto⟩

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion

Tactic:
simp [disjUnion, Prepartition.iUnion, iUnion_or, iUnion_union_distrib]

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

Goal state before:
pp: case 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 : E
i : ι
⊢ ‖⟪x, b i⟫‖ ^ 2 = ‖⟪b i, x⟫‖ ^ 2

Tactic:
← inner_conj_symm,

Goal state after:
case 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 : E
i : ι
⊢ ‖(starRingEnd 𝕜) ⟪b i, x⟫‖ ^ 2 = ‖⟪b i, x⟫‖ ^ 2
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case inl
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ J.lower i
⊢ ↑J = J.splitUpper i x

pp: case inr
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : J.upper i ≤ x
⊢ ↑J = J.splitLower i x

Tactic:
· rwa [eq_comm, Box.splitUpper_eq_self]

Goal state after:
case inr
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : J.upper i ≤ x
⊢ ↑J = J.splitLower i x
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case e'_3.e'_4
ι : 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 : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun x)
q : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun y)
key : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x = ∑ i, p.ofLp i • v i

Tactic:
← v.equivFun.symm_apply_apply x,

Goal state after:
case e'_3.e'_4
ι : 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 : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun x)
q : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun y)
key : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ v.equivFun.symm (v.equivFun x) = ∑ i, p.ofLp i • v i
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
this✝ : Module.Finite ℤ ↥L
this : Free ℤ ↥L
⊢ Basis ι K E

Tactic:
let e := (Free.chooseBasis ℤ L).indexEquiv b

Goal state after:
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
this✝ : Module.Finite ℤ ↥L
this : Free ℤ ↥L
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := (Free.chooseBasis ℤ ↥L).indexEquiv b
⊢ Basis ι K E
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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
this✝¹ : Module.Finite ℤ ↥L
this✝ : Free ℤ ↥L
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := (Free.chooseBasis ℤ ↥L).indexEquiv b
this : Fintype ι
⊢ ⊤ ≤ span K (Set.range (⇑L.subtype ∘ ⇑b))

pp: case refine_2
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
this✝¹ : Module.Finite ℤ ↥L
this✝ : Free ℤ ↥L
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := (Free.chooseBasis ℤ ↥L).indexEquiv b
this : Fintype ι
⊢ Fintype.card ι = finrank K E

Tactic:
· rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top,
      range_subtype, top_le_iff, hs.span_top]

Goal state after:
case refine_2
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
this✝¹ : Module.Finite ℤ ↥L
this✝ : Free ℤ ↥L
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := (Free.chooseBasis ℤ ↥L).indexEquiv b
this : Fintype ι
⊢ Fintype.card ι = finrank K E
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 ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ ((a.toBasis.toMatrix ⇑b)ᴴ * a.toBasis.toMatrix ⇑b) i j = 1 i j

Tactic:
convert! a.repr.inner_map_map (b i) (b j)

Goal state after:
case e'_2
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ ((a.toBasis.toMatrix ⇑b)ᴴ * a.toBasis.toMatrix ⇑b) i j = ⟪a.repr (b i), a.repr (b j)⟫

case e'_3
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ 1 i j = ⟪b i, b j⟫
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)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

Tactic:
obtain ⟨δ, δ0, hδ⟩ : ∃ r > 0, K ⊆ S r := by
    obtain ⟨T, Tb, Tfin, hT⟩ := comp.elim_finite_subcover_image S_open S_cover
    by_cases T_nonempty : T.Nonempty
    · use Tfin.isWF.min T_nonempty, Tb (Tfin.isWF.min_mem T_nonempty)
      intro x hx
      obtain ⟨r, hr⟩ := mem_iUnion.1 (hT hx)
      simp only [mem_iUnion, exists_prop] at hr
      exact (S_antitone _ r (IsWF.min_le Tfin.isWF T_nonempty hr.1)) hr.2
    · rw [not_nonempty_iff_eq_empty] at T_nonempty
      use 1, one_pos, subset_trans hT (by simp [T_nonempty])

Goal state after:
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)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: 𝕜 : Type u_7
E : Type u_8
F : Type u_9
ι : Type u_10
ι' : Type u_11
inst✝⁷ : RCLike 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
x : E
y : F
b : Basis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 F
this : Fintype ι
⊢ Matrix.vecMulVec ⇑(b.repr x) ⇑(OrthonormalBasis.singleton Unit 𝕜).toBasis *
      (toMatrix b'.toBasis (OrthonormalBasis.singleton Unit 𝕜).toBasis) ↑((innerSL 𝕜) y) =
    Matrix.vecMulVec (⇑(b.repr x)) (star (b'.repr y).ofLp)

Tactic:
toLinearMap_innerSL_apply,

Goal state after:
𝕜 : Type u_7
E : Type u_8
F : Type u_9
ι : Type u_10
ι' : Type u_11
inst✝⁷ : RCLike 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
x : E
y : F
b : Basis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 F
this : Fintype ι
⊢ Matrix.vecMulVec ⇑(b.repr x) ⇑(OrthonormalBasis.singleton Unit 𝕜).toBasis *
      (toMatrix b'.toBasis (OrthonormalBasis.singleton Unit 𝕜).toBasis) ((innerₛₗ 𝕜) y) =
    Matrix.vecMulVec (⇑(b.repr x)) (star (b'.repr y).ofLp)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
x✝ : ∃ x ∈ ↑(box n ν), x ∈ ↑(box n ν')
x : ι → ℝ
hx : x ∈ ↑(box n ν)
hx' : x ∈ ↑(box n ν')
⊢ ν = ν'

Tactic:
rw [← mem_box_iff_index.mp hx, ← mem_box_iff_index.mp hx']

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

Goal state before:
pp: case neg
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ¬∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B

Tactic:
dif_neg hI

Goal state after:
case neg
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ¬∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ ⋯.choose ∈ Box.Icc B
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ J ∈ (prepartition n B).boxes, (volume.toBoxAdditive.toSMul J) (s.indicator F ((prepartition n B).tag J)) =
    (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ card ι

Tactic:
rw [tsum_fintype, Finset.sum_set_coe, Finset.sum_div, eq_comm]

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ J ∈ (prepartition n B).boxes, (volume.toBoxAdditive.toSMul J) (s.indicator F ((prepartition n B).tag J))
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
x : ι → ℝ
⊢ ∃ r, closedBall x ↑r ⊆ U (N x)

Tactic:
obtain ⟨r, hr₀, hr⟩ := nhds_basis_closedBall.mem_iff.1 ((hUo _).mem_nhds (hNU _ rfl))

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
x : ι → ℝ
r : ℝ
hr₀ : 0 < r
hr : closedBall ?m.309 r ⊆ U (N ?m.309)
⊢ ∃ r, closedBall x ↑r ⊆ U (N x)