mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
x✝¹ x✝ : WithLp p (α × β)
⊢ edist ((WithLp.congr p (Equiv.prodComm α β)).toFun x✝¹) ((WithLp.congr p (Equiv.prodComm α β)).toFun x✝) =
    edist x✝¹ x✝

Tactic:
rcases p.trichotomy with rfl | rfl | hp

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
hp : Fact (1 ≤ 0)
__spread✝⁻⁰ : WithLp 0 (α × β) ≃ WithLp 0 (β × α) := WithLp.congr 0 (Equiv.prodComm α β)
x✝¹ x✝ : WithLp 0 (α × β)
⊢ edist ((WithLp.congr 0 (Equiv.prodComm α β)).toFun x✝¹) ((WithLp.congr 0 (Equiv.prodComm α β)).toFun x✝) =
    edist x✝¹ x✝

case inr.inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
hp : Fact (1 ≤ ∞)
__spread✝⁻⁰ : WithLp ∞ (α × β) ≃ WithLp ∞ (β × α) := WithLp.congr ∞ (Equiv.prodComm α β)
x✝¹ x✝ : WithLp ∞ (α × β)
⊢ edist ((WithLp.congr ∞ (Equiv.prodComm α β)).toFun x✝¹) ((WithLp.congr ∞ (Equiv.prodComm α β)).toFun x✝) =
    edist x✝¹ x✝

case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
x✝¹ x✝ : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist ((WithLp.congr p (Equiv.prodComm α β)).toFun x✝¹) ((WithLp.congr p (Equiv.prodComm α β)).toFun x✝) =
    edist x✝¹ x✝
Module: Mathlib.Analysis.Normed.Lp.ProdLp

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

Tactic:
rcases p.trichotomy with rfl | rfl | hp

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
hp : Fact (1 ≤ 0)
x✝¹ x✝ : WithLp 0 (WithLp 0 (α × β) × γ)
⊢ edist ((fun x ↦ WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd))) x✝¹)
      ((fun x ↦ WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd))) x✝) =
    edist x✝¹ x✝

case inr.inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
hp : Fact (1 ≤ ∞)
x✝¹ x✝ : WithLp ∞ (WithLp ∞ (α × β) × γ)
⊢ edist ((fun x ↦ WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd))) x✝¹)
      ((fun x ↦ WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd))) x✝) =
    edist x✝¹ x✝

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
x y : WithLp p (α × β)
⊢ edist x.fst y.fst = edist x y

Tactic:
rcases p.trichotomy with rfl | rfl | hp

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
hp : Fact (1 ≤ 0)
__spread✝⁻⁰ : WithLp 0 (α × β) ≃ α := (WithLp.equiv 0 (α × β)).trans (Equiv.prodUnique α β)
x y : WithLp 0 (α × β)
⊢ edist x.fst y.fst = edist x y

case inr.inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
hp : Fact (1 ≤ ∞)
__spread✝⁻⁰ : WithLp ∞ (α × β) ≃ α := (WithLp.equiv ∞ (α × β)).trans (Equiv.prodUnique α β)
x y : WithLp ∞ (α × β)
⊢ edist x.fst y.fst = edist x y

case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist x.fst y.fst = edist x y
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ∞
x y : PiLp p β
⊢ dist x y = (∑ i, dist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
exact dist_eq_sum (p.toReal_pos_iff_ne_top.mpr hp) _ _

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (ofReal |(Matrix.diagonal D).det| • Measure.map (⇑(toLin' (Matrix.diagonal D))) volume) (univ.pi s) =
    ∏ i, volume (s i)

Tactic:
simp only [det_diagonal, Measure.coe_smul, smul_eq_mul, Pi.smul_apply]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal |∏ i, D i| * (Measure.map (⇑(toLin' (Matrix.diagonal D))) volume) (univ.pi s) = ∏ x, volume (s x)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p✝ : ℝ≥0∞
𝕜 : Type u_1
ι✝ : Type u_2
α✝ : ι✝ → Type u_3
β : ι✝ → Type u_4
hp : Fact (1 ≤ p✝)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : Fintype ι
inst✝² : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝¹ : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
⊢ ‖((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
            LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
          (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))).symm)
        ((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd)).symm x)‖₊ =
    ‖(WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd)).symm x‖₊

Tactic:
WithLp.linearEquiv_symm_apply

Goal state after:
p✝ : ℝ≥0∞
𝕜 : Type u_1
ι✝ : Type u_2
α✝ : ι✝ → Type u_3
β : ι✝ → Type u_4
hp : Fact (1 ≤ p✝)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : Fintype ι
inst✝² : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝¹ : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
⊢ ‖((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
            LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
          (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))).symm)
        ((WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x)‖₊ =
    ‖(WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x‖₊
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
⊢ ∃ t, (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a

Tactic:
refine ⟨fun i => x i / a i, fun i => ?_, funext fun i => ?_⟩

Goal state after:
case mpr.refine_1
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
i : ι
⊢ 0 ≤ (fun i ↦ x i / a i) i ∧ (fun i ↦ x i / a i) i ≤ 1

case mpr.refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
i : ι
⊢ x i = ((fun i ↦ x i / a i) • a) i
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖

Tactic:
toLp_add,

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖

Tactic:
toLp_add,

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A✝ : Bornology.IsBounded (range fun n ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
⊢ c ^ n - c ^ m ≠ 0

Tactic:
simpa only [sub_eq_zero, Ne] using (pow_right_strictAnti₀ cpos cone).injective.ne hmn.symm

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 : fract b a✝ = fract b b✝
⊢ -a✝ + b✝ ∈ (span ℤ (Set.range ⇑b)).toAddSubgroup

Tactic:
mem_toAddSubgroup,

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✝ ∈ span ℤ (Set.range ⇑b)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
⊢ ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x

Tactic:
rw [ae_ball_iff A_count]

Goal state after:
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
⊢ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ T i → p x
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x

Tactic:
filter_upwards [M, M'] with x hx h'x

Goal state after:
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
⊢ x ∈ s → p x
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
h : r ≠ 0
⊢ μ (sphere x r) = 0

Tactic:
exact addHaar_sphere_of_ne_zero μ x h

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)

Tactic:
by
  set t' := R⁻¹ • t with ht'
  set u' := R⁻¹ • u with hu'
  have A : Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0) := by
    apply tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 μ s x h t' u'
    · simp only [u', h'u, (pow_pos Rpos _).ne', abs_nonpos_iff, addHaar_smul, not_false_iff,
        ENNReal.ofReal_eq_zero, inv_eq_zero, inv_pow, Ne, or_self_iff, mul_eq_zero]
    · refine (smul_set_mono t_bound).trans_eq ?_
      rw [smul_closedBall _ _ Rpos.le, smul_zero, Real.norm_of_nonneg (inv_nonneg.2 Rpos.le),
        inv_mul_cancel₀ Rpos.ne']
  have B : Tendsto (fun r : ℝ => R * r) (𝓝[>] 0) (𝓝[>] (R * 0)) := by
    apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
    · exact (tendsto_const_nhds.mul tendsto_id).mono_left nhdsWithin_le_nhds
    · filter_upwards [self_mem_nhdsWithin]
      intro r rpos
      rw [mul_zero]
      exact mul_pos Rpos rpos
  rw [mul_zero] at B
  apply (A.comp B).congr' _
  filter_upwards [self_mem_nhdsWithin]
  rintro r -
  have T : (R * r) • t' = r • t := by
    rw [mul_comm, ht', smul_smul, mul_assoc, mul_inv_cancel₀ Rpos.ne', mul_one]
  have U : (R * r) • u' = r • u := by
    rw [mul_comm, hu', smul_smul, mul_assoc, mul_inv_cancel₀ Rpos.ne', mul_one]
  dsimp
  rw [T, U]

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

Goal state before:
pp: ⊢ Henstock ≤ Riemann

Tactic:
by trivial

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

Goal state before:
pp: ⊢ Henstock ≤ McShane

Tactic:
by trivial

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : NormedField K
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
L : Submodule ℤ E
hL : span K ↑L = ⊤
e : F →ₗ[K] E
he : ↑L ⊆ ↑e.range
⊢ span K (⇑e ⁻¹' ↑L) = ⊤

Tactic:
Submodule.span_preimage_eq (Submodule.nonempty L) he,

Goal state after:
K : Type u_1
inst✝⁴ : NormedField K
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
L : Submodule ℤ E
hL : span K ↑L = ⊤
e : F →ₗ[K] E
he : ↑L ⊆ ↑e.range
⊢ comap e (span K ↑L) = ⊤
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

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

Tactic:
simpa only [ofPred_exists] using! hasBasis_iSup (l.hasBasis_toFilterDistortion I)

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hD : D ∈ 𝓝 x
⊢ oscillationWithin f D x = oscillation f x

Tactic:
by
  rw [oscillation, oscillationWithin, nhdsWithin_eq_nhds.2 hD]

Goal state after:
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 < ↑ε
⊢ ∃ 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:
rw [NNReal.coe_pos] at ε0

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 < ε
⊢ ∃ 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
ν : ι → ℤ
x : ι → ℝ
⊢ x ∈ box n ν ↔ ∀ (i : ι), ↑(ν i) < ↑n * x i ∧ ↑n * x i ≤ ↑(ν i) + 1

Tactic:
have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
  simp_rw [mem_box_iff, ← _root_.le_div_iff₀' h, ← div_lt_iff₀' h]

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

Goal state before:
pp: case neg.h
𝕜 : 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
h : ¬gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 ≠ 0

Tactic:
inner_self_ne_zero

Goal state after:
case neg.h
𝕜 : 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
h : ¬gramSchmidt 𝕜 f a = 0
⊢ gramSchmidt 𝕜 f a ≠ 0
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

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

Tactic:
refine Finset.sum_bij (fun x _ ↦ box n (index n x)) (fun _ hx ↦ Finset.mem_filter.mpr ?_)
    (fun _ hx _ hy h ↦ ?_) (fun I hI ↦ ?_) (fun _ hx ↦ ?_)

Goal state after:
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 ℝ ι)))).toFinset
⊢ box n (index n x✝) ∈ (prepartition n B).boxes ∧ (prepartition n B).tag (box n (index n x✝)) ∈ s

case refine_2
ι : 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 ℝ ι)))).toFinset
x✝ : ι → ℝ
hy : x✝ ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset
h : box n (index n x✝¹) = box n (index n x✝)
⊢ x✝¹ = x✝

case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
I : Box ι
hI : I ∈ {x ∈ (prepartition n B).boxes | (prepartition n B).tag x ∈ s}
⊢ ∃ a, ∃ (_ : a ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset), box n (index n a) = I

case refine_4
ι : 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 ℝ ι)))).toFinset
⊢ F x✝ / ↑n ^ card ι = volume.real ↑(box n (index n x✝)) * F ((prepartition n B).tag (box n (index n x✝)))