mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ∀ (a : Matrix.ProjectiveSpecialLinearGroup ι K), PSLAction.toPermHom a = 1 → a = 1

Tactic:
intro g hg

Goal state after:
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg : PSLAction.toPermHom g = 1
⊢ g = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ IsUnit 1

pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ max (Module.finrank R V) 1 ≠ 0

Tactic:
· exact isUnit_one

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ max (Module.finrank R V) 1 ≠ 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
⊢ Submodule.map (↑e.toLinearEquiv) Q.radical = Q'.radical

Tactic:
by
  ext
  simp [mem_radical_iff', ← e.map_app, -map_app, e.toEquiv.forall_congr_left]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : Module R M
Q : QuadraticForm R M
⊢ sigPos Q ≤ Module.finrank R M

Tactic:
exact mem_Iic.mp <| mem_of_mem_filter _ <| max'_mem _ _

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_4
ι : 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
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P) =
    (P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (shortAddLongRoot P)) (shortAddLongRoot P)

Tactic:
rw [long_eq_three_mul_short, shortAddLongRoot_shortRoot]

Goal state after:
case calc_4
ι : 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
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (3 * (B.form (shortRoot P)) (shortRoot P)) =
    (P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (shortRoot P)) (shortRoot P)
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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
hki : P.pairing k i = 0
⊢ P.pairing j i = -P.pairing m i

Tactic:
simp only [← root_coroot_eq_pairing, ← h₂]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
hki : P.pairing k i = 0
⊢ (P.toLinearMap (P.root j)) (P.coroot i) = -(P.toLinearMap (P.root k - P.root j)) (P.coroot i)
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
e : SymmetricAlgebra R M ≃ₐ[R] A
he : ↑↑e ∘ₗ SymmetricAlgebra.ι R M = f
h : ↑e = SymmetricAlgebra.lift f
⊢ IsSymmetricAlgebra f

Tactic:
by
    change Function.Bijective _
    exact h ▸ e.bijective

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
b : α
h : (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) b a
he : count b (s + {a}) = count b (t + u)
⊢ count b s = count b t

Tactic:
simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)]
      using he

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h' : a' ∈ s.erase a + t
⊢ p a'

Tactic:
obtain (h' | h') := mem_add.1 h'

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h'✝ : a' ∈ s.erase a + t
h' : a' ∈ s.erase a
⊢ p a'

case inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h'✝ : a' ∈ s.erase a + t
h' : a' ∈ t
⊢ p a'
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; simp only [mem_compl_iff, mem_cylinder]

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

Goal state before:
pp: ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
⊢ Measurable Δ.domRestrict

Tactic:
rw [@measurable_pi_iff]

Goal state after:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
⊢ ∀ (a : ↑Δ), Measurable fun x ↦ Δ.domRestrict x a
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
⊢ ∅ ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}

Tactic:
inhabit α
    exact ⟨default, default, le_rfl, by simp⟩

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
hc0 : c = 0
key : ∀ (x : V), g (e x) • (v - e v) ∈ (↑e).fixedSubmodule ⊔ K ∙ v
⊢ ∃ w, g w ≠ 0

Tactic:
contrapose! hg0

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
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
hc0 : c = 0
key : ∀ (x : V), g (e x) • (v - e v) ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hg0 : ∀ (w : V), g w = 0
⊢ g = 0
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun i ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun i ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun i ↦ ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type ?u.192} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (fun j ↦ μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₀ : ∀ (j : ℕ), d ∈ cthickening (r₁ (f j)) (s (f j))
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
j : ℕ
hrp : 0 ≤ r₁ (f j)
hrp' : 0 < r₁ (f j)
⊢ ∃ w ∈ s (f j), d ∈ closedBall w (2 * r₁ (f j))

Tactic:
· simpa using mem_iUnion₂.mp (cthickening_subset_iUnion_closedBall_of_lt (s (f j))
        (by positivity) (lt_two_mul_self hrp') (hf₀ j))

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
h_union : m (t ∪ s \ t) = m t + m (s \ t)
⊢ m (s \ t) = m s - m t

Tactic:
Set.union_sdiff_self,

Goal state after:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
h_union : m (t ∪ s) = m t + m (s \ t)
⊢ m (s \ t) = m s - m t
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
n : ℕ
⊢ m ((partialSups f) n) = m (accumulate (disjointed f) n)

Tactic:
← partialSups_disjointed,

Goal state after:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
n : ℕ
⊢ m ((partialSups (disjointed f)) n) = m (accumulate (disjointed f) n)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : 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 : α
⊢ ‖{x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}.indicator f x‖ₑ ^ p.toReal =
    ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ

Tactic:
enorm_indicator_eq_indicator_enorm,

Goal state after:
α : 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 : α
⊢ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}.indicator (fun a ↦ ‖f a‖ₑ) x ^ p.toReal =
    ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ : blimsup (fun i ↦ cthickening (r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ thickening (r i) (s i)) atTop p
h₂ : blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
⊢ blimsup (fun i ↦ thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ thickening (r i) (s i)) atTop p

Tactic:
replace hr : Tendsto (fun i => M * r i) atTop (𝓝 0) := by convert! hr.const_mul M; simp

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ : blimsup (fun i ↦ cthickening (r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ thickening (r i) (s i)) atTop p
h₂ : blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
hr : Tendsto (fun i ↦ M * r i) atTop (𝓝 0)
⊢ blimsup (fun i ↦ thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ thickening (r i) (s i)) atTop p
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

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

Tactic:
← @Set.sdiff_empty _ i

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i \ ∅] 0
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
⊢ 0 < s (s.someExistsOneDivLT (i \ ∅))
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 : AEStronglyMeasurable f μ
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
⊢ μ[fun ω ↦ (B (AEStronglyMeasurable.mk f hf ω)) (g ω) | m] =ᵐ[μ] fun ω ↦
    (B (AEStronglyMeasurable.mk f hf ω)) (μ[g | m] ω)

Tactic:
by
    refine condExp_bilin_of_stronglyMeasurable_left B hf.stronglyMeasurable_mk
      ((integrable_congr ?_).mp hfg) hg
    filter_upwards [hf.ae_eq_mk] with ω hω using by rw [hω]

Goal state after:
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 : AEStronglyMeasurable f μ
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
⊢ (fun ω ↦ (B (AEStronglyMeasurable.mk f hf ω)) (μ[g | m] ω)) =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)

Tactic:
by
    filter_upwards [hf.ae_eq_mk] with a ha using by rw [ha]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ s (v ∪ w \ v) = s w

Tactic:
Set.union_sdiff_self,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ s (v ∪ w) = s w
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
a : ℕ
x : α
a✝ : a < k
hx : x ∈ s.restrictNonposSeq i a
⊢ x ∈ i

Tactic:
exact restrictNonposSeq_subset _ hx

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
hn : ¬∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

Tactic:
by
  classical
  by_cases h : s ≤[i] 0
  · exact ⟨i, hi₁, Set.Subset.refl _, h, hi₂⟩
  push Not at hn
  set k := Nat.find hn
  have hk₂ : s ≤[i \ ⋃ l < k, restrictNonposSeq s i l] 0 := Nat.find_spec hn
  have hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), restrictNonposSeq s i l) :=
    MeasurableSet.iUnion fun _ => MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
  refine ⟨i \ ⋃ l < k, restrictNonposSeq s i l, hi₁.diff hmeas, Set.sdiff_subset, hk₂, ?_⟩
  rw [of_sdiff hmeas hi₁, s.of_disjoint_iUnion]
  · have h₁ : ∀ l < k, 0 ≤ s (restrictNonposSeq s i l) := by
      intro l hl
      refine le_of_lt (measure_of_restrictNonposSeq h _ ?_)
      refine mt (restrict_le_zero_subset _ (hi₁.diff ?_) (Set.Subset.refl _)) (Nat.find_min hn hl)
      exact
        MeasurableSet.iUnion fun _ =>
          MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
    suffices 0 ≤ ∑' l : ℕ, s (⋃ _ : l < k, restrictNonposSeq s i l) by
      rw [sub_neg]
      exact lt_of_lt_of_le hi₂ this
    refine tsum_nonneg ?_
    intro l; by_cases h : l < k
    · convert! h₁ _ h
      ext x
      rw [Set.mem_iUnion, exists_prop, and_iff_right_iff_imp]
      exact fun _ => h
    · convert! le_of_eq s.empty.symm
      ext; simp only [exists_prop, Set.mem_empty_iff_false, Set.mem_iUnion, not_and, iff_false]
      exact fun h' => False.elim (h h')
  · intro; exact MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
  · intro a b hab
    refine Set.disjoint_iUnion_left.mpr fun _ => ?_
    refine Set.disjoint_iUnion_right.mpr fun _ => ?_
    exact restrictNonposSeq_disjoint hab
  · apply Set.iUnion_subset
    intro a x
    simp only [and_imp, exists_prop, Set.mem_iUnion]
    intro _ hx
    exact restrictNonposSeq_subset _ hx

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ S = 0
⊢ s S = 0

Tactic:
rw [← VectorMeasure.ennrealToMeasure_apply hS₁] at hS₂

Goal state after:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
⊢ s S = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case a
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ s ≤[B] 0} ∧ s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ (fun x ↦ s A) n ≤ f n

Tactic:
← (hB n).2,

Goal state after:
case a
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ s ≤[B] 0} ∧ s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ (fun x ↦ s A) n ≤ s (B n)
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
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensityᵥ 0) s = 0 s

Tactic:
rw [withDensityᵥ_apply (integrable_zero α E μ) hs]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, 0 x ∂μ = 0 s
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℚ≥0 E
inst✝ : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ s.card • lpNorm (𝔼 i ∈ s, f i) p μ ≤ ∑ i ∈ s, (fun i ↦ lpNorm (f i) p μ) i

Tactic:
← lpNorm_nsmul,

Goal state after:
case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℚ≥0 E
inst✝ : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ lpNorm (s.card • 𝔼 i ∈ s, f i) p μ ≤ ∑ i ∈ s, (fun i ↦ lpNorm (f i) p μ) i