mathlib-initiative/mathlib-tactics huggingface dataset:
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
hSB : B.IsSymm
y z : M
⊢ (B x) x * (B y) z - 2 * (B x) y * (B x) z - (2 * (B x) z * (B y) x - 2 * (B x) z * (coroot B hx) y * (B x) x) =
    (B x) x * (B y) z

Tactic:
rw [sub_eq_iff_eq_add, ← hSB.eq x y, RingHom.id_apply, mul_assoc _ _ (B x x), mul_comm _ (B x x),
    apply_self_mul_coroot_apply]

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
hSB : B.IsSymm
y z : M
⊢ (B x) x * (B y) z - 2 * (B x) y * (B x) z = (B x) x * (B y) z + (2 * (B x) z * (B x) y - 2 * (B x) z * (2 * (B x) y))
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
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x : ↑{x | B.IsReflective x}
⊢ LeftInverse (fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩) fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩

Tactic:
intro y

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
⊢ (fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩) ((fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩) y) = y
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
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x : ↑{x | B.IsReflective x}
⊢ RightInverse (fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩) fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩

Tactic:
intro y

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
⊢ (fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩) ((fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩) y) = y
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]

Goal state after:
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) ^ p ≡ (y ^ p ^ m) ^ p [SMOD I ^ (m + 1 + 1)]
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M)) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
a : SymmetricAlgebra R M
⊢ motive a

Tactic:
rcases algHom_surjective _ _ a with ⟨a, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M)) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
a : TensorAlgebra R M
⊢ motive ((algHom R M) a)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basis

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Free R M
κ : Type uM
b : Basis κ R M
⊢ Cardinal.lift.{uR, uM} #(List κ) = Cardinal.lift.{uR, uM} (sum fun n ↦ Module.rank R M ^ n)

Tactic:
mk_list_eq_sum_pow,

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Free R M
κ : Type uM
b : Basis κ R M
⊢ Cardinal.lift.{uR, uM} (sum fun n ↦ #κ ^ n) = Cardinal.lift.{uR, uM} (sum fun n ↦ Module.rank R M ^ n)
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: case inr
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄, i ≠ j → i < j → (Coprime on coprimes a) i j
ltij : j ≤ i
⊢ (Coprime on coprimes a) i j

pp: m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
⊢ (Coprime on coprimes a) i j

Tactic:
· exact (this a hij.symm (lt_of_le_of_ne ltij hij.symm)).symm

Goal state after:
m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
⊢ (Coprime on coprimes a) i j
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
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
u : V
hu : u ∉ (↑e).fixedSubmodule
⊢ ∃ f v, (↑e).fixedSubmodule ≤ ker f ∧ f v = 1

Tactic:
obtain ⟨f, hfu, hf⟩ := Submodule.exists_dual_map_eq_bot_of_notMem hu inferInstance

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
u : V
hu : u ∉ (↑e).fixedSubmodule
f : Dual K V
hfu : f u ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
⊢ ∃ f v, (↑e).fixedSubmodule ≤ ker f ∧ f v = 1
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case refine_1
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hv' : v - e v ∈ (↑e).fixedSubmodule
t : V ≃ₗ[K] V := auxTransvection ⋯
ht : t = auxTransvection ⋯
⊢ t⁻¹ ∈ transvections K V

Tactic:
inv_mem_transvections_iff,

Goal state after:
case refine_1
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hv' : v - e v ∈ (↑e).fixedSubmodule
t : V ≃ₗ[K] V := auxTransvection ⋯
ht : t = auxTransvection ⋯
⊢ t ∈ transvections K V
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : ↑I ⊆ C
hI : (↑I).PairwiseDisjoint id
hst : s \ t = ⋃₀ ↑I
⊢ I.sup id = s \ t

pp: case refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : ↑I ⊆ C
hI : (↑I).PairwiseDisjoint id
hst : s \ t = ⋃₀ ↑I
⊢ ↑(Finpartition.ofErase I ⋯ ?refine_1).parts ⊆ C

Tactic:
· rw [sup_id_eq_sSup, sSup_eq_sUnion, hst]

Goal state after:
case refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : ↑I ⊆ C
hI : (↑I).PairwiseDisjoint id
hst : s \ t = ⋃₀ ↑I
⊢ ↑(Finpartition.ofErase I ⋯ ⋯).parts ⊆ C
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert.inr
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid s).parts → Finpartition t
hQ : ∀ (t : Set α) (a : t ∈ (P.avoid s).parts), ↑(Q t a).parts ⊆ C
⊢ s ∈ C ∧ ∀ i ∈ ↑(P.avoid s).parts.attach, ↑(Q ↑i ⋯).parts ⊆ C

Tactic:
Subtype.forall

Goal state after:
case insert.inr
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid s).parts → Finpartition t
hQ : ∀ (t : Set α) (a : t ∈ (P.avoid s).parts), ↑(Q t a).parts ⊆ C
⊢ s ∈ C ∧ ∀ (a : Set α) (b : a ∈ (P.avoid s).parts), ⟨a, b⟩ ∈ ↑(P.avoid s).parts.attach → ↑(Q ↑⟨a, b⟩ ⋯).parts ⊆ C
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}
s : Set α
x✝ : ∃ x ∈ 𝒜, xᶜ = s
x : Set α
x_mem : x ∈ 𝒜
hx : xᶜ = s
⊢ sᶜ ∈ 𝒜

Tactic:
by simp [← hx, x_mem]

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

Goal state before:
pp: case refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ↑{s} ⊆ C

Tactic:
singleton_subset_set_iff

Goal state after:
case refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ s ∈ C
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case inr
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
⊢ False

Tactic:
· -- When `c ≠ 0`, we contradict `hne_top`
    refine hne_top.ne ?_
    rw [eq_top_iff]
    intro x _
    have h1 : g (e x) • (v - e v) ∈ K ∙ (e v - v) :=
      mem_span_singleton.mpr ⟨-g (e x), by rw [neg_smul, smul_sub, smul_sub, neg_sub]⟩
    have hle : e.fixedSubmodule ⊔ K ∙ v ≤ e.fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v :=
      sup_le_sup_right le_sup_left _
    have h2 : c • x ∈ e.fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v := by
      rw [show c • x = g (e x) • (v - e v) - (g (e x) • (v - e v) - c • x) by abel]
      exact Submodule.sub_mem _ (mem_sup_left (mem_sup_right h1)) (hle (key x))
    simpa [smul_smul, inv_mul_cancel₀ hc0] using Submodule.smul_mem _ c⁻¹ h2

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
x✝ : ℕ
⊢ Function.extend e (fun i ↦ v (f i)) 0 x✝ = v (Function.extend e f (fun x ↦ ∅) x✝)

pp: case e'_6
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ⋃ i, f i = ⋃ i, Function.extend e f (fun x ↦ ∅) i

pp: case convert_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ∀ (i : ℕ), MeasurableSet (Function.extend e f (fun x ↦ ∅) i)

pp: case convert_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Pairwise (Disjoint on Function.extend e f fun x ↦ ∅)

Tactic:
· simp only [Pi.zero_def, Function.apply_extend v, Function.comp_def, empty]

Goal state after:
case e'_6
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ⋃ i, f i = ⋃ i, Function.extend e f (fun x ↦ ∅) i

case convert_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ∀ (i : ℕ), MeasurableSet (Function.extend e f (fun x ↦ ∅) i)

case convert_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Pairwise (Disjoint on Function.extend e f fun x ↦ ∅)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ (μ + ν) i = (μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) i

Tactic:
add_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ μ i + ν i = (μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
v : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ v.ennrealToMeasure s = v s

Tactic:
by
  rw [ennrealToMeasure, ofMeasurable_apply _ hs]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.restrictNonposSeq i 0 ⊆ i

Tactic:
rw [restrictNonposSeq]; exact someExistsOneDivLT_subset'

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ s.restrictNonposSeq i (n✝ + 1) ⊆ i

Tactic:
rw [restrictNonposSeq]; exact someExistsOneDivLT_subset'

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ (v.restrict i) j = v (j ∩ i)

Tactic:
rw [restrict, dif_pos hi]
  exact if_pos hj

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid M
inst✝¹ : T2Space M
inst✝ : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
A : Set α
hA : MeasurableSet A
⊢ Disjoint (A ∩ i) (A ∩ iᶜ)

Tactic:
exact disjoint_compl_right.inter_right' A |>.inter_left' A

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ -j.negPart.real A ≤ 0 A

Tactic:
neg_le,

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ -0 A ≤ j.negPart.real A
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : s ≤[u] 0
hw₁ : s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ s v = 0

Tactic:
rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu
  have := subset_positive_null_set hu hv hw hsu
  simp only [neg_apply, neg_eq_zero] at this
  exact this hw₁ hw₂ hwt

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ (↑(bdd n) + 1)⁻¹
⊢ Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop

Tactic:
exact Summable.tendsto_atTop_of_pos h₃' fun n => Nat.cast_add_one_pos (bdd n)

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : n ≤ ↑i
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
· rw [(_ : f i = g ⟨i.val, hi⟩)]
      · exact hδ₁ _ s hs (le_trans hμs <| ENNReal.ofReal_le_ofReal <| min_le_left _ _)
      · simp [g]

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : n ≤ ↑i
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i + s.toJordanDecomposition.negPart i = 0
⊢ s i = 0

Tactic:
add_eq_zero

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
⊢ s i = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mp.left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S + s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.posPart S = 0

Tactic:
add_eq_zero

Goal state after:
case mp.left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.posPart S = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S + s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.negPart S = 0

Tactic:
add_eq_zero

Goal state after:
case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.negPart S = 0