mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : 0 ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairingIn ℤ i k ≤ -2
contra : P.root k + P.root i = 0
⊢ False

Tactic:
exact P.ne_zero _ hk'.choose_spec

Goal state after:
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 : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : P.root k ≠ -P.root i
hk' : P.root k - P.root j ∈ range ⇑P.root
_i : InvolutiveNeg ι := P.indexNeg
hk : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
⊢ P.root (-k) + P.root j ∈ range ⇑P.root

Tactic:
convert! P.neg_mem_range_root_iff.mpr hk' using 1; simp [neg_add_eq_sub]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inr
ι : 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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i j : ι
k : ↥b.support
h : P.root i = P.root j + P.root ↑k
l : ι
⊢ ⁅f k, v b i⁆ (Sum.inr l) = ((↑(chainTopCoeff (↑k) i) + 1) • v b j) (Sum.inr l)

Tactic:
· simp [f, h, Pi.single_apply]

Goal state after:
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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i✝ : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
i : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hi : v b i ∈ ωConjLieSubmodule U
j : ↥b.support
hj : u j ∈ ωConjLieSubmodule U
⊢ u j ∈ U

Tactic:
simpa [hωu] using! hj

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case 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 j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k : ι
l : ↥b.support
aux₁ : P.root k ≠ P.root ↑i - P.root ↑j
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inl l) = 0 (Sum.inr k) (Sum.inl l)

Tactic:
simp [e, f, ← sub_eq_add_neg, if_neg aux₁]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case refine_1
ι : 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
w : ↥b.support ⊕ ι → K
i : ι
hw : ∀ (x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) (hx : x ∈ lieAlgebra b), ⟨x, hx⟩ ∈ H → ∃ k, (toLin' x ^ k) w = 0
j : ↥b.support
hj : P.pairingIn ℤ i ↑j ≠ 0
⊢ w (Sum.inr i) = 0

Tactic:
obtain ⟨k, hk⟩ := hw (h j) (h_mem_lieAlgebra j) (h_mem_cartanSubalgebra' j _)

Goal state after:
case refine_1
ι : 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
w : ↥b.support ⊕ ι → K
i : ι
hw : ∀ (x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) (hx : x ∈ lieAlgebra b), ⟨x, hx⟩ ∈ H → ∃ k, (toLin' x ^ k) w = 0
j : ↥b.support
hj : P.pairingIn ℤ i ↑j ≠ 0
k : ℕ
hk : (toLin' (h j) ^ k) w = 0
⊢ w (Sum.inr i) = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : 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
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
h₇ : P.root l - P.root ↑j ∉ range ⇑P.root
aux₃ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)
x : ι
hx : P.root x = P.root l - P.root ↑j
hx' : P.root k = P.root ↑i + P.root x
⊢ False

Tactic:
exact h₇ ⟨x, hx⟩

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: case refine_1
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), 0 ≤ (B x) x
x : n → R
⊢ 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x

Tactic:
rw [star_dotProduct_toMatrix₂_mulVec]

Goal state after:
case refine_1
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), 0 ≤ (B x) x
x : n → R
⊢ 0 ≤ (B (b.equivFun.symm x)) (b.equivFun.symm x)
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
x : V
hx : x ∈ (↑e).fixedSubmodule
⊢ x ∈ (↑(transvection hfv)).fixedSubmodule

Tactic:
by
    rw [mem_fixedSubmodule_transvection_iff, smul_eq_zero]
    left
    rw [← Submodule.mem_bot K, ← hf]
    exact mem_map_of_mem hx

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 f✝ : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
⊢ u - e u ∈ K ∙ (e u - u)

Tactic:
rw [mem_span_singleton]

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f✝ : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
⊢ ∃ a, a • (e u - u) = u - e u
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
⊢ squareCylinders C = ⋃ s, (fun t ↦ (↑s).pi t) '' univ.pi C

Tactic:
ext1 f

Goal state after:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
f : Set ((i : ι) → α i)
⊢ f ∈ squareCylinders C ↔ f ∈ ⋃ s, (fun t ↦ (↑s).pi t) '' univ.pi C
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
⊢ (cylinder s S)ᶜ = cylinder s Sᶜ

Tactic:
ext1 f

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
f : (i : ι) → α i
⊢ f ∈ (cylinder s S)ᶜ ↔ f ∈ cylinder s Sᶜ
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
S T : Set ((i : ↥s) → α ↑i)
⊢ cylinder s S \ cylinder s T = cylinder s (S \ T)

Tactic:
ext1 f

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S T : Set ((i : ↥s) → α ↑i)
f : (i : ι) → α i
⊢ f ∈ cylinder s S \ cylinder s T ↔ f ∈ cylinder s (S \ T)
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict x ∈ S ↔ J.restrict x ∈ T
⊢ S = Finset.restrict₂ hJI ⁻¹' T

Tactic:
ext1 f

Goal state after:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict x ∈ S ↔ J.restrict x ∈ T
f : (i : ↥I) → α ↑i
⊢ f ∈ S ↔ f ∈ Finset.restrict₂ hJI ⁻¹' T
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
J : Finset ι
⊢ cylinder I S = cylinder (I ∪ J) (Finset.restrict₂ ⋯ ⁻¹' S)

Tactic:
ext1 f

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
J : Finset ι
f : (i : ι) → α i
⊢ f ∈ cylinder I S ↔ f ∈ cylinder (I ∪ J) (Finset.restrict₂ ⋯ ⁻¹' S)
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert.inl
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
a✝ : ⊥ ∉ S
hsC : ⊥ ∈ C
⊢ ∃ P, ↑P.parts ⊆ C

pp: case insert.inr
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
hs : s ≠ ⊥
⊢ ∃ P, ↑P.parts ⊆ C

Tactic:
· rw [sup_bot_eq]; exact ⟨P, hP⟩

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

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

Tactic:
by
  intro s hs
  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: 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
y : V
hy : -y ∈ (↑e).fixedSubmodule
k : K
hk : v - e v = y + k • v
⊢ (k - 1) • v + 1 • e v = -y

Tactic:
← sub_eq_iff_eq_add

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
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
y : V
hy : -y ∈ (↑e).fixedSubmodule
k : K
hk : v - e v - k • v = y
⊢ (k - 1) • v + 1 • e v = -y
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
d a : ι
⊢ Tendsto (untopD d) (Filter.map some (𝓝 a)) (𝓝 (untopD d ↑a))

Tactic:
tendsto_map'_iff

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
d a : ι
⊢ Tendsto (untopD d ∘ some) (𝓝 a) (𝓝 (untopD d ↑a))
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

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

Tactic:
rw [ennrealToMeasure, ofMeasurable_apply _ hs]

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

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

Tactic:
toENNRealVectorMeasure_apply_measurable hs,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ μ.ennrealToMeasure s = μ s
Module: Mathlib.MeasureTheory.Measure.Complex

Goal state before:
pp: case mp.left
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ re c ≪ᵥ μ

Tactic:
intro i hi; simp [h hi]

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

Goal state before:
pp: case mp.right
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ im c ≪ᵥ μ

Tactic:
intro i hi; simp [h hi]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ 0 ≤ w j

Tactic:
w.not_measurable hj₁

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ 0 ≤ 0
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
⊢ ∀ {f : Fin (n + 1) → α → β}, (∀ (i : Fin (n + 1)), MemLp (f i) p μ) → UnifIntegrable f p μ

Tactic:
intro f hfLp ε hε
    let g : Fin n → α → β := fun k => f k.castSucc
    have hgLp : ∀ i, MemLp (g i) p μ := fun i => hfLp i.castSucc
    obtain ⟨δ₁, hδ₁pos, hδ₁⟩ := h hgLp hε
    obtain ⟨δ₂, hδ₂pos, hδ₂⟩ := (hfLp (Fin.last n)).eLpNorm_indicator_le hp_one hp_top hε
    refine ⟨min δ₁ δ₂, lt_min hδ₁pos hδ₂pos, fun i s hs hμs => ?_⟩
    by_cases! hi : i.val < n
    · rw [(_ : f i = g ⟨i.val, hi⟩)]
      · exact hδ₁ _ s hs (le_trans hμs <| ENNReal.ofReal_le_ofReal <| min_le_left _ _)
      · simp [g]
    · obtain rfl : i = Fin.last n := Fin.ext (le_antisymm (Fin.is_le i) hi)
      exact hδ₂ _ hs (le_trans hμs <| ENNReal.ofReal_le_ofReal <| min_le_right _ _)

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 : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensityᵥ (f • g)) s = ((μ.withDensity fun x ↦ ↑(f x)).withDensityᵥ g) s

Tactic:
rw [withDensityᵥ_apply hfg hs,
    withDensityᵥ_apply ((integrable_withDensity_iff_integrable_smul₀ hf).mpr hfg) hs,
    setIntegral_withDensity_eq_setIntegral_smul₀ hf.restrict _ hs]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (f • g) x ∂μ = ∫ (x : α) in s, f x • g x ∂μ
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ((μ.withDensityᵥ f).trim hm) i = ∫ (x : α) in i, f x ∂μ

Tactic:
by
  rw [VectorMeasure.trim_measurableSet_eq hm hi, withDensityᵥ_apply hf (hm _ hi)]

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 ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ℕ) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
let F : Fin N → α → β := fun n => f 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
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ℕ) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ((c.singularPart μ) i).im + (∫ (x : α) in i, c.rnDeriv μ x ∂μ).im = { re := (re c) i, im := (im c) i }.im

Tactic:
← RCLike.im_eq_complex_im,

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ RCLike.im ((c.singularPart μ) i) + RCLike.im (∫ (x : α) in i, c.rnDeriv μ x ∂μ) =
    RCLike.im { re := (re c) i, im := (im c) i }
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type u_2
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
⊢ ⇑(c • μ) = c • ⇑μ

Tactic:
funext; simp [← ENNReal.coe_inj, ENNReal.coe_smul]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (s n) x) u (𝓝 (f x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 ↦ t.indicator (fn (s x_1)) x) u (𝓝 (t.indicator ((fun f ↦ ↑f) ⟨f, ⋯⟩) x))

Tactic:
· filter_upwards [hs] with a ha
    by_cases memt : a ∈ t
    · simpa [memt]
    · simp [memt]

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ (μs i).testAgainstNN 0 + nndist f 0 * (μs i).mass
⊢ Tendsto (fun b ↦ dist ((μs b).testAgainstNN f) 0) F (𝓝 0)

Tactic:
simp_rw [testAgainstNN_zero, zero_add] at obs

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
⊢ Tendsto (fun b ↦ dist ((μs b).testAgainstNN f) 0) F (𝓝 0)
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
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i ↦ (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
by
  have lim_mass := μs_lim.mass
  have aux : {(0 : ℝ≥0)}ᶜ ∈ 𝓝 μ.mass :=
    isOpen_compl_singleton.mem_nhds (μ.mass_nonzero_iff.mpr nonzero)
  have eventually_nonzero : ∀ᶠ i in F, μs i ≠ 0 := by
    simp_rw [← mass_nonzero_iff]
    exact lim_mass aux
  have eve : ∀ᶠ i in F,
      (μs i).normalize.toFiniteMeasure.testAgainstNN f =
        (μs i).mass⁻¹ * (μs i).testAgainstNN f := by
    filter_upwards [eventually_iff.mp eventually_nonzero]
    intro i hi
    apply normalize_testAgainstNN _ hi
  simp_rw [tendsto_congr' eve, μ.normalize_testAgainstNN nonzero]
  have lim_pair :
    Tendsto (fun i ↦ (⟨(μs i).mass⁻¹, (μs i).testAgainstNN f⟩ : ℝ≥0 × ℝ≥0)) F
      (𝓝 ⟨μ.mass⁻¹, μ.testAgainstNN f⟩) := by
    refine (Prod.tendsto_iff _ _).mpr ⟨?_, ?_⟩
    · exact (continuousOn_inv₀.continuousAt aux).tendsto.comp lim_mass
    · exact tendsto_iff_forall_testAgainstNN_tendsto.mp μs_lim f
  exact tendsto_mul.comp lim_pair

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

Goal state before:
pp: case refine_1
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝ : TopologicalSpace 𝓧
h : ∀ (ε : ENNReal), 0 < ε → ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε
ε : ENNReal
hε : 0 < ε
⊢ ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

pp: case refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝ : TopologicalSpace 𝓧
h : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
⊢ ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε

Tactic:
· obtain ⟨A, ⟨K, h1, h2⟩, hA⟩ := h ε hε
    exact ⟨K, h1, hA Kᶜ h2⟩

Goal state after:
case refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝ : TopologicalSpace 𝓧
h : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
⊢ ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε