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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k : ι
hk : k ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
this : ⁅e ⟨k, hk⟩, u ⟨k, hk⟩⁆ = 2 • v b k
e' : ↥(lieAlgebra b) := ⟨e ⟨k, hk⟩, ⋯⟩
⊢ v b k ∈ U

Tactic:
change ⁅e', u ⟨k, hk⟩⁆ = _ at this

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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k : ι
hk : k ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
e' : ↥(lieAlgebra b) := ⟨e ⟨k, hk⟩, ⋯⟩
this : ⁅e', u ⟨k, hk⟩⁆ = 2 • v b k
⊢ v b k ∈ U
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}
z : M
⊢ 2 * (B ↑x) ↑y * (2 * (B ↑x) z) = 2 * (2 * (B ↑x) ↑y) * (RingHom.id R) ((B ↑x) z)

Tactic:
RingHom.id_apply

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}
z : M
⊢ 2 * (B ↑x) ↑y * (2 * (B ↑x) z) = 2 * (2 * (B ↑x) ↑y) * (B ↑x) z
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : 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
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) := { toSubmodule := ↑U, lie_mem := ⋯ }
hU : ↑U ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬∑ k, c k * ↑|b.cartanMatrix j k| = 0
this : ⁅e j, x⁆ ∈ U
aux : ∀ (k : ↥b.support), ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b ↑j
⊢ v b ↑j ∈ U

Tactic:
← hc,

Goal state after:
ι : 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
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) := { toSubmodule := ↑U, lie_mem := ⋯ }
hU : ↑U ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬∑ k, c k * ↑|b.cartanMatrix j k| = 0
aux : ∀ (k : ↥b.support), ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b ↑j
this : ⁅e j, ∑ i, c i • u i⁆ ∈ U
⊢ v b ↑j ∈ U
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case of.perm.right
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ (addConGen (Rel R ι M)) (r • (PiTensorProduct.tprod R) fun i ↦ f i) (r • (PiTensorProduct.tprod R) fun i ↦ f (e i))

Tactic:
convert!
          AddConGen.Rel.of _ _ <|
            SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)
        · rw [MultilinearMap.map_update_smul, Function.update_eq_self]
        · simp_rw [Function.update_apply_equiv_apply, MultilinearMap.map_update_smul,
              ← Function.update_comp_equiv, Function.update_eq_self]; rfl

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
a✝ : t ∉ T
ih : ∀ ⦃s : Set α⦄, s ∈ supClosure C → ↑T ⊆ C → s \ T.sup id ∈ supClosure C
s : Set α
hs : s ∈ supClosure C
hTC : ↑(insert t T) ⊆ C
⊢ s \ (t ∪ T.sup id) ∈ supClosure C

Tactic:
← sdiff_sdiff

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
a✝ : t ∉ T
ih : ∀ ⦃s : Set α⦄, s ∈ supClosure C → ↑T ⊆ C → s \ T.sup id ∈ supClosure C
s : Set α
hs : s ∈ supClosure C
hTC : ↑(insert t T) ⊆ C
⊢ (s \ t) \ T.sup id ∈ supClosure C
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
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
f : Dual K V
hf : map f ((↑e).fixedSubmodule ⊔ K ∙ (e u - u)) = ⊥
hfu : f u ≠ 0
v : V := (f u)⁻¹ • u
v_def : v = (f u)⁻¹ • u
hspan : K ∙ (e v - v) = K ∙ (e u - u)
⊢ ∃ f v,
    LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] ∧
      (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f ∧ f v = 1

Tactic:
rw [← hspan, ← le_ker_iff_map] at hf

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
f : Dual K V
hfu : f u ≠ 0
v : V := (f u)⁻¹ • u
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
v_def : v = (f u)⁻¹ • u
hspan : K ∙ (e v - v) = K ∙ (e u - u)
⊢ ∃ f v,
    LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] ∧
      (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f ∧ f v = 1
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
⊢ s ∈ ℬ

Tactic:
induction hs with
  | base t t_mem => exact h t_mem
  | empty => exact hℬ.empty_mem
  | compl t _ t_mem => exact hℬ.compl_mem t_mem
  | union t u _ _ t_mem u_mem => exact hℬ.union_mem t_mem u_mem

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

Goal state before:
pp: case inl
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 : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ v + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = 0 → s = 0 ∧ t = 0
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
hmem : v - e v ∈ (↑e).fixedSubmodule ⊔ K ∙ v
⊢ 1 = 0

Tactic:
simp only [mem_sup, mem_span_singleton, exists_exists_eq_and] at hmem

Goal state after:
case inl
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 : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ v + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = 0 → s = 0 ∧ t = 0
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
hmem : ∃ y ∈ (↑e).fixedSubmodule, ∃ a, y + a • v = v - e v
⊢ 1 = 0
Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct

Goal state before:
pp: M : Type u_3
N : Type u_1
α : Type u_4
β : Type u_2
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableConstSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : SMul N β
inst✝ : ContinuousConstSMul N β
⊢ ∀ (m : Mᵈᵐᵃ) (n : N) (a : α →ₘ[μ] β), m • n • a = n • m • a

Tactic:
rintro _ _ ⟨_⟩; rfl

Goal state after:
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' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ extend (fun x x_1 ↦ m x) ∅ = 0

Tactic:
extend_eq,

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ m ∅ = 0

case h
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ ∅ ∈ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
hS : (↑S).PairwiseDisjoint s
⊢ m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)

Tactic:
induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    simp only [Finset.coe_insert, Set.pairwiseDisjoint_insert] at hS
    rw [← h hs.2 hS.1]
    refine addContent_union hC hs.1 (hC.biUnion_mem S hs.2) ?_
    rw [disjoint_iUnion₂_right]
    exact fun j hjS ↦ hS.2 j hjS (ne_of_mem_of_not_mem hjS hiS).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
M : ℕ
⊢ AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ

Tactic:
apply hf.1.indicator

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
M : ℕ
⊢ MeasurableSet {x | ↑M ≤ ↑‖f x‖₊}
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
inst✝ : T2Space M
ι : Type u_4
s : Set ι
f : ι → Set α
hs : s.Countable
hd : s.Pairwise (Disjoint on f)
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ v (⋃ b ∈ s, f b) = ∑' (p : ↑s), v (f ↑p)

Tactic:
by
  have := hs.toEncodable
  rw [biUnion_eq_iUnion]
  apply of_disjoint_iUnion
  · exact fun x ↦ h x x.2
  · exact hd.on_injective Subtype.coe_injective fun x => x.2

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ s A
hB₂ : 0 ≤ s B
hAB : s (A ∪ B) = 0
⊢ s A = 0

Tactic:
rw [of_union h hA₁ hB₁] at hAB

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ s A
hB₂ : 0 ≤ s B
hAB : s A + s B = 0
⊢ s A = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : s A ≤ 0
hB₂ : s B ≤ 0
hAB : s (A ∪ B) = 0
⊢ s A = 0

Tactic:
rw [of_union h hA₁ hB₁] at hAB

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : s A ≤ 0
hB₂ : s B ≤ 0
hAB : s A + s B = 0
⊢ s A = 0
Module: Mathlib.MeasureTheory.Measure.Complex

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : μ i = 0
⊢ c i = 0

Tactic:
rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)]

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0

α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : μ i = 0
⊢ (c i).im = 0

α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : μ i = 0
⊢ (c i).re = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ s.someExistsOneDivLT i ⊆ i ∧
    MeasurableSet (s.someExistsOneDivLT i) ∧ 1 / (↑(s.findExistsOneDivLT i) + 1) < s (s.someExistsOneDivLT i)

Tactic:
someExistsOneDivLT,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ (if hi : ¬s ≤[i] 0 then Classical.choose ⋯ else ∅) ⊆ i ∧
    MeasurableSet (if hi : ¬s ≤[i] 0 then Classical.choose ⋯ else ∅) ∧
      1 / (↑(s.findExistsOneDivLT i) + 1) < s (if hi : ¬s ≤[i] 0 then Classical.choose ⋯ else ∅)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ s.someExistsOneDivLT i ⊆ i

Tactic:
someExistsOneDivLT,

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ (if hi : ¬s ≤[i] 0 then Classical.choose ⋯ else ∅) ⊆ i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet (s.someExistsOneDivLT i)

Tactic:
someExistsOneDivLT,

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet (if hi : ¬s ≤[i] 0 then Classical.choose ⋯ else ∅)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
⊢ ¬s ≤[i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k] 0

Tactic:
refine mt (restrict_le_zero_subset _ ?_ (by simp)) hn

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
⊢ MeasurableSet (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n < m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
by
  rw [Set.eq_empty_iff_forall_notMem]
  rintro x ⟨hx₁, hx₂⟩
  cases m; · lia
  · 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.Hahn

Goal state before:
pp: case e'_3
α : 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)
n : ℕ
⊢ (fun l ↦ ⋃ (_ : l ≤ n), s.restrictNonposSeq i l) = fun l ↦ ⋃ (_ : l < n + 1), s.restrictNonposSeq i l

Tactic:
ext l
        simp only [exists_prop, Set.mem_iUnion, and_congr_left_iff]
        exact fun _ => Nat.lt_succ_iff.symm

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

Goal state before:
pp: case e'_4
α : 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)
n : ℕ
⊢ (fun l ↦ ⋃ (_ : l ≤ n), s.restrictNonposSeq i l) = fun l ↦ ⋃ (_ : l < n + 1), s.restrictNonposSeq i l

Tactic:
ext l
        simp only [exists_prop, Set.mem_iUnion, and_congr_left_iff]
        exact fun _ => Nat.lt_succ_iff.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n ↦ f ↑n
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ℕ) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
have hF : ∀ n, MemLp (F n) p μ := fun n => hf n

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n ↦ f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ℕ) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ

Tactic:
· rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by
      simpa [hc] using h.smul_measure c⁻¹]
    simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ∞
⊢ StronglyMeasurable (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))

Tactic:
exact (SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : p ≠ 0
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, μ[fun x ↦ ‖f x‖ ^ p | m] x ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ^ p ∂μ

Tactic:
by
    apply setIntegral_condExp_le_of_ae_nonneg hs
    filter_upwards with ω using by positivity

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 g : ι → α → β
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C
⊢ UniformIntegrable g p μ

Tactic:
refine ⟨fun i => (hfm i).congr (hfg i), (unifIntegrable_congr_ae hfg).1 hunif, C, fun i => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C
i : ι
⊢ eLpNorm (g i) p μ ≤ ↑C
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
m : Measure (Measure α)
inst✝ : IsProbabilityMeasure m
hm : ∀ᵐ (μ : Measure α) ∂m, IsProbabilityMeasure μ
⊢ IsProbabilityMeasure m.join

Tactic:
by
  simp only [isProbabilityMeasure_iff, MeasurableSet.univ, Measure.join_apply]
  simp_rw [isProbabilityMeasure_iff] at hm
  exact lintegral_eq_const hm

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

Goal state before:
pp: ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else univ) = ⋂ i, Y i ⁻¹' t i ∩ if i ∈ s then f i else univ

Tactic:
rw [Set.iInter_inter_distrib]

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

Goal state before:
pp: case e_a.e_6
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := ⋯
⊢ (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i = ⋂ i, g i

Tactic:
calc
        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
          simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]
        _ = ⋂ i, Y i ⁻¹' t i ∩ (if i ∈ s then f i else .univ) := by rw [Set.iInter_inter_distrib]
        _ = _ := Set.iInter_congr fun i ↦ by by_cases hi : i ∈ s <;> simp [hi, g]

Goal state after: