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

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ ENNReal.ofReal |(Pi.basisFun ℝ ι).det ⇑b| * 1 = ENNReal.ofReal |(Matrix.of ⇑b).det|

Tactic:
mul_one,

Goal state after:
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ ENNReal.ofReal |(Pi.basisFun ℝ ι).det ⇑b| = ENNReal.ofReal |(Matrix.of ⇑b).det|
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ⇑((b.constr ℕ) v) '' parallelepiped ⇑b
⊢ ENNReal.ofReal |LinearMap.det ((b.constr ℕ) v)| * 1 = ENNReal.ofReal |b.det v|

Tactic:
mul_one,

Goal state after:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ⇑((b.constr ℕ) v) '' parallelepiped ⇑b
⊢ ENNReal.ofReal |LinearMap.det ((b.constr ℕ) v)| = ENNReal.ofReal |b.det v|
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
z : ι
⊢ (starRingEnd 𝕜) ((inst✝ z).toInner.1 (y.ofLp z) (x.ofLp z)) = (inst✝ z).toInner.1 (x.ofLp z) (y.ofLp z)

Tactic:
apply inner_conj_symm

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

Goal state before:
pp: ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ : J₁ ∈ π.boxes
J₂ : Box ι
h₂ : J₂ ∈ π.boxes
Hne : ↑J ⊓ ↑J₁ ≠ ↑J ⊓ ↑J₂
this : J₁ ≠ J₂
⊢ Disjoint (↑J ⊓ ↑J₁) (↑J ⊓ ↑J₂)

Tactic:
exact ((Box.disjoint_coe.2 <| π.disjoint_coe_of_mem h₁ h₂ this).inf_left' _).inf_right' _

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
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n ↦ fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_ne : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
h_nz : -↑n + ↑m ≠ 0
⊢ v ∈ span ℚ (Set.range ⇑e)

Tactic:
apply (smul_mem_iff _ h_nz).mp

Goal state after:
case refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := ⋯
b : Free.ChooseBasisIndex ℤ ↥L → E := ⋯
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n ↦ fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_ne : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
h_nz : -↑n + ↑m ≠ 0
⊢ (-↑n + ↑m) • v ∈ span ℚ (Set.range ⇑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 ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
i : ι
⊢ (b.equiv b' e) (b i) = b' (e i)

Tactic:
simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self]
  refine DFunLike.congr rfl ?_
  ext j
  simp

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

Goal state before:
pp: case hp
ι : Type u_1
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J ↦ ↑J ⊆ ↑I
⊢ ∀ J ∈ splitMany I s, ↑J ⊆ ↑I

Tactic:
exact fun J hJ => le_of_mem _ hJ

Goal state after:
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
⊢ IsCompact (Set.range f)

Tactic:
let b := Module.Free.chooseBasis ℤ L

Goal state after:
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
⊢ IsCompact (Set.range f)
Module: Mathlib.Analysis.BoxIntegral.Partition.Measure

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Box ι
x : E
⊢ (BoxAdditiveMap.volume I) x = (∏ j, (I.upper j - I.lower j)) • x

Tactic:
BoxAdditiveMap.volume,

Goal state after:
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Box ι
x : E
⊢ (volume.toBoxAdditive.toSMul I) x = (∏ j, (I.upper j - I.lower j)) • x
Module: Mathlib.Analysis.Oscillation

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

Tactic:
by_cases r_top : r = ⊤

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

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Tactic:
calc
    ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₁.boxes, ∑ J' ∈ (splitMany J s).boxes, f J' :=
      Finset.sum_congr rfl fun J hJ => (f.sum_partition_boxes ?_ (isPartition_splitMany _ _)).symm
    _ = ∑ J ∈ (π₁.biUnion fun J => splitMany J s).boxes, f J := (sum_biUnion_boxes _ _ _).symm
    _ = ∑ J ∈ (π₂.biUnion fun J => splitMany J s).boxes, f J := by rw [h₁, h₂]
    _ = ∑ J ∈ π₂.boxes, ∑ J' ∈ (splitMany J s).boxes, f J' := sum_biUnion_boxes _ _ _
    _ = ∑ J ∈ π₂.boxes, f J :=
      Finset.sum_congr rfl fun J hJ => f.sum_partition_boxes ?_ (isPartition_splitMany _ _)

Goal state after:
case calc_1
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
J : Box ι
hJ : J ∈ π₁.boxes
⊢ ↑J ≤ I₀

case calc_2
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
J : Box ι
hJ : J ∈ π₂.boxes
⊢ ↑J ≤ I₀
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: 𝕜 : Type u_3
inst✝³ : RCLike 𝕜
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L : ↥S →ₗᵢ[𝕜] V
s : ↥S
⊢ L.extend ↑s = L s

Tactic:
simp only [LinearIsometry.extend, ← LinearIsometry.coe_toLinearMap]

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

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
this : ∀ x ∈ Box.Icc I \ s, ∃ r, closedBall x ↑r ⊆ Fᶜ
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun x ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ ↑I) • y) ≤ ‖y‖ * ↑ε

Tactic:
choose! rs' hrs'F using this

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun x ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ ↑I) • y) ≤ ‖y‖ * ↑ε
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
x : ι → ℝ
hx : ∀ (i : ι), ↑n * x i ∈ Set.range ⇑(algebraMap ℤ ℝ)
i : ι
a : ℤ
ha : ↑a = ↑n * x i
⊢ ↑a / ↑n = x i

Tactic:
div_eq_iff (NeZero.ne _),

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
x : ι → ℝ
hx : ∀ (i : ι), ↑n * x i ∈ Set.range ⇑(algebraMap ℤ ℝ)
i : ι
a : ℤ
ha : ↑a = ↑n * x i
⊢ ↑a = x i * ↑n
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
⊢ (s ∩ ↑(span ℤ (Set.range ⇑((Pi.basisFun ℝ ι).isUnitSMul ⋯)))).Finite

Tactic:
exact ZSpan.setFinite_inter _ (B.isBounded.subset hs₀)

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

Goal state before:
pp: case refine_1
ι : 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 ℝ ι))))
x✝ : ι → ℝ
hx : x✝ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ x✝ ∈ s

Tactic:
hx.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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ f n ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Tactic:
gramSchmidt_def' 𝕜 f,

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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ gramSchmidt 𝕜 f n + ∑ i < n, (𝕜 ∙ gramSchmidt 𝕜 f i).starProjection (f n) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case hbc.refine_2
ι : 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
htU : t ⊆ U ∩ ↑I
⊢ μ.real (s ∩ ↑I) - μ.real t ≤ ↑ε

Tactic:
· have hμt : μ t ≠ ∞ := ((measure_mono (htU.trans inter_subset_left)).trans_lt hUt).ne
    refine (ENNReal.le_toReal_sub hμt).trans (ENNReal.toReal_le_coe_of_le_coe ?_)
    refine le_measure_sdiff.trans ((measure_mono ?_).trans hμF.le)
    rintro x ⟨⟨hxs, hxI⟩, hxt⟩
    refine ⟨⟨hxs, Box.coe_subset_Icc hxI⟩, fun hxF => hxt ?_⟩
    simp only [t, TaggedPrepartition.iUnion_def, TaggedPrepartition.mem_filter, Set.mem_iUnion]
    rcases hπp x hxI with ⟨J, hJπ, hxJ⟩
    refine ⟨J, ⟨hJπ, ?_⟩, hxJ⟩
    contrapose hxF
    refine hrs'F _ ⟨π.tag_mem_Icc J, hxF⟩ ?_
    simpa only [r, s.piecewise_eq_of_notMem _ _ hxF] using hπ.1 J hJπ (Box.coe_subset_Icc hxJ)

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

Goal state before:
pp: case e'_3
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
x✝ : ℕ
⊢ ↑(Nat.card ↑(s ∩ (↑x✝)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) =
    ↑(Nat.card ↑(s ∩ (↑x✝)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) * 1

Tactic:
mul_one,

Goal state after:
case e'_3
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
x✝ : ℕ
⊢ ↑(Nat.card ↑(s ∩ (↑x✝)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) =
    ↑(Nat.card ↑(s ∩ (↑x✝)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))))
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case intro.h
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
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ SameRay R ((g ⇑e • (LinearMap.det ↑f.symm * 1)) • e.det) (↑(LinearEquiv.det f)⁻¹ • g ⇑e • e.det)

Tactic:
mul_one,

Goal state after:
case intro.h
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
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ SameRay R ((g ⇑e • LinearMap.det ↑f.symm) • e.det) (↑(LinearEquiv.det f)⁻¹ • g ⇑e • e.det)
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
⊢ SameRay R (x ⇑e • e.det) e.det ∨ SameRay R (x ⇑e • e.det) (-e.det)

Tactic:
sameRay_neg_smul_left_iff_of_ne e.det_ne_zero hx,

Goal state after:
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
⊢ SameRay R (x ⇑e • e.det) e.det ∨ x ⇑e < 0
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A : o.volumeForm.measure ↑(stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1
⊢ o.volumeForm.measure = volume

Tactic:
addHaarMeasure_unique o.volumeForm.measure
    (stdOrthonormalBasis ℝ F).toBasis.parallelepiped,

Goal state after:
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A : o.volumeForm.measure ↑(stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1
⊢ o.volumeForm.measure ↑(stdOrthonormalBasis ℝ F).toBasis.parallelepiped •
      addHaarMeasure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped =
    volume
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
⊢ dirac (toLp 2 0) = dirac 0

Tactic:
toLp_zero

Goal state after:
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
⊢ dirac 0 = dirac 0
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
p q : ℕ
hpq : p ≤ q
⊢ (fun x ↦ x ^ p) =O[cobounded R] fun x ↦ x ^ q

Tactic:
rcases hpq.eq_or_lt with rfl | h

Goal state after:
case inl
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
p : ℕ
hpq : p ≤ p
⊢ (fun x ↦ x ^ p) =O[cobounded R] fun x ↦ x ^ p

case inr
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
p q : ℕ
hpq : p ≤ q
h : p < q
⊢ (fun x ↦ x ^ p) =O[cobounded R] fun x ↦ x ^ q
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ covolume L₁ volume / covolume L₂ volume =
    |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₂ b₂)).det⁻¹| * |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)).det|

Tactic:
covolume_eq_det _ b₁,

Goal state after:
ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ |(Matrix.of (Subtype.val ∘ ⇑b₁)).det| / covolume L₂ volume =
    |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₂ b₂)).det⁻¹| * |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)).det|
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ c⁻¹ • x ∈ X ∧ F x ≤ c ^ card ι * 1 ↔ x ∈ X ∧ F x ≤ c ^ card ι

Tactic:
mul_one,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ c⁻¹ • x ∈ X ∧ F x ≤ c ^ card ι ↔ x ∈ X ∧ F x ≤ c ^ card ι