mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inl.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ↥b.support
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inl l) = 0 (Sum.inl k) (Sum.inl l)

Tactic:
ne_comm

Goal state after:
case inl.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : j ≠ i
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ↥b.support
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inl l) = 0 (Sum.inl k) (Sum.inl l)
Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
a b : M
⊢ 2 * (B x) (a + b) = 2 * (B x) a + 2 * (B x) b

Tactic:
map_add,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
a b : M
⊢ 2 * ((B x) a + (B x) b) = 2 * (B x) a + 2 * (B x) b
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
I : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x ≡ y [SMOD I]
m : ℕ
ih : x ^ p ^ m ≡ y ^ p ^ m [SMOD I ^ (m + 1)]
⊢ x ^ p ^ (m + 1) ≡ y ^ p ^ (m + 1) [SMOD I ^ (m + 1 + 1)]

Tactic:
simp_rw [pow_succ _ m, pow_mul]
    exact ih.pow_add_one hpI m.succ_ne_zero

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝ : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem : P.root i + P.root m ∈ range ⇑P.root
hik_mem : P.root i + P.root k ∈ range ⇑P.root
hjk_mem : P.root (-k) + P.root j ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
h₁' : P.root (-k) - P.root i = P.root (-l)
h₂' : P.root (-k) + P.root j = P.root (-m)
h₃' : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
hki : P.pairingIn ℤ k i < 0
hik : chainBotCoeff i k = 0
hkj : P.pairingIn ℤ (-k) j < 0
hjk : chainBotCoeff j (-k) = 0
⊢ (chainBotCoeff i m + 1) * (chainBotCoeff j (-k) + 1) = (chainBotCoeff j (-l) + 1) * (chainBotCoeff i k + 1)

Tactic:
suffices P.chainBotCoeff i m = P.chainBotCoeff j (-l) by rw [hik, hjk, this]

Goal state after:
case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝ : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem : P.root i + P.root m ∈ range ⇑P.root
hik_mem : P.root i + P.root k ∈ range ⇑P.root
hjk_mem : P.root (-k) + P.root j ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
h₁' : P.root (-k) - P.root i = P.root (-l)
h₂' : P.root (-k) + P.root j = P.root (-m)
h₃' : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
hki : P.pairingIn ℤ k i < 0
hik : chainBotCoeff i k = 0
hkj : P.pairingIn ℤ (-k) j < 0
hjk : chainBotCoeff j (-k) = 0
⊢ chainBotCoeff i m = chainBotCoeff j (-l)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ x y : TensorAlgebra R M
i : ℕ
hx : x ∈ (ι R).range ^ i
hy : y ∈ (ι R).range ^ i
ihx : ((lift R) (GradedAlgebra.ι R M)) x = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x, hx⟩
ihy : ((lift R) (GradedAlgebra.ι R M)) y = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨y, hy⟩
⊢ ((lift R) (GradedAlgebra.ι R M)) (x + y) = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x + y, ⋯⟩

Tactic:
map_add,

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ x y : TensorAlgebra R M
i : ℕ
hx : x ∈ (ι R).range ^ i
hy : y ∈ (ι R).range ^ i
ihx : ((lift R) (GradedAlgebra.ι R M)) x = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x, hx⟩
ihy : ((lift R) (GradedAlgebra.ι R M)) y = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨y, hy⟩
⊢ ((lift R) (GradedAlgebra.ι R M)) x + ((lift R) (GradedAlgebra.ι R M)) y =
    (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x + y, ⋯⟩
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s ↦ s.1 + s.2

Tactic:
by
  rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩; dsimp at he ⊢
  classical
  obtain ⟨ha, rfl⟩ := add_singleton_eq_iff.1 he
  rw [add_assoc, mem_add] at ha
  obtain h | h := ha
  · refine ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, ?_⟩, ?_⟩
    · rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
    · rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
  · refine ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, ?_⟩, ?_⟩
    · rw [add_comm, singleton_add, cons_erase h]
    · rw [add_assoc, erase_add_right_pos _ h]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ ν : Measure ((i : ι) → α i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
⊢ μ univ = ν univ

Tactic:
rw [hμ.measure_univ_eq (∅ : Finset ι), hν.measure_univ_eq (∅ : Finset ι)]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders α
⊢ μ (cylinder I S) = ν (cylinder I S)

Tactic:
hμ.measure_cylinder _ hS,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders α
⊢ (P I) S = ν (cylinder I S)
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋃ i, ⋃ (_ : i ≤ n), s i ∈ C
⊢ (⋃ k, ⋃ (_ : k ≤ n), s k) ∪ s (n + 1) ∈ C

Tactic:
exact hC.union_mem hn (hs _)

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : accumulate s n ∈ C
⊢ accumulate s n ∪ s (n + 1) ∈ C

Tactic:
exact hC.union_mem hn (hs _)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X ↑i)
mS : MeasurableSet S
⊢ t.restrict ⁻¹' S ∈ {(Finset.Iic (t.sup id)).restrict ⁻¹' Finset.restrict₂ ⋯ ⁻¹' S}

Tactic:
rw [← preimage_comp, Finset.restrict₂_comp_restrict]

Goal state after:
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X ↑i)
mS : MeasurableSet S
⊢ t.restrict ⁻¹' S ∈ {t.restrict ⁻¹' S}
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c ≠ 0
x : V
a✝ : x ∈ ⊤
⊢ -g (e x) • (e v - v) = g (e x) • (v - e v)

Tactic:
rw [neg_smul, smul_sub, smul_sub, neg_sub]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
u v : α
h : u ≤ v
⊢ onIocAux f (Set.Ioc u v) = f v - f u

Tactic:
have h' : ∃ (p : α × α), p.1 ≤ p.2 ∧ Ioc u v = Ioc p.1 p.2 := ⟨(u, v), h, rfl⟩
  simp only [onIocAux, h', ↓reduceDIte]
  set u' := h'.choose.1
  set v' := h'.choose.2
  have hu'v' : u' ≤ v' ∧ Ioc u v = Ioc u' v' := h'.choose_spec
  rcases h.eq_or_lt with rfl | huv
  · grind [Set.Ioc_eq_empty_iff]
  rw [Ioc_eq_Ioc_iff (Or.inl huv)] at hu'v'
  grind

Goal state after:
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
⊢ interior {⊤} = {⊤}

Tactic:
interior_eq_iff_isOpen

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] {⊤}
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w → ∀ (i : Set α), MeasurableSet i → v i = w i

pp: case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → v i = w i) → v = w

Tactic:
· rintro rfl _ _
    rfl

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → v i = w i) → v = w
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ r • v x✝ = 0

Tactic:
v.not_measurable hi,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ r • 0 = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ v x✝ + w x✝ = 0

Tactic:
v.not_measurable hi,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ 0 + w x✝ = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ v x✝ - w x✝ = 0

Tactic:
v.not_measurable hi,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ 0 - w x✝ = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
⊢ μ i = ν i

Tactic:
have : μ.toSignedMeasure i = ν.toSignedMeasure i := by rw [h]

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : μ.toSignedMeasure i = ν.toSignedMeasure i
⊢ μ i = ν i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
⊢ v i ≤ w i

Tactic:
v.not_measurable hi,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
⊢ 0 ≤ w i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : AddLeftMono M
inst✝ : ContinuousAdd M
x✝² x✝¹ x✝ : VectorMeasure α M
h : x✝¹ ≤ x✝
i : Set α
hi : MeasurableSet i
⊢ x✝² i + x✝¹ i ≤ x✝² i + x✝ i

Tactic:
grw [h i hi]

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Subsingleton ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
i : ι
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδpos, hδ⟩ := (hf i).eLpNorm_indicator_le hp_one hp_top hε

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Subsingleton ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
i : ι
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
n : ℕ
hn : n ≥ N
⊢ eLpNorm (t.indicator (f n + -g)) p μ + eLpNorm (tᶜ.indicator (f n + -g)) p μ ≤ ε

Tactic:
Set.indicator_add' t,

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
n : ℕ
hn : n ≥ N
⊢ eLpNorm (t.indicator (f n) + t.indicator (-g)) p μ + eLpNorm (tᶜ.indicator (f n + -g)) p μ ≤ ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case a
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ s ≤[B] 0} ∧ s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ (fun x ↦ s ((⋃ i, B i) \ B n) + s (B n)) n ≤ s (B n)

pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ s ≤[B] 0} ∧ s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ MeasurableSet ((⋃ i, B i) \ B n)

Tactic:
· refine add_le_of_nonpos_left ?_
        have : s ≤[A] 0 :=
          restrict_le_restrict_iUnion _ _ hB₁ fun m =>
            let ⟨_, h⟩ := (hB m).1
            h
        refine
          nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ ?_ Set.sdiff_subset this)
        exact MeasurableSet.iUnion hB₁

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ s ≤[B] 0} ∧ s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ MeasurableSet ((⋃ i, B i) \ B n)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
⊢ μ.withDensityᵥ (s.rnDeriv μ) = s

Tactic:
ext1 i hi
    rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv_def, integral_sub,
      setIntegral_toReal_rnDeriv h.1 i, setIntegral_toReal_rnDeriv h.2 i]
    · conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition]
      rw [JordanDecomposition.toSignedMeasure, _root_.sub_apply,
        toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
        measureReal_def]
    all_goals
      refine Integrable.integrableOn ?_
      refine ⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩
      · apply Measurable.aestronglyMeasurable (by fun_prop)
      · exact (lintegral_rnDeriv_lt_top _ _).ne

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ s (i ∆ j) = 0 ∧ s (iᶜ ∆ jᶜ) = 0

Tactic:
by
  rw [restrict_le_restrict_iff s 0, restrict_le_restrict_iff 0 s] at hi' hj'
  constructor
  · rw [Set.symmDiff_def, Set.sdiff_eq_compl_inter, Set.sdiff_eq_compl_inter, of_union,
      le_antisymm (hi'.2 (hi.compl.inter hj) Set.inter_subset_left)
        (hj'.1 (hi.compl.inter hj) Set.inter_subset_right),
      le_antisymm (hj'.2 (hj.compl.inter hi) Set.inter_subset_left)
        (hi'.1 (hj.compl.inter hi) Set.inter_subset_right), zero_apply, zero_apply, zero_add]
    · exact
        Set.disjoint_of_subset_left Set.inter_subset_left
          (Set.disjoint_of_subset_right Set.inter_subset_right
            (disjoint_comm.1 (IsCompl.disjoint isCompl_compl)))
    · exact hj.compl.inter hi
    · exact hi.compl.inter hj
  · rw [Set.symmDiff_def, Set.sdiff_eq_compl_inter, Set.sdiff_eq_compl_inter, compl_compl,
      compl_compl, of_union,
      le_antisymm (hi'.2 (hj.inter hi.compl) Set.inter_subset_right)
        (hj'.1 (hj.inter hi.compl) Set.inter_subset_left),
      le_antisymm (hj'.2 (hi.inter hj.compl) Set.inter_subset_right)
        (hi'.1 (hi.inter hj.compl) Set.inter_subset_left), zero_apply, zero_apply, zero_add]
    · exact
        Set.disjoint_of_subset_left Set.inter_subset_left
          (Set.disjoint_of_subset_right Set.inter_subset_right
            (IsCompl.disjoint isCompl_compl))
    · exact hj.inter hi.compl
    · exact hi.inter hj.compl
  all_goals measurability

Goal state after: