mathlib-initiative/mathlib-tactics huggingface dataset:
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
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
m : ι
hml : m ≠ l
contra : P.root m = P.root ↑i + P.root k
⊢ P.root m = P.root l

Tactic:
rw [hl, contra, hk₁]; module

Goal state after:
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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
⊢ chainBotCoeff i j = if P.pairingIn ℤ i j = 0 then 1 else 0

Tactic:
have aux₂ := P.chainBotCoeff_add_chainTopCoeff_le_two i j

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
aux₂ : chainBotCoeff i j + chainTopCoeff i j ≤ 2
⊢ chainBotCoeff i j = if P.pairingIn ℤ i j = 0 then 1 else 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inr.inr
ι : 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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k l : ι
hki : k ≠ ↑i
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)

Tactic:
rcases eq_or_ne k (-i) with rfl | hki'

Goal state after:
case inr.inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -↑i ≠ ↑i
⊢ ⁅e i, f i⁆ (Sum.inr (-↑i)) (Sum.inr l) = h i (Sum.inr (-↑i)) (Sum.inr l)

case inr.inr.inr.inr
ι : 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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k l : ι
hki : k ≠ ↑i
hki' : k ≠ -↑i
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)
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
i : ι
hi : P.root i ∉ allRoots P
h₁ : P.IsOrthogonal i (short P)
h₂ : P.IsOrthogonal i (long P)
this✝ : Fintype ι
B : P.InvariantForm
this : Module.IsReflexive R M
⊢ False

Tactic:
rw [isOrthogonal_iff_pairing_eq_zero, ← B.apply_root_root_zero_iff] at h₁ h₂

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
i : ι
hi : P.root i ∉ allRoots P
this✝ : Fintype ι
B : P.InvariantForm
h₂ : (B.form (P.root i)) (P.root (long P)) = 0
h₁ : (B.form (P.root i)) (P.root (short P)) = 0
this : Module.IsReflexive R M
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
i j : ↥b.support
hij : i ≠ j
⊢ ⁅⟨e i, ⋯⟩, ⟨f j, ⋯⟩⁆ = 0

Tactic:
simp [Subtype.ext_iff, lie_e_f_ne hij]

Goal state after:
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 ↑y) ↑x * (2 * (B ↑x) z) = (B ↑x) ↑x * (2 * (IsReflective.coroot B ⋯) ↑y) * (B z) ↑x

Tactic:
mul_left_comm (B x x),

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

Goal state before:
pp: case refine_2
ι : 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
⊢ span K (range u) ≤ ↑(genWeightSpace (↥b.support ⊕ ι → K) 0)

Tactic:
rw [span_le]
    rintro - ⟨i, rfl⟩
    simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule, mem_genWeightSpace]
    rintro ⟨⟨x, -⟩, hx⟩
    exact ⟨1, funext fun j ↦ by simpa using apply_sum_inl_eq_zero_of_mem_span_h i j hx⟩

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
s : Multiset α
⊢ ¬CutExpand r s 0

Tactic:
by
  classical
  rw [cutExpand_iff]
  rintro ⟨_, _, _, ⟨⟩, _⟩

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

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
this : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑(transvection hfv * e)).fixedSubmodule
⊢ transvection hfv ∈ dilatransvections K V

Tactic:
exact transvection_mem_dilatransvections hfv

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

Goal state before:
pp: case neg
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
hi₁ : i ∉ s₁
⊢ f i ∈ t₁' i

Tactic:
h1' i hi₁

Goal state after:
case neg
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
hi₁ : i ∉ s₁
⊢ f i ∈ univ
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ : Measure ((i : ι) → α i)
h : IsProjectiveLimit μ P
I : Finset ι
s : Set ((i : ↥I) → α ↑i)
hs : MeasurableSet s
⊢ μ (cylinder I s) = (P I) s

Tactic:
rw [cylinder, ← Measure.map_apply _ hs, h I]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ : Measure ((i : ι) → α i)
h : IsProjectiveLimit μ P
I : Finset ι
s : Set ((i : ↥I) → α ↑i)
hs : MeasurableSet s
⊢ Measurable I.restrict
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case neg
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₁ : i ∉ s₁
⊢ t₁' i ∈ C i

Tactic:
h1' i hi₁

Goal state after:
case neg
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₁ : i ∉ s₁
⊢ univ ∈ C i
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case convert_2
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝¹ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
inst✝ : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ i, f i ∈ C
⊢ (↑Finset.univ).PairwiseDisjoint f

pp: case convert_3
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝¹ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
inst✝ : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ i, f i ∈ C
⊢ ⋃ i ∈ Finset.univ, f i ∈ C

Tactic:
· simpa [Set.PairwiseDisjoint, Set.pairwise_univ] using h_dis

Goal state after:
case convert_3
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝¹ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
inst✝ : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ i, f i ∈ C
⊢ ⋃ i ∈ Finset.univ, f i ∈ C
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun A ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
⊢ (generateSetAlgebra 𝒜).Countable

Tactic:
let 𝒟 := {A | A.Finite ∧ A ⊆ 𝒞}

Goal state after:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun A ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A | A.Finite ∧ A ⊆ 𝒞}
⊢ (generateSetAlgebra 𝒜).Countable
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
x : V
a✝ : x ∈ ⊤
h1 : g (e x) • (v - e v) ∈ K ∙ (e v - v)
hle : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v
h2 : c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v
⊢ x ∈ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v

Tactic:
simpa [smul_smul, inv_mul_cancel₀ hc0] using Submodule.smul_mem _ c⁻¹ h2

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 ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
⊢ μ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ≤ 0

Tactic:
refine (measure_mono this).trans ?_

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
⊢ μ {x | eLpNormEssSup f μ < ↑‖f x‖₊} ≤ 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case neg.refine_7
Ω : 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Ω
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
this : μ[fun ω ↦ (B (f ω)) (μ[g | m] ω) | m] = fun ω ↦ (B (f ω)) (μ[g | m] ω)
n : ℕ
x✝ : Ω
⊢ ‖B‖ * ‖(fs n) x✝‖ * ‖g x✝‖ ≤ ‖B‖ * c * ‖g x✝‖

Tactic:
hfs_bound

Goal state after:
case neg.refine_7
Ω : 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Ω
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
this : μ[fun ω ↦ (B (f ω)) (μ[g | m] ω) | m] = fun ω ↦ (B (f ω)) (μ[g | m] ω)
n : ℕ
x✝ : Ω
⊢ ‖B‖ * c * ‖g x✝‖ ≤ ‖B‖ * c * ‖g x✝‖
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case neg.refine_8
Ω : 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Ω
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
this : μ[fun ω ↦ (B (f ω)) (μ[g | m] ω) | m] = fun ω ↦ (B (f ω)) (μ[g | m] ω)
n : ℕ
x✝ : Ω
⊢ ‖B‖ * ‖(fs n) x✝‖ * ‖μ[g | m] x✝‖ ≤ ‖B‖ * c * ‖μ[g | m] x✝‖

Tactic:
hfs_bound

Goal state after:
case neg.refine_8
Ω : 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Ω
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
this : μ[fun ω ↦ (B (f ω)) (μ[g | m] ω) | m] = fun ω ↦ (B (f ω)) (μ[g | m] ω)
n : ℕ
x✝ : Ω
⊢ ‖B‖ * c * ‖μ[g | m] x✝‖ ≤ ‖B‖ * c * ‖μ[g | m] x✝‖
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : 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
⊢ j₁.posPart.real i = j₁.posPart.real (i ∩ Sᶜ) - j₁.negPart.real (i ∩ Sᶜ)

Tactic:
measureReal_def (μ := j₁.negPart),

Goal state after:
α : 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
⊢ j₁.posPart.real i = j₁.posPart.real (i ∩ Sᶜ) - (j₁.negPart (i ∩ Sᶜ)).toReal
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
⊢ s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)

Tactic:
hA,

Goal state after:
α : 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
⊢ s i = s (i \ ⋃ l, s.restrictNonposSeq i l) + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

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

Tactic:
have hℒp := hf

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

Goal state before:
pp: case pos
α : 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)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

Tactic:
have h₃ : Tendsto (fun n => (bdd n : ℝ) + 1) atTop atTop := by
    simp only [one_div] at h₃'
    exact Summable.tendsto_atTop_of_pos h₃' fun n => Nat.cast_add_one_pos (bdd n)

Goal state after:
case pos
α : 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
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case neg.posPart
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ (r • s).toJordanDecomposition.posPart = (r • s.toJordanDecomposition).posPart

Tactic:
rw [real_smul_posPart_neg _ _ hr,
        show r • s = -(-r • s) by rw [neg_smul, neg_neg], toJordanDecomposition_neg, neg_posPart,
        toJordanDecomposition_smul_real_nonneg, ← smul_negPart, real_smul_nonneg]
      all_goals exact Left.nonneg_neg_iff.2 hr.le

Goal state after: