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

Goal state before:
pp: case h
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
χ : ↥H → K
hχ : χ ≠ 0
hχ' : genWeightSpace (↥U) χ ≠ ⊥
this : ∀ {w : ↥b.support ⊕ ι → K}, w ≠ 0 → w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ → ∃ i t, t • w = v b i
w : ↥U
hw₀ : w ≠ 0
hw : U.incl w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
i : ι
t : K
hi : t • ↑w = v b i
⊢ v b i ∈ genWeightSpace (↥b.support ⊕ ι → K) χ ⊓ U

Tactic:
← hi,

Goal state after:
case h
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
χ : ↥H → K
hχ : χ ≠ 0
hχ' : genWeightSpace (↥U) χ ≠ ⊥
this : ∀ {w : ↥b.support ⊕ ι → K}, w ≠ 0 → w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ → ∃ i t, t • w = v b i
w : ↥U
hw₀ : w ≠ 0
hw : U.incl w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
i : ι
t : K
hi : t • ↑w = v b i
⊢ t • ↑w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ ⊓ U
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: case refine_1
ι : 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
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k 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
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
⊢ 0 < -P.pairingIn ℤ i j

Tactic:
neg_pos,

Goal state after:
case refine_1
ι : 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
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k 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
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
⊢ P.pairingIn ℤ i j < 0
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 y : ↑{x | B.IsReflective x}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : 2 * (B ↑x) ↑y = (B ↑x) ↑x * 2
h2y : (B ↑y) ↑y * 2 = 2 * (B ↑y) ↑x
⊢ 2 * (B ↑x) ↑y = 2 * (B ↑y) ↑y

Tactic:
← hSB.eq,

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}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : 2 * (B ↑x) ↑y = (B ↑x) ↑x * 2
h2y : (B ↑y) ↑y * 2 = 2 * (B ↑y) ↑x
⊢ 2 * (RingHom.id R) ((B ↑y) ↑x) = 2 * (B ↑y) ↑y
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Submodule.map (mk R ι M) ⊤ = ⊤

Tactic:
Submodule.map_top,

Goal state after:
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (mk R ι M).range = ⊤
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 f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
⊢ finrank K ↥(↑(f * e)).fixedSubmodule ≤ 1 + finrank K ↥(↑e).fixedSubmodule

Tactic:
by
  conv_rhs => rw [show e = f⁻¹ * (f * e) by simp]
  rw [← inv_mem_dilatransvections_iff] at hf
  exact le_one_add_finrank_fixedSubmodule_dilatransvection_mul (f * e) f⁻¹ hf

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case hf
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 : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ map f (↑e).fixedSubmodule = ⊥

Tactic:
rw [eq_bot_iff]
    rw [gc_map_comap, Submodule.comap_bot]
    exact le_trans le_sup_left hf

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

Goal state before:
pp: case refine_2
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
⊢ eval i ⁻¹' (fun j ↦ if hji : j = i then ⋯.mpr t else univ) i = S

Tactic:
· #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was: `grind` -/
    simp [h]

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (insert t ↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id

Tactic:
have h := hC.pairwiseDisjoint_disjointOfDiff hs ht
  refine PairwiseDisjoint.insert_of_notMem h (hC.notMem_disjointOfDiff hs ht) fun u hu ↦ ?_
  simp_rw [id]
  refine Disjoint.mono_right ?_ (hC.disjoint_sUnion_disjointOfDiff hs ht)
  exact subset_sUnion_of_mem hu

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
⊢ s = cylinder (I ∪ J) S'

Tactic:
hs_eq

Goal state after:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
⊢ cylinder I S = cylinder (I ∪ J) S'
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : ↑I ⊆ _root_.supClosure C
h'I : (↑I).PairwiseDisjoint id
hh'I : ⋃₀ ↑I ∈ _root_.supClosure C
⊢ m.supClosureFun (⋃₀ ↑I) = ∑ u ∈ I, m.supClosureFun u

Tactic:
choose! J hJC using fun s (hs : s ∈ I) => hC.mem_supClosure_iff.mp (hI hs)
    let K : Finpartition (I.sup id) := Finpartition.combine J h'I.supIndep
    rw [← sSup_eq_sUnion, ← sup_id_eq_sSup, ← K.sup_parts, sup_id_eq_sSup, sSup_eq_sUnion,
      m.supClosureFun_apply hC (by simpa [K] using hJC) K.supIndep.pairwiseDisjoint rfl,
      Finpartition.sum_combine]
    refine Finset.sum_congr rfl fun i hi ↦ Eq.symm <|
      m.supClosureFun_apply hC (hJC i hi) (J i).supIndep.pairwiseDisjoint ?_
    rw [← sSup_eq_sUnion, ← sup_id_eq_sSup, (J i).sup_parts]

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

Goal state before:
pp: case refine_2
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ (↑(Finset.image f I)).PairwiseDisjoint id

Tactic:
simp only [coe_image]
    intro s hs t ht hst
    rw [Set.mem_image] at hs ht
    obtain ⟨i, _, rfl⟩ := hs
    obtain ⟨j, _, rfl⟩ := ht
    have hij : i ≠ j := by intro h_eq; rw [h_eq] at hst; exact hst rfl
    exact hf_disj hij

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∈ C
⊢ (AddContent.extend hC m) s = m s

Tactic:
rwa [m.extend_eq_extend, extend_eq]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
⊢ Tendsto (fun i ↦ M * r i) atTop (𝓝[>] 0)

Tactic:
convert! TendstoNhdsWithinIoi.const_mul hM hr

Goal state after:
case e'_3
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
⊢ 0 = M * 0

case e'_4
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
⊢ 0 = M * 0
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := fun i ↦ if 0 < r i then r i else 1 / (↑i + 1)
i : ℕ
hi : 0 < r i
⊢ r' i ∈ Ioi 0

Tactic:
simp [r', hi]

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

Goal state before:
pp: case iUnion
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
X : Type u_5
mX : MeasurableSpace X
μ ν : VectorMeasure X M
C : Set (Set X)
hμν : ∀ s ∈ C, μ s = ν s
hA : mX = MeasurableSpace.generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set X
f : ℕ → Set X
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), μ (f i) = ν (f i)
⊢ μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
simp [of_disjoint_iUnion, hfm, hfd, ihf]

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 : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
n✝ : ℕ
h : n < n✝ + 1
hx₂ : x ∈ s.restrictNonposSeq i (n✝ + 1)
⊢ False

Tactic:
rw [restrictNonposSeq] at hx₂
    exact
      (someExistsOneDivLT_subset hx₂).2
        (Set.mem_iUnion.2 ⟨n, Set.mem_iUnion.2 ⟨Nat.lt_succ_iff.mp h, hx₁⟩⟩)

Goal state after:
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 : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : s (u ∆ v) = 0
this : (-s) (u ∆ v) = 0 → (-s) (w ∩ u) = (-s) (w ∩ v)
⊢ s (w ∩ u) = s (w ∩ v)

Tactic:
simp only [neg_apply, neg_inj, neg_eq_zero] at this

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : s (u ∆ v) = 0
this : s (u ∆ v) = 0 → s (w ∩ u) = s (w ∩ v)
⊢ s (w ∩ u) = s (w ∩ v)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
⊢ toJordanDecomposition 0 = 0

Tactic:
apply toSignedMeasure_injective

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
⊢ (toJordanDecomposition 0).toSignedMeasure = toSignedMeasure 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ (-s).toJordanDecomposition = -s.toJordanDecomposition

Tactic:
apply toSignedMeasure_injective

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ (-s).toJordanDecomposition.toSignedMeasure = (-s.toJordanDecomposition).toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
apply toSignedMeasure_injective

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (r • s).toJordanDecomposition.toSignedMeasure = (r • s.toJordanDecomposition).toSignedMeasure
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 = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.posPart S = 0

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 = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.negPart S = 0

Tactic:
exacts [this.1, this.2]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : ¬Integrable f μ
⊢ μ.withDensityᵥ (-f) = -μ.withDensityᵥ f

Tactic:
· rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, neg_zero]
    rwa [integrable_neg_iff]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
⊢ μ.withDensityᵥ (f + g) = μ.withDensityᵥ f + μ.withDensityᵥ g

Tactic:
by
  ext1 i hi
  rw [withDensityᵥ_apply (hf.add hg) hi, _root_.add_apply, withDensityᵥ_apply hf hi,
    withDensityᵥ_apply hg hi]
  simp_rw [Pi.add_apply]
  rw [integral_add]
  · exact hf.integrableOn
  · exact hg.integrableOn

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ = μ

Tactic:
by
  refine Measure.ext fun i hi => ?_
  lift μ i to ℝ≥0 using (measure_lt_top _ _).ne with m hm
  rw [SignedMeasure.toMeasureOfZeroLE_apply _ _ _ hi, ENNReal.coe_inj]
  congr
  simp [hi, ← hm, measureReal_def]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • s).toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

Tactic:
rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart]
    infer_instance

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).toJordanDecomposition.toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure

Tactic:
rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

Tactic:
by
        use ⟨t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)⟩
        refine ⟨hf.ennreal_ofReal, htμ.1, ?_⟩
        rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ singularPart 0 μ = 0

Tactic:
by
  refine (eq_singularPart 0 0 VectorMeasure.MutuallySingular.zero_left ?_).symm
  rw [zero_add, withDensityᵥ_zero]

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ ↑(ν s) = ↑ν s

Tactic:
by
  rw [← coeFn_comp_toFiniteMeasure_eq_coeFn, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure,
    toMeasure_comp_toFiniteMeasure_eq_toMeasure]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Tactic:
refine ⟨((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1).toNNReal, fun i => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ eLpNorm (f i) p μ ≤ ↑(↑C * μ univ ^ p.toReal⁻¹ + 1).toNNReal
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
⊢ Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize)

Tactic:
by
  rw [ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds,
    tendsto_iff_forall_testAgainstNN_tendsto]
  exact fun f ↦ tendsto_normalize_testAgainstNN_of_tendsto μs_lim nonzero f

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_1
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk X mX ∘ Prod.fst =ᵐ[μ.prod ν] X ∘ Prod.fst

Tactic:
apply ae_eq_comp

Goal state after:
case refine_1.hf
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable Prod.fst (μ.prod ν)

case refine_1.h
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk X mX =ᵐ[Measure.map Prod.fst (μ.prod ν)] X