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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
c : 𝕜
hc : (starRingEnd 𝕜) c = c
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ (c • T).IsSymmetric

Tactic:
by
  intro x y
  simp only [smul_apply, inner_smul_left, hc, hT x y, inner_smul_right]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
h : U ⟂ V
x y : E
⊢ ⟪(U.subtype ∘ₗ U.projectionOnto V hUV) x, y⟫ =
    ⟪(U.projection V hUV) x + (V.projection U ⋯) x, (U.subtype ∘ₗ U.projectionOnto V hUV) y⟫

Tactic:
nth_rw 1 [← projection_add_projection_eq_self hUV y]

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
h : U ⟂ V
x y : E
⊢ ⟪(U.subtype ∘ₗ U.projectionOnto V hUV) x, (U.projection V hUV) y + (V.projection U ⋯) y⟫ =
    ⟪(U.projection V hUV) x + (V.projection U ⋯) x, (U.subtype ∘ₗ U.projectionOnto V hUV) y⟫
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : K.HasOrthogonalProjection
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
v : E'
w : E
hwK : w ∈ K
hw : f.symm v - w ∈ Kᗮ
⊢ ∃ w ∈ map (↑f.toLinearEquiv) K, v - w ∈ (map (↑f.toLinearEquiv) K)ᗮ

Tactic:
refine ⟨f w, Submodule.mem_map_of_mem hwK, Set.forall_mem_image.2 fun u hu ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : K.HasOrthogonalProjection
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
v : E'
w : E
hwK : w ∈ K
hw : f.symm v - w ∈ Kᗮ
u : E
hu : u ∈ ↑K
⊢ ⟪↑f.toLinearEquiv u, v - f w⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case hbc
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ ‖K.orthogonalProjectionOnto‖ ≤ 1

Tactic:
exact orthogonalProjectionOnto_norm_le K

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case of.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ 0 = (DFinsupp.single j x) i

pp: case of.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ ↑x ∈ (V i)ᗮ

Tactic:
DFinsupp.single_eq_of_ne hij

Goal state after:
case of.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ 0 = 0

case of.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ ↑x ∈ (V i)ᗮ
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ (edist x.fst y.fst ^ p.toReal) ^ (1 / p.toReal)

Tactic:
simp only [← ENNReal.rpow_mul, cancel, ENNReal.rpow_one, le_refl]

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

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.snd y.snd ≤ (edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
simp only [← ENNReal.rpow_mul, cancel, ENNReal.rpow_one, le_refl]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
⊢ ∃ u ⊇ v, Orthonormal 𝕜 Subtype.val ∧ u ≠ v

Tactic:
have he : ‖e‖ = 1 := by simp [e, norm_smul_inv_norm hx]

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
⊢ ∃ u ⊇ v, Orthonormal 𝕜 Subtype.val ∧ u ≠ v
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ volume (Icc (sInf s) (sSup s))

Tactic:
exact volume.mono hs.subset_Icc_sInf_sSup

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

Goal state before:
pp: p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < volume {x | p x}

Tactic:
grw [← hs]

Goal state after:
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < volume (Ioo l u)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
⊢ volume (ball a r) = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
simp only [MeasureTheory.volume_pi_ball a hr, volume_ball, Finset.prod_const]
  exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr.le) _).symm

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

Goal state before:
pp: 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

Tactic:
change ∀ x : ι ⊕ ι', Sum.elim t s x ≤ 1
      aesop

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p ↦ Real.le✝ p.2 (g p.1)) (μ.prod volume)

Tactic:
· change NullMeasurableSet {p : α × ℝ | p.snd ≤ g p.fst} (μ.prod volume)
    rw [show {p : α × ℝ | p.snd ≤ g p.fst} = {p : α × ℝ | g p.fst < p.snd}ᶜ by
          ext p
          simp]
    exact (nullMeasurableSet_lt (by fun_prop) measurable_snd.aemeasurable).compl

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

Goal state before:
pp: case refine_2.h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
a✝ b✝ : E
hxy : ⟦a✝⟧.liftOn (fractRestrict b) ⋯ = ⟦b✝⟧.liftOn (fractRestrict b) ⋯
⊢ ⟦a✝⟧ = ⟦b✝⟧

Tactic:
rw [Quotient.liftOn_mk (s := quotientRel (span ℤ (Set.range b))), fractRestrict,
      Quotient.liftOn_mk (s := quotientRel (span ℤ (Set.range b))), fractRestrict,
      Subtype.mk.injEq] at hxy

Goal state after:
case refine_2.h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
a✝ b✝ : E
hxy : fract b a✝ = fract b b✝
⊢ ⟦a✝⟧ = ⟦b✝⟧
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_1.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
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 ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ span ℤ s ≤ L

Tactic:
exact span_le.mpr h_incl

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'
ι : Type u_7
inst✝² : Fintype ι
f : ι → Type u_8
inst✝¹ : (i : ι) → NormedAddCommGroup (f i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (f i)
x y : PiLp 2 f
⊢ (starRingEnd 𝕜) (∑ i, (inst✝ i).toInner.1 (y.ofLp i) (x.ofLp i)) = ∑ i, (inst✝ i).toInner.1 (x.ofLp i) (y.ofLp i)

Tactic:
map_sum

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁹ : RCLike 𝕜
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type u_6
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
ι : Type u_7
inst✝² : Fintype ι
f : ι → Type u_8
inst✝¹ : (i : ι) → NormedAddCommGroup (f i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (f i)
x y : PiLp 2 f
⊢ ∑ x_1, (starRingEnd 𝕜) ((inst✝ x_1).toInner.1 (y.ofLp x_1) (x.ofLp x_1)) =
    ∑ i, (inst✝ i).toInner.1 (x.ofLp i) (y.ofLp i)
Module: Mathlib.Analysis.InnerProductSpace.PiL2

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

Tactic:
PiLp.single_apply

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ∀ (i j : ι), True
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 y : E
this : ((innerSL 𝕜) x) (∑ i, (b.repr y).ofLp i • b i) = ((innerSL 𝕜) x) y
⊢ ∑ i, ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, y⟫

Tactic:
map_sum

Goal state after:
ι : 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
⊢ ∑ i, ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, y⟫
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, ‖⟪b i, x⟫‖ ^ 2 = √(re (∑ i, ⟪x, b i⟫ * ⟪b i, x⟫)) ^ 2

Tactic:
map_sum

Goal state after:
ι : 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, ‖⟪b i, x⟫‖ ^ 2 = √(∑ x_1, re (⟪x, b x_1⟫ * ⟪b x_1, x⟫)) ^ 2
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, ‖⟪b i, x⟫‖ ^ 2 = ‖x‖ ^ 2

Tactic:
rw [@norm_eq_sqrt_re_inner 𝕜, ← OrthonormalBasis.sum_inner_mul_inner b x x, map_sum]
  simp_rw [inner_mul_symm_re_eq_norm, norm_mul, ← inner_conj_symm x, starRingEnd_apply,
    norm_star, ← pow_two]
  rw [Real.sq_sqrt]
  exact Fintype.sum_nonneg fun _ ↦ by positivity

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
i : ι
⊢ inner ℝ ((basisFun ι ℝ) i) x = x.ofLp i

Tactic:
basisFun_inner

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
i : ι
⊢ x.ofLp i = x.ofLp i
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 : ι ≃ ι'
x : E
⊢ (b.equiv b' e) (∑ i, (b.repr x).ofLp i • b i) = ∑ i, (b.repr x).ofLp i • b' (e i)

Tactic:
map_sum

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 ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
x : E
⊢ ∑ x_1, (b.equiv b' e) ((b.repr x).ofLp x_1 • b x_1) = ∑ i, (b.repr x).ofLp i • b' (e i)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : TopologicalSpace F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
x : E
x' : ↥L := b.repr.symm (Finsupp.equivFunOnFinite.symm fun i ↦ ⌊((Basis.ofZLatticeBasis ℝ L b).repr x) i⌋)
⊢ x + -↑x' ∈ ↑(Basis.ofZLatticeBasis ℝ L b).parallelepiped

Tactic:
simp [parallelepiped_basis_eq, x', Int.floor_le, Int.lt_floor_add_one, le_of_lt, add_comm (1 : ℝ)]

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:
i

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.LinearAlgebra.Orientation

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : M [⋀^ι]→ₗ[R] R
hx✝ : x ≠ 0
hx : x ⇑e ≠ 0
⊢ rayOfNeZero R x hx✝ = e.orientation ∨ rayOfNeZero R x hx✝ = -e.orientation

Tactic:
rwa [Basis.orientation, ray_eq_iff, neg_rayOfNeZero, ray_eq_iff, x.eq_smul_basis_det e,
    sameRay_neg_smul_left_iff_of_ne e.det_ne_zero hx, sameRay_smul_left_iff_of_ne e.det_ne_zero hx,
    lt_or_lt_iff_ne, ne_comm]

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

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
by_cases hfi : Integrable.{u, v, v} I l f μ.toBoxAdditive.toSMul

Goal state after:
case pos
ι : Type u
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul

case neg
ι : Type u
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : ¬Integrable I l f μ.toBoxAdditive.toSMul
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis ↥w ℝ E
_hw : ⇑b = Subtype.val
⊢ map (⇑f) b.toBasis.addHaar = (b.map f).toBasis.addHaar

Tactic:
Basis.map_addHaar _ f.toContinuousLinearEquiv

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis ↥w ℝ E
_hw : ⇑b = Subtype.val
⊢ (b.toBasis.map ↑↑f).addHaar = (b.map f).toBasis.addHaar
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this : IntegrableOn f (↑I) μ
⊢ ∫ (x : ι → ℝ) in ↑I, f x ∂μ = y

Tactic:
exact HasIntegral.unique (IntegrableOn.hasBoxIntegral this ⊥ rfl) (HasIntegral.mono hy bot_le)

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n ↦ ∑ i ∈ Finset.range n, (u i - l)) =o[atTop] fun n ↦ ↑n
⊢ (fun x ↦ (↑x)⁻¹ • ↑x) =ᶠ[atTop] fun _x ↦ 1

Tactic:
filter_upwards [Ici_mem_atTop 1] with n npos
    have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
    rw [smul_eq_mul, inv_mul_cancel₀ nposℝ.ne']

Goal state after:
Module: Mathlib.Analysis.PSeries

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

pp: case inl.h_mono
p : ℝ
hp : 0 ≤ p
⊢ ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹

Tactic:
· intro n
      positivity

Goal state after:
case inl.h_mono
p : ℝ
hp : 0 ≤ p
⊢ ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ (↑k)⁻¹ - (↑n)⁻¹ + ((↑n + 1) ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n + 1)⁻¹

Tactic:
have A : 0 < (n : α) := by simpa using hk.bot_lt.trans_le hn

Goal state after:
case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
A : 0 < ↑n
⊢ (↑k)⁻¹ - (↑n)⁻¹ + ((↑n + 1) ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n + 1)⁻¹
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x✝ x y : k[A]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}
m : A
hm : m ∈ (x • y).coeff.support
⊢ ∃ m' ∈ s, ∃ d, m = d + m'

Tactic:
by
      simp only [smul_eq_mul, mul_def, coeff_finsuppSum] at hm
      obtain ⟨xm, -, hm⟩ := Finset.mem_biUnion.mp <| Finsupp.support_sum hm
      obtain ⟨ym, hym, hm⟩ := Finset.mem_biUnion.mp <| Finsupp.support_sum hm
      obtain rfl := Finset.mem_singleton.mp <| Finsupp.support_single_subset hm
      refine (hy _ hym).imp fun sm ↦ .imp_right ?_
      rintro ⟨d, rfl⟩
      exact ⟨xm + d, (add_assoc ..).symm⟩

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
inst✝ : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ (volume {x | x ∈ X ∧ F x ≤ 1}).toReal / covolume L volume =
    (volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})).toReal

Tactic:
volume_image_eq_volume_div_covolume' L b h₃.nullMeasurableSet,

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
inst✝ : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ (volume {x | x ∈ X ∧ F x ≤ 1}).toReal / covolume L volume =
    (volume {x | x ∈ X ∧ F x ≤ 1} / ENNReal.ofReal (covolume L volume)).toReal
Module: Mathlib.Algebra.MvPolynomial.Comap

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
i : σ
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x i = x i

Tactic:
simp only [comap, AlgHom.id_apply, aeval_X]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ multinomial s f = multinomial t g

Tactic:
← Nat.mul_right_inj (prod_ne_zero_iff.mpr (fun x _ ↦ factorial_ne_zero (g x))),

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ (∏ x ∈ ?m.37, (g x)!) * multinomial s f = (∏ x ∈ ?m.37, (g x)!) * multinomial t g

α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ Finset α
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
this :
  p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)
⊢ X i ∣ p ∨ X i ∣ q

Tactic:
simp only [X_dvd_iff_modMonomial_eq_zero] at h ⊢
      rwa [h, mul_eq_zero] at this

Goal state after: