mathlib-initiative/mathlib-tactics huggingface dataset:
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
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 : ι
hj : j ∈ b.support
hj₀ : P.pairingIn ℤ j i ≠ 0
⊢ ∃ j, P.pairingIn ℤ i ↑j ≠ 0

Tactic:
ne_eq,

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.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 : ι
hj : j ∈ b.support
hj₀ : ¬P.pairingIn ℤ j i = 0
⊢ ∃ j, P.pairingIn ℤ i ↑j ≠ 0
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
⊢ (↑e).fixedSubmodule ⊔ K ∙ v = (↑(transvection hfv * e)).fixedSubmodule

Tactic:
apply Submodule.eq_of_le_of_finrank_le this
    rw [finrank_sup_span_singleton hv, add_comm]
    apply finrank_fixedSubmodule_dilatransvection_mul_le
    exact transvection_mem_dilatransvections hfv

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

Goal state before:
pp: case hv
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
hu' : u ∈ ker f
⊢ False

Tactic:
mem_ker

Goal state after:
case hv
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
hu' : f u = 0
⊢ False
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
⊢ ⋂ i, ⋂ (_ : i ≤ n), s i ∈ C

Tactic:
induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [biInter_le_succ]; exact hC.inter_mem hn (hs _)

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
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 ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid s).parts → Finpartition t
hQ : ∀ (t : Set α) (a : t ∈ (P.avoid s).parts), ↑(Q t a).parts ⊆ C
⊢ s ∈ C ∧ ⋃ x ∈ ↑(P.avoid s).parts.attach, ↑(Q ↑x ⋯).parts ⊆ C

Tactic:
iUnion₂_subset_iff,

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 ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid s).parts → Finpartition t
hQ : ∀ (t : Set α) (a : t ∈ (P.avoid s).parts), ↑(Q t a).parts ⊆ C
⊢ s ∈ C ∧ ∀ i ∈ ↑(P.avoid s).parts.attach, ↑(Q ↑i ⋯).parts ⊆ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case convert_2
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
i j : Fin (Nat.succ 0).succ
hij : i ≠ j
⊢ (Disjoint on ![s, t]) i j

Tactic:
fin_cases i <;> fin_cases j

Goal state after:
case convert_2.«0».«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case convert_2.«0».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case convert_2.«1».«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case convert_2.«1».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
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
𝒟 : Set (Set (Set (Set α))) := {A | A.Finite ∧ A ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
⊢ (generateSetAlgebra 𝒜).Countable

Tactic:
have : generateSetAlgebra 𝒜 ⊆ f '' 𝒟 := by
    intro s s_mem
    rcases mem_generateSetAlgebra_elim s_mem with ⟨A, A_fin, mem_A, hA, rfl⟩
    exact ⟨A, ⟨A_fin, fun a ha ↦ ⟨mem_A a ha, hA a ha⟩⟩, rfl⟩

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 ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
this : generateSetAlgebra 𝒜 ⊆ f '' 𝒟
⊢ (generateSetAlgebra 𝒜).Countable
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inr.coe.coe
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb : b < a
⊢ ∃ t ⊆ Iio ↑a, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ ↑b ∈ t

Tactic:
obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Iio a := h_basis.isOpen_iff.1 (isOpen_Iio' a) b hb

Goal state after:
case a.inr.coe.coe
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ ∃ t ⊆ Iio ↑a, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ ↑b ∈ t
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⨆ x, ↑(J.equivFin.symm x)
⊢ m t ≤ ∑ u ∈ J, m u

Tactic:
iSup_eq_iUnion,

Goal state after:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃ x, ↑(J.equivFin.symm x)
⊢ m t ≤ ∑ u ∈ J, m u
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
⊢ e ∈ transvections K V * (transvections K V ^ n * dilatransvections K V)

Tactic:
Set.mem_mul

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
n✝ : ℕ
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h : ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
h_ss : ↑(insert s I) ⊆ C
h_dis : (↑(insert s I)).PairwiseDisjoint id
h_mem : ⋃₀ ↑(insert s I) ∈ C
⊢ m (⋃₀ ↑(insert s I)) = ∑ u ∈ insert s I, m u

Tactic:
rw [Finset.coe_insert] at *

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h : ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
h_ss : insert s ↑I ⊆ C
h_dis : (insert s ↑I).PairwiseDisjoint id
h_mem : ⋃₀ insert s ↑I ∈ C
⊢ m (⋃₀ insert s ↑I) = ∑ u ∈ insert s I, m u
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
⊢ μ[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)

Tactic:
by_cases hm : m ≤ mΩ

Goal state after:
case pos
Ω : 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
⊢ μ[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)

case neg
Ω : 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : ¬m ≤ mΩ
⊢ μ[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)
Module: Mathlib.MeasureTheory.Measure.Complex

Goal state before:
pp: case fst
α : Type u_1
m : MeasurableSpace α
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
r : R
c : ComplexMeasure α
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ (equivSignedMeasure (r • c)).1 i✝ = (r • equivSignedMeasure c).1 i✝

pp: case snd
α : Type u_1
m : MeasurableSpace α
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
r : R
c : ComplexMeasure α
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ (equivSignedMeasure (r • c)).2 i✝ = (r • equivSignedMeasure c).2 i✝

Tactic:
· simp [Complex.smul_re]

Goal state after:
case snd
α : Type u_1
m : MeasurableSpace α
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
r : R
c : ComplexMeasure α
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ (equivSignedMeasure (r • c)).2 i✝ = (r • equivSignedMeasure c).2 i✝
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ (if MeasurableSet (⋃ i, g i) then v (⋃ i, f ⁻¹' g i) else 0) = v (⋃ i, f ⁻¹' g i)

Tactic:
if_pos (MeasurableSet.iUnion hg₁)

Goal state after:
case e'_6
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ v (⋃ i, f ⁻¹' g i) = v (⋃ i, f ⁻¹' g i)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
hx : x ∉ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}
⊢ 0 ^ p.toReal = 0

Tactic:
simp [ENNReal.toReal_pos hp_ne_zero hp_ne_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
⊢ (∀ (i : ℕ), MeasurableSet (f i)) →
    Pairwise (Disjoint on f) →
      HasSum (fun i_1 ↦ if MeasurableSet (f i_1) then v (f i_1 ∩ i) else 0)
        (if MeasurableSet (⋃ i, f i) then v ((⋃ i, f i) ∩ i) else 0)

Tactic:
hf₁

Goal state after:
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
⊢ Pairwise (Disjoint on f) →
    HasSum (fun i_1 ↦ if MeasurableSet (f i_1) then v (f i_1 ∩ i) else 0)
      (if MeasurableSet (⋃ i, f i) then v ((⋃ i, f i) ∩ i) else 0)
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 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε

Tactic:
(_ : f = { x : α | M ≤ ‖f x‖₊ }.indicator f + { x : α | ‖f x‖ < M }.indicator f)

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 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator ({x | M ≤ ↑‖f x‖₊}.indicator f + {x | ‖f x‖ < M}.indicator f)) p μ ≤ 2 * ENNReal.ofReal ε

α : 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 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ f = {x | M ≤ ↑‖f x‖₊}.indicator f + {x | ‖f x‖ < M}.indicator f
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ 0 ≤[Sᶜ] j.toSignedMeasure

Tactic:
· refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_
    rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def (μ := j.negPart),
      show j.negPart A = 0 from nonpos_iff_eq_zero.1 (hS₃ ▸ measure_mono hA₁), ENNReal.toReal_zero,
      sub_zero]
    exact ENNReal.toReal_nonneg

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : w s = 0
⊢ (-v) s = 0

Tactic:
rw [neg_apply, h hs, neg_zero]

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

Goal state before:
pp: case mp.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, t t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ (t.toMeasureOfZeroLE j hj₁ hj₂) uᶜ + t.toJordanDecomposition.negPart uᶜ = 0

Tactic:
hjneg,

Goal state after:
case mp.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, t t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ (t.toMeasureOfZeroLE j hj₁ hj₂) uᶜ + (t.toMeasureOfLEZero jᶜ ⋯ hj₃) uᶜ = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
⊢ ∀ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      s.toMeasureOfZeroLE' i hi₂ (⋃ i, f i) ⋯ = ∑' (i_1 : ℕ), s.toMeasureOfZeroLE' i hi₂ (f i_1) ⋯

Tactic:
hf₁

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
⊢ Pairwise (Disjoint on f) →
    s.toMeasureOfZeroLE' i hi₂ (⋃ i, f i) ⋯ = ∑' (i_1 : ℕ), s.toMeasureOfZeroLE' i hi₂ (f i_1) ⋯
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ (μ tᶜ).toReal ^ (1 / p.toReal) * (1 / ↑(measureUnivNNReal μ) ^ (1 / p.toReal)) ≤ 1

Tactic:
mul_one_div,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ (μ tᶜ).toReal ^ (1 / p.toReal) / ↑(measureUnivNNReal μ) ^ (1 / p.toReal) ≤ 1