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

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : (e i).col (Sum.inr j) = u i
⊢ (e i ^ 2 * e i) *ᵥ Pi.single (Sum.inr j) 1 = 0

Tactic:
← Matrix.mulVec_mulVec

Goal state after:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : (e i).col (Sum.inr j) = u i
⊢ e i ^ 2 *ᵥ e i *ᵥ Pi.single (Sum.inr j) 1 = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : ¬j = -↑i
k : ι
x : ℕ
hk₁ : P.root j + (chainTopCoeff (↑i) j + 1) • P.root ↑i ∈ range ⇑P.root
⊢ ↑i ≠ j

Tactic:
rintro rfl

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
k : ι
x : ℕ
hij : ¬↑i = -↑i
hk₁ : P.root ↑i + (chainTopCoeff ↑i ↑i + 1) • P.root ↑i ∈ range ⇑P.root
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : 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
hki : P.pairingIn ℤ k i = 0
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
⊢ n ≠ k

Tactic:
rintro rfl

Goal state after:
ι : 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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
h₁ : P.root n + P.root i = P.root l
h₂ : P.root n - P.root j = P.root m
hki : P.pairingIn ℤ n i = 0
hjk_mem : P.root j + P.root (-n) ∈ range ⇑P.root
hn : P.root n = P.root n + P.root i - P.root j
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
k ij : ι
hij : ij ∈ {long P, short P}
hk : P.root k ∉ allRoots P
⊢ P.IsOrthogonal k ij

Tactic:
have aux := isOrthogonal_short_and_long P hk

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
k ij : ι
hij : ij ∈ {long P, short P}
hk : P.root k ∉ allRoots P
aux : P.IsOrthogonal k (short P) ∧ P.IsOrthogonal k (long P)
⊢ P.IsOrthogonal k ij
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case neg
ι : 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 : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∉ range ⇑P.root
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0

Tactic:
have aux₃ : ∀ x ∈ Finset.univ,
          ¬ (P.root x = P.root i + P.root l ∧ P.root k = P.root x - P.root j) := by
        rintro x - ⟨hx, hx'⟩; exact h₅ ⟨k, by rw [hx', hx]; abel⟩
      have aux₄ : ∀ x ∈ Finset.univ,
          ¬ (P.root x = P.root l - P.root j ∧ P.root k = P.root i + P.root x) := by
        rintro x - ⟨hx, hx'⟩; exact h₅ ⟨k, by rw [hx', hx]; abel⟩
      simp [Finset.sum_ite_of_false aux₃, Finset.sum_ite_of_false aux₄]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (DirectSum.coeAlgHom fun x ↦ (ι R).range ^ x).comp ((lift R) (GradedAlgebra.ι R M)) = AlgHom.id R (TensorAlgebra R M)

Tactic:
ext m

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (((DirectSum.coeAlgHom fun x ↦ (ι R).range ^ x).comp ((lift R) (GradedAlgebra.ι R M))).toLinearMap ∘ₗ ι R) m =
    ((AlgHom.id R (TensorAlgebra R M)).toLinearMap ∘ₗ ι R) m
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (squareCylinders fun i ↦ {s | MeasurableSet s}) = MeasurableSpace.pi

Tactic:
by
  apply le_antisymm
  · rw [MeasurableSpace.generateFrom_le_iff]
    rintro S ⟨s, t, h, rfl⟩
    simp only [mem_univ_pi, mem_ofPred_eq] at h
    exact MeasurableSet.pi (Finset.countable_toSet _) (fun i _ ↦ h i)
  · refine iSup_le fun i ↦ ?_
    refine (comap_eval_le_generateFrom_squareCylinders_singleton α i).trans ?_
    refine MeasurableSpace.generateFrom_mono ?_
    rw [← Finset.coe_singleton, squareCylinders_eq_iUnion_image]
    exact subset_iUnion
      (fun (s : Finset ι) ↦
        (fun t : ∀ i, Set (α i) ↦ (s : Set ι).pi t) '' univ.pi (fun i ↦ Set.ofPred MeasurableSet))
      ({i} : Finset ι)

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u' ≤ u
u'' v'' : α
h'' : u'' ≤ v''
heq : Set.Ioc (max u v') v = Set.Ioc u'' v''
⊢ ↑{Set.Ioc u'' v''} ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} ∧
    (↑{Set.Ioc u'' v''}).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ ↑{Set.Ioc u'' v''}

Tactic:
grind [coe_singleton, pairwiseDisjoint_singleton]

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v ≤ v'
u'' v'' : α
h'' : u'' ≤ v''
heq : Set.Ioc u (min u' v) = Set.Ioc u'' v''
⊢ ↑{Set.Ioc u'' v''} ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} ∧
    (↑{Set.Ioc u'' v''}).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ ↑{Set.Ioc u'' v''}

Tactic:
grind [coe_singleton, pairwiseDisjoint_singleton]

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
⊢ ∃ I, ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} ∧ (↑I).PairwiseDisjoint id ∧ Set.Ioc u u' ∪ Set.Ioc v' v = ⋃₀ ↑I

Tactic:
refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
⊢ (↑{Set.Ioc u u', Set.Ioc v' v}).PairwiseDisjoint id
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    (fun ω ↦ (B (s.indicator (Function.const Ω c) ω)) (f ω)) = s.indicator fun ω ↦ (B c) (f ω)
g₁ g₂ : SimpleFunc Ω F
x✝ : Disjoint (Function.support ⇑g₁) (Function.support ⇑g₂)
h_eq₁ : μ[fun ω ↦ (B (g₁ ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (g₁ ω)) (μ[g | m] ω)
h_eq₂ : μ[fun ω ↦ (B (g₂ ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (g₂ ω)) (μ[g | m] ω)
h_add : ⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
⊢ μ[fun ω ↦ (B (g₁ ω + g₂ ω)) (g ω) | m] =ᵐ[μ] μ[fun ω ↦ (B (g₁ ω)) (g ω) | m] + μ[fun ω ↦ (B (g₂ ω)) (g ω) | m]

Tactic:
B.map_add

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    (fun ω ↦ (B (s.indicator (Function.const Ω c) ω)) (f ω)) = s.indicator fun ω ↦ (B c) (f ω)
g₁ g₂ : SimpleFunc Ω F
x✝ : Disjoint (Function.support ⇑g₁) (Function.support ⇑g₂)
h_eq₁ : μ[fun ω ↦ (B (g₁ ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (g₁ ω)) (μ[g | m] ω)
h_eq₂ : μ[fun ω ↦ (B (g₂ ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (g₂ ω)) (μ[g | m] ω)
h_add : ⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
⊢ μ[fun ω ↦ (B (g₁ ω) + B (g₂ ω)) (g ω) | m] =ᵐ[μ] μ[fun ω ↦ (B (g₁ ω)) (g ω) | m] + μ[fun ω ↦ (B (g₂ ω)) (g ω) | m]
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
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
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
g : Dual K V
hg0 : g ≠ 0
hg2 : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v ≤ ker g
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
he' : ∀ (a : K), ∃ x, (auxTransvection hf * e).fixedReduce x ≠ a • x
⊢ finrank K (V ⧸ (↑(auxTransvection hf * e)).fixedSubmodule) = n + 1

Tactic:
by rw [auxTransvection_mul_fixed hfv, hrank]

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
⊢ (v.map id) i = v i

Tactic:
rw [map_apply v measurable_id hi, Set.preimage_id]

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
⊢ (v.restrict i) A + (v.restrict iᶜ) A = v A

Tactic:
restrict_apply _ hi hA,

Goal state after:
α : 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
⊢ v (A ∩ i) + (v.restrict iᶜ) A = v A
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → 0 j ≤ s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → 0 j ≤ s j
hs : s (u ∆ v) = 0
a : 0 (u \ v) ≤ s (u \ v)
b : 0 (v \ u) ≤ s (v \ u)
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0

Tactic:
rw [Set.symmDiff_def,
      of_union (v := s) (Set.disjoint_of_subset_left sdiff_subset disjoint_sdiff_self_right)
        (hu.diff hv) (hv.diff hu)] at hs

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → 0 j ≤ s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → 0 j ≤ s j
hs : s (u \ v) + s (v \ u) = 0
a : 0 (u \ v) ≤ s (u \ v)
b : 0 (v \ u) ≤ s (v \ u)
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → v s = 0
s : Set α
hmeas : MeasurableSet s
hs : μ s = 0
⊢ μ.ennrealToMeasure s = 0

Tactic:
rw [← hs, ennrealToMeasure_apply hmeas]

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ MeasurableSet (i ∩ Sᶜ)

Tactic:
exact hi.inter hS₁.compl

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
⊢ s.totalVariation ≪ μ.ennrealToMeasure

Tactic:
refine Measure.AbsolutelyContinuous.mk fun S hS₁ hS₂ => ?_

Goal state after:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
⊢ s.totalVariation S = 0
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 ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : 0 E < s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / s E + 1) 1 ≤ ↑(bdd a)
⊢ 1 / s E < ↑(bdd k)

Tactic:
linarith only [le_of_max_le_left (hk k le_rfl)]

Goal state after:
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

pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure
⊢ μ.toENNRealVectorMeasure.ennrealToMeasure = μ

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:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure
⊢ μ.toENNRealVectorMeasure.ennrealToMeasure = μ
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ Continuous[instTopologicalSpace, _] fun μ ↦ μ.mass

Tactic:
simp_rw [← testAgainstNN_one]

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ Continuous[instTopologicalSpace, _] fun μ ↦ μ.testAgainstNN 1
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN
f : Ω →ᵇ ℝ≥0
key : μ.toWeakDualBCNN f = ν.toWeakDualBCNN f
⊢ ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ ≠ ∞

pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN
f : Ω →ᵇ ℝ≥0
key : μ.toWeakDualBCNN f = ν.toWeakDualBCNN f
⊢ ∫⁻ (ω : Ω), ↑(f ω) ∂↑ν ≠ ∞

Tactic:
· exact (lintegral_lt_top_of_nnreal μ f).ne

Goal state after:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN
f : Ω →ᵇ ℝ≥0
key : μ.toWeakDualBCNN f = ν.toWeakDualBCNN f
⊢ ∫⁻ (ω : Ω), ↑(f ω) ∂↑ν ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: case inl
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst✝² : TopologicalSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed[inst✝²] s) MeasurableSet
ε : ENNReal
hε : 0 < ε
r : ENNReal := μ univ
hεr : ε < r
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
| inl hεr =>

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

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst✝²] F
hne : L.NeBot
ε : ℝ≥0
⊢ 0 < ε → ↑μ F < ∞ → limsup (fun i ↦ ↑(μs i) F) L ≤ ↑μ F + ↑ε

Tactic:
ε_pos

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst✝²] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
⊢ ↑μ F < ∞ → limsup (fun i ↦ ↑(μs i) F) L ≤ ↑μ F + ↑ε
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_2.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
this : ∀ (i : ℕ), s.indicator ((↑n)⁻¹ • f i) = (↑n)⁻¹ • s.indicator (f i)
hn : n ≠ 0
⊢ ‖(↑n)⁻¹‖ₑ * ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
enorm_inv (by positivity),

Goal state after:
case refine_2.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
this : ∀ (i : ℕ), s.indicator ((↑n)⁻¹ • f i) = (↑n)⁻¹ • s.indicator (f i)
hn : n ≠ 0
⊢ ‖↑n‖ₑ⁻¹ * ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε