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

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

Tactic:
Finset.univ.card_image_of_injective

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
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) = ⊤
⊢ Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = Finset.univ.card

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) = ⊤
⊢ Function.Injective b
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
Ji : Box ι
hJi : Ji ∈ πi J
hlei : J' ≤ Ji
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Tactic:
exact ⟨Ji, π.mem_biUnion.2 ⟨J, hJ, hJi⟩, hlei⟩

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
x✝ : ι
⊢ 0 x✝ ≤ ‖⟪b x✝, x⟫‖ ^ 2

Tactic:
positivity

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
⊢ 0 ≤ ‖x‖

Tactic:
positivity

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 ι
⊢ 0 ≤ ‖⟪b ⋯.some, x⟫‖

Tactic:
positivity

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 ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ b.repr.symm ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e.symm) (EuclideanSpace.single i' 1)) =
    b.repr.symm (EuclideanSpace.single (e.symm i') 1)

Tactic:
EuclideanSpace.piLpCongrLeft_single

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ b.repr.symm (EuclideanSpace.single (e.symm i') 1) = b.repr.symm (EuclideanSpace.single (e.symm i') 1)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) := comap (Submodule.restrictScalars ℤ F).subtype (span ℤ s)
f : ↥(comap (Submodule.restrictScalars ℤ (span ℝ s)).subtype (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) := comapSubtypeEquivOfLe ⋯
this✝ : DiscreteTopology ↥L
this : IsZLattice ℝ L
⊢ finrank ℝ ↥(span ℝ s) = finrank ℤ ↥(span ℤ s)

Tactic:
← f.finrank_eq

Goal state after:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) := comap (Submodule.restrictScalars ℤ F).subtype (span ℤ s)
f : ↥(comap (Submodule.restrictScalars ℤ (span ℝ s)).subtype (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) := comapSubtypeEquivOfLe ⋯
this✝ : DiscreteTopology ↥L
this : IsZLattice ℝ L
⊢ finrank ℝ ↥(span ℝ s) = finrank ℤ ↥(comap (Submodule.restrictScalars ℤ (span ℝ s)).subtype (span ℤ s))
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
l : IntegrationParams
I : Box ι
⊢ (toFilteriUnion I ⊤).HasBasis (fun r ↦ ∀ (c : ℝ≥0), l.RCond (r c)) fun r ↦
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.IsPartition}

Tactic:
by
  simpa only [TaggedPrepartition.isPartition_iff_iUnion_eq, Prepartition.iUnion_top] using
    l.hasBasis_toFilteriUnion I ⊤

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν ↦ tag n ν) x✝¹ = (fun ν ↦ tag n ν) x✝
i : ι
this : (↑(x✝¹ i) + 1) / ↑n = (↑(x✝ i) + 1) / ↑n
⊢ x✝¹ i = x✝ i

Tactic:
div_left_inj' (c := (n : ℝ)) (Nat.cast_ne_zero.mpr (NeZero.ne n)),

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν ↦ tag n ν) x✝¹ = (fun ν ↦ tag n ν) x✝
i : ι
this : ↑(x✝¹ i) + 1 = ↑(x✝ i) + 1
⊢ x✝¹ i = x✝ i
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
h : 0 < ↑n
⊢ 0 < 1 / ↑n

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ 0 ≤ 1 / ↑n

Tactic:
positivity

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

Goal state before:
pp: case e'_6
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
⊢ ⟪b k, v i⟫_𝕜 / ↑‖b k‖ ^ 2 * ⟪b j, b k⟫_𝕜 = 0

Tactic:
have hki : k < i := by simpa using hki'

Goal state after:
case e'_6
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
hki : k < i
⊢ ⟪b k, v i⟫_𝕜 / ↑‖b k‖ ^ 2 * ⟪b j, b k⟫_𝕜 = 0
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case h.e_6
R : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
⊢ (fun i_1 ↦ ↑f.symm (i i_1)) = i

Tactic:
simp only [LinearEquiv.coe_coe, eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_4
ι' : Type u_5
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
e : Basis ι R M
eι : ι ≃ ι'
⊢ rayOfNeZero R (e.reindex eι).det ⋯ = (Orientation.reindex R M eι) (rayOfNeZero R e.det ⋯)

Tactic:
Orientation.reindex_apply,

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_4
ι' : Type u_5
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
e : Basis ι R M
eι : ι ≃ ι'
⊢ rayOfNeZero R (e.reindex eι).det ⋯ = rayOfNeZero R (AlternatingMap.domDomCongr eι e.det) ⋯
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
⊢ ↑⌊x⌋₊ ^ card ι ≠ 0

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
x : ℝ
hx : 1 ≤ x
⊢ ↑⌈x⌉₊ ^ card ι ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case empty
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
h : ∀ i ∈ ∅, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x ↦ ∑ i ∈ ∅, f i x) vol (∑ i ∈ ∅, g i)

Tactic:
simp [hasIntegral_zero]

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

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
⊢ (-o).volumeForm = -o.volumeForm

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Goal state after:
case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
⊢ o = positiveOrientation → (-o).volumeForm = -o.volumeForm

case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
⊢ o = -positiveOrientation → (-o).volumeForm = -o.volumeForm
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ |o.volumeForm v| = |b.toBasis.det v|

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Goal state after:
case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ o = positiveOrientation → |o.volumeForm v| = |b.toBasis.det v|

case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ o = -positiveOrientation → |o.volumeForm v| = |b.toBasis.det v|
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ 0 < finrank R M

Tactic:
rw [← h]

Goal state after:
R : Type u_1
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ 0 < Fintype.card ι
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
⊢ |o.volumeForm v| ≤ ∏ i, ‖v i‖

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Goal state after:
case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
⊢ o = positiveOrientation → |o.volumeForm v| ≤ ∏ i, ‖v i‖

case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
⊢ o = -positiveOrientation → |o.volumeForm v| ≤ ∏ i, ‖v i‖
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin n.succ
a✝ : i ∈ Finset.univ
⊢ 0 ≤ |⟪b i, v i⟫|

Tactic:
positivity

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

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
⊢ |o.volumeForm v| = ∏ i, ‖v i‖

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Goal state after:
case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
⊢ o = positiveOrientation → |o.volumeForm v| = ∏ i, ‖v i‖

case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
⊢ o = -positiveOrientation → |o.volumeForm v| = ∏ i, ‖v i‖
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x x✝ : E
⊢ 0 ≤ ‖((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm) x✝‖

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x x✝ : E
⊢ 0 ≤ ‖x✝‖

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x x✝ : E
⊢ ‖((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm) x✝‖ = ‖x✝‖

Tactic:
rw [← sq_eq_sq₀ (by positivity) (by positivity), WithLp.prod_norm_sq_eq_of_L2,
      K.norm_sq_eq_add_norm_sq_projection]
    simp [starProjection_apply_eq_isComplProjection]

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

Goal state before:
pp: case neg.e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
h : ∀ (i : Fin (n + 1)), v i ≠ 0
i : Fin n.succ
hb : b i = ‖v i‖⁻¹ • v i
⊢ 0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)

Tactic:
positivity

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

Goal state before:
pp: case zero
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
inst✝ : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ ((map (Fin 0) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Goal state after:
case zero.refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
inst✝ : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ o = positiveOrientation → ((map (Fin 0) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

case zero.refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
inst✝ : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ o = -positiveOrientation → ((map (Fin 0) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
x : Fin 0 → E
⊢ o.volumeForm (⇑φ ∘ x) = o.volumeForm x

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Goal state after:
case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
x : Fin 0 → E
⊢ o = positiveOrientation → o.volumeForm (⇑φ ∘ x) = o.volumeForm x

case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
x : Fin 0 → E
⊢ o = -positiveOrientation → o.volumeForm (⇑φ ∘ x) = o.volumeForm x
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Tendsto (integralSum f vol) (toFilteriUnion I π₀) (𝓝 (∑ J ∈ π₀.boxes, integral J l f vol))

Tactic:
by
  refine ((l.hasBasis_toFilteriUnion I π₀).tendsto_iff nhds_basis_closedBall).2 fun ε ε0 => ?_
  refine ⟨h.convergenceR ε, h.convergenceR_cond ε, ?_⟩
  simp only [mem_ofPred_eq]
  rintro π ⟨c, hc, hU⟩
  exact h.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq ε0 hc hU

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

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
A : ⇑b = ⇑(b.reindex e) ∘ ⇑e
⊢ ENNReal.ofReal 1 = 1

Tactic:
ENNReal.ofReal_one

Goal state after:
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
A : ⇑b = ⇑(b.reindex e) ∘ ⇑e
⊢ 1 = 1
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x ↦ ∑ i ∈ Finset.range N, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
n : ℕ
hn : ‖∑ i ∈ Finset.range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ Finset.range n, g i‖
⊢ n ∈ Set.Ici N → ‖∑ i ∈ Finset.range n, f i‖ ≤ ε * ‖∑ i ∈ Finset.range n, g i‖

Tactic:
Nn

Goal state after:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x ↦ ∑ i ∈ Finset.range N, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
n : ℕ
hn : ‖∑ i ∈ Finset.range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ Finset.range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i ∈ Finset.range n, f i‖ ≤ ε * ‖∑ i ∈ Finset.range n, g i‖
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl.h_nonneg
p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ 0 ≤ (↑n ^ p)⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: i : ℕ
⊢ 0 ≤ 1 / (↑i + 1)

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: ⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, 1 / (↑i + 1)) atTop atTop

Tactic:
rw [← not_summable_iff_tendsto_nat_atTop_of_nonneg]
  · exact_mod_cast mt (_root_.summable_nat_add_iff 1).1 not_summable_one_div_natCast
  · exact fun i => by positivity

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case hf
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n i : ℕ
_hi : i ∈ Ioc k (max (k + 1) n)
_hident : i ∉ Ioo k n
⊢ 0 ≤ (↑i ^ 2)⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ ∑ i ∈ Ioc k (max (k + 1) n), (↑i ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), (↑i ^ 2)⁻¹

Tactic:
rw [← Icc_add_one_left_eq_Ioc, ← Ico_add_one_right_eq_Icc, sum_eq_sum_Ico_succ_bot]

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ (↑(k + 1) ^ 2)⁻¹ + ∑ k ∈ Ico (k + 1 + 1) (max (k + 1) n + 1), (↑k ^ 2)⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), (↑i ^ 2)⁻¹

case hab
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ k + 1 < max (k + 1) n + 1
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
⊢ 0 < ε / 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
h_abs : (fun n ↦ |↑n + a|) ~[atTop] fun x ↦ ↑x
n : ℕ
⊢ 0 n ≤ ↑n

Tactic:
positivity

Goal state after: