mathlib-initiative/mathlib-tactics huggingface dataset:
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 ℤ (Set.range ⇑b)) ⊆ ↑L

Tactic:
rw [SetLike.coe_subset_coe, Basis.coe_mk, Subtype.range_coe_subtype, Set.ofPred_mem_eq]

Goal state after:
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
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 ι
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
v₀ w₀ : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [LinearEquiv.trans_apply]

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'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
v₀ w₀ : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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:
by
    rintro ⟨⟨b₁, h₁le, h₁d⟩, t₁, ht₁⟩ ⟨⟨b₂, h₂le, h₂d⟩, t₂, ht₂⟩ H
    simpa using H

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

Goal state before:
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
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
⊢ finrank K ↥⊤ ≤ Fintype.card (Free.ChooseBasisIndex ℤ ↥L)

Tactic:
← h_spanE

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
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
⊢ finrank K ↥(span K (Set.range b)) ≤ Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
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 ℤ ↥(comap (Submodule.restrictScalars ℤ (span ℝ s)).subtype (span ℤ s))

Tactic:
exact (ZLattice.rank ℝ L).symm

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

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

Tactic:
· rw [orthonormal_iff_ite.mp b.orthonormal i j, Matrix.one_apply]

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✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
⊢ (a.toBasis.toMatrix ⇑b)ᴴ * a.toBasis.toMatrix ⇑b = 1

Tactic:
by
  ext i j
  convert! a.repr.inner_map_map (b i) (b j)
  · simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, star_def, PiLp.inner_apply,
      inner_apply']
    congr
  · rw [orthonormal_iff_ite.mp b.orthonormal i j, Matrix.one_apply]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
l✝ l₁ l₂ : IntegrationParams
r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
r : (ι → ℝ) → ↑(Set.Ioi 0)
l : IntegrationParams
I : Box ι
⊢ (l.toFilterDistortion I I.distortion).NeBot

Tactic:
by
  simpa using (l.toFilterDistortioniUnion_neBot' I ⊤).mono inf_le_left

Goal state after:
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 ι
⊢ (toMatrix b'.toBasis b) ↑(((rankOne 𝕜) x) y) = Matrix.vecMulVec (⇑(b.repr x)) (star (b'.repr y).ofLp)

Tactic:
rankOne_def',

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 ι
⊢ (toMatrix b'.toBasis b) ↑(ContinuousLinearMap.toSpanSingleton 𝕜 x ∘SL (innerSL 𝕜) y) =
    Matrix.vecMulVec (⇑(b.repr x)) (star (b'.repr y).ofLp)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case hbc
ι : 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
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun x ↦ π.tag x ∈ s).iUnion
⊢ |μ.real (π.filter fun i ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ ↑I)| ≤ ↑ε

Tactic:
change abs (μ.real t - μ.real (s ∩ I)) ≤ ε

Goal state after:
case hbc
ι : 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
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun x ↦ π.tag x ∈ s).iUnion
⊢ |μ.real t - μ.real (s ∩ ↑I)| ≤ ↑ε
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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
⊢ ∀ b_1 ∈ Iio b,
    b_1 ≠ a →
      ⟪gramSchmidt 𝕜 f b_1, f b⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f b_1‖ ^ 2) * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b_1⟫_𝕜 = 0

Tactic:
intro i hi hia

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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ ⟪gramSchmidt 𝕜 f i, f b⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f i‖ ^ 2) * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
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
⊢ Integrable I l f vol ↔
    ∀ ε > 0,
      ∃ r,
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
            l.MemBaseSet I c₁ (r c₁) π₁ →
              π₁.IsPartition →
                l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε

Tactic:
integrable_iff_cauchy,

Goal state after:
ι : 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
⊢ Cauchy (Filter.map (integralSum f vol) (toFilteriUnion I ⊤)) ↔
    ∀ ε > 0,
      ∃ r,
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
            l.MemBaseSet I c₁ (r c₁) π₁ →
              π₁.IsPartition →
                l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε
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
x : WithLp 2 (E × F)
⊢ ‖x‖ ^ 2 = RCLike.re (⟪x.fst, x.fst⟫_𝕜 + ⟪x.snd, x.snd⟫_𝕜)

Tactic:
simp [prod_norm_sq_eq_of_L2]

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
⊢ Fintype.card ι = n

Tactic:
← _i.out,

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
⊢ Fintype.card ι = finrank ℝ F
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
L₁ L₂ : Submodule ℤ E
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
f : (Fin (finrank ℝ E) → ℝ) ≃L[ℝ] E :=
  (EuclideanSpace.equiv (Fin (finrank ℝ E)) ℝ).symm.trans (↑(stdOrthonormalBasis ℝ E).repr).symm
hf : MeasurePreserving (⇑f) volume volume
⊢ covolume L₁ volume / covolume L₂ volume = ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)

Tactic:
rw [← covolume_comap L₁ volume volume hf, ← covolume_comap L₂ volume volume hf,
    covolume_div_covolume_eq_relIndex _ _ (fun _ h' ↦ h h'), ZLattice.comap_toAddSubgroup,
    ZLattice.comap_toAddSubgroup, Nat.cast_inj, LinearEquiv.toAddMonoidHom_commutes,
    AddSubgroup.comap_equiv_eq_map_symm', AddSubgroup.comap_equiv_eq_map_symm',
    AddSubgroup.relIndex_map_map_of_injective _ _ f.symm.injective]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
rw [← summable_condensed_iff_of_nonneg]

Goal state after:
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k ↦ 2 ^ k * (↑(2 ^ k) ^ p)⁻¹) ↔ 1 < p

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

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 inl
p : ℝ
hp : 0 ≤ p
⊢ ‖2 * (2 ^ p)⁻¹‖ < 1 ↔ 1 < p

Tactic:
← rpow_one 2

Goal state after:
case inl
p : ℝ
hp : 0 ≤ p
⊢ ‖2 ^ 1 * (2 ^ p)⁻¹‖ < 1 ↔ 1 < p
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inr
p : ℝ
hp : p < 0
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
suffices ¬Summable (fun n => ((n : ℝ) ^ p)⁻¹ : ℕ → ℝ) by
      have : ¬1 < p := fun hp₁ => hp.not_ge (zero_le_one.trans hp₁.le)
      simpa only [this, iff_false]

Goal state after:
case inr
p : ℝ
hp : p < 0
⊢ ¬Summable fun n ↦ (↑n ^ p)⁻¹
Module: Mathlib.Data.Set.SMulAntidiagonal

Goal state before:
pp: G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m))
        ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n))
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) (fun x ↦ x ∈ s.smulAntidiagonal t a)
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (?m.125 m))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (?m.125 n))
⊢ False

Tactic:
refine mn.ne (g.injective <| (h.natEmbedding _).injective ?_)

Goal state after:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m))
        ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n))
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) (fun x ↦ x ∈ s.smulAntidiagonal t a)
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (?m.125 m))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (?m.125 n))
⊢ (Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m) = (Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case e_a
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ (∑ i ∈ f.support, f i)! = (∑ i ∈ s, f i)!

pp: case e_a
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ ∏ i ∈ f.support, (f i)! = ∏ i ∈ s, (f i)!

Tactic:
· simp [Finset.sum_subset h]

Goal state after:
case e_a
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ ∏ i ∈ f.support, (f i)! = ∏ i ∈ s, (f i)!
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ m.countPerms = m.card.choose (count a m) * (filter (fun x ↦ a ≠ x) m).countPerms

Tactic:
by
  dsimp only [countPerms]
  convert! Finsupp.multinomial_update a _
  · rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]
  · ext1 a
    rw [toFinsupp_apply, count_filter, Finsupp.coe_update]
    split_ifs with h
    · rw [Function.update_of_ne h.symm, toFinsupp_apply]
    · rw [not_ne_iff.1 h, Function.update_self]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ antidiagonal n,
    ∑ g ∈ s.piAntidiag p.2,
        ↑((g a + p.1 + s.sum g).choose (g a + p.1)) * ↑(multinomial s (g + fun i ↦ if i = a then p.1 else 0)) *
          (f a ^ (g a + p.1) * s.noncommProd (fun i ↦ f i ^ (g i + if i = a then p.1 else 0)) ⋯) =
      ∑ g ∈ s.piAntidiag p.2, ↑(n.choose p.1) * ↑(multinomial s g) * (f a ^ p.1 * s.noncommProd (fun i ↦ f i ^ g i) ⋯)
⊢ ∑ m ∈ range (n + 1), f a ^ m * (∑ i ∈ s, f i) ^ (n - m) * ↑(n.choose m) =
    ∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        ↑(n.choose x) * ↑(multinomial s x_1) * (f a ^ x * s.noncommProd (fun i ↦ f i ^ x_1 i) ⋯)

Tactic:
simp only [ih (hc.mono (by simp)), sum_mul, mul_sum]

Goal state after:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ antidiagonal n,
    ∑ g ∈ s.piAntidiag p.2,
        ↑((g a + p.1 + s.sum g).choose (g a + p.1)) * ↑(multinomial s (g + fun i ↦ if i = a then p.1 else 0)) *
          (f a ^ (g a + p.1) * s.noncommProd (fun i ↦ f i ^ (g i + if i = a then p.1 else 0)) ⋯) =
      ∑ g ∈ s.piAntidiag p.2, ↑(n.choose p.1) * ↑(multinomial s g) * (f a ^ p.1 * s.noncommProd (fun i ↦ f i ^ g i) ⋯)
⊢ ∑ x ∈ range (n + 1),
      ∑ i ∈ s.piAntidiag (n - x),
        f a ^ x * (↑(multinomial s i) * s.noncommProd (fun i_1 ↦ f i_1 ^ i i_1) ⋯) * ↑(n.choose x) =
    ∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        ↑(n.choose x) * ↑(multinomial s x_1) * (f a ^ x * s.noncommProd (fun i ↦ f i ^ x_1 i) ⋯)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr.succ.refine_1.inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
hp : p ∣ (monomial n') 1 * q
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

pp: case inr.succ.refine_1.inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
hp : X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ (monomial n') 1 * q
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
· obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' p q).mp hp
        exact ⟨m, r, le_trans hm hnn', hr, hp⟩

Goal state after:
case inr.succ.refine_1.inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
hp : X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ (monomial n') 1 * q
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r