mathlib-initiative/mathlib-tactics huggingface dataset:
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
h : IsSymmetricAlgebra f
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r)
ι : ∀ (x : M), motive (f x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
⊢ motive a

Tactic:
rw [← h.equiv.right_inv a]

Goal state after:
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
h : IsSymmetricAlgebra f
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r)
ι : ∀ (x : M), motive (f x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
⊢ motive (h.equiv.toFun (h.equiv.invFun a))
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case trans
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • x✝) (r • z✝)

Tactic:
apply AddCon.trans <;> assumption

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Matrix

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst✝¹⁴ : DecidableEq ι
inst✝¹³ : DecidableEq κ
inst✝¹² : Fintype ι
inst✝¹¹ : Fintype κ
inst✝¹⁰ : Finite ι'
inst✝⁹ : Finite κ'
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ (toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN')) (map f g) (i, j) (i', j') =
    kroneckerMap (fun x1 x2 ↦ x1 * x2) ((toMatrix bM bM') f) ((toMatrix bN bN') g) (i, j) (i', j')

Tactic:
Matrix.kroneckerMap_apply,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst✝¹⁴ : DecidableEq ι
inst✝¹³ : DecidableEq κ
inst✝¹² : Fintype ι
inst✝¹¹ : Fintype κ
inst✝¹⁰ : Finite ι'
inst✝⁹ : Finite κ'
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ (toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN')) (map f g) (i, j) (i', j') =
    (toMatrix bM bM') f i i' * (toMatrix bN bN') g j j'
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s : Multiset α
⊢ (∃ t a, (∀ a' ∈ t, r a' a) ∧ s' + {a} = s + t) ↔ ∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t

Tactic:
add_singleton_eq_iff

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s : Multiset α
⊢ (∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a) ↔
    ∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
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
he : e ∈ dilatransvections K V
⊢ ?m.70 + finrank K V ≤ ?m.70 + (finrank K ↥(↑e - LinearMap.id).ker + 1)

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
he : e ∈ dilatransvections K V
⊢ ℕ

Tactic:
← add_assoc,

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
he : e ∈ dilatransvections K V
⊢ ?a + finrank K V ≤ ?a + finrank K ↥(↑e - LinearMap.id).ker + 1

case a
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
he : e ∈ dilatransvections K V
⊢ ℕ
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case inl.refine_1
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ {a} + (s₁.erase a + t) = s₁ + t

Tactic:
← add_assoc,

Goal state after:
case inl.refine_1
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ {a} + s₁.erase a + t = s₁ + t
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case neg
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S.Nonempty
⊢ ⋂ i ∈ S, s i ∈ 𝒜

Tactic:
· exact h𝒜.isSetRing.biInter_mem S h hs

Goal state after:
Module: Mathlib.MeasureTheory.SetAlgebra

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

Tactic:
intro s hs
  induction hs with
  | base t t_mem => exact self_subset_generateSetAlgebra (h t_mem)
  | empty => exact isSetAlgebra_generateSetAlgebra.empty_mem
  | compl t _ t_mem => exact isSetAlgebra_generateSetAlgebra.compl_mem t_mem
  | union t u _ _ t_mem u_mem => exact isSetAlgebra_generateSetAlgebra.union_mem t_mem u_mem

Goal state after:
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case compl.refine_1
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
f : (a : ↑A) → ↑↑a
a : ↑A
⊢ (↑(f a))ᶜ ∈ 𝒜 ∨ ↑(f a) ∈ 𝒜

Tactic:
or_comm

Goal state after:
case compl.refine_1
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
f : (a : ↑A) → ↑↑a
a : ↑A
⊢ ↑(f a) ∈ 𝒜 ∨ (↑(f a))ᶜ ∈ 𝒜
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.top.inr
ι : 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 : ι
hb : ⊤ ∈ Ioi ↑a
ha : (Ioi a).Nonempty
⊢ ∃ t ⊆ Ioi ↑a, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ ⊤ ∈ t

Tactic:
· obtain ⟨b, bc', hb⟩ : ∃ b ∈ c', b ∈ Ioi a := hc'.exists_mem_open (isOpen_Ioi' a) ha
          refine ⟨Ioi b, ?_, ?_, by simp⟩
          · apply Ioi_subset_Ioi
            simpa using hb.le
          · apply isOpen_generateFrom_of_mem
            exact ⟨b, by simp [d, bc'], Or.inl rfl⟩

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

Goal state before:
pp: α : 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
⊢ m (s ∪ t) = m s + m t

Tactic:
by
  have A : s ∪ t = ⋃ i, ![s, t] i := by ext; simp
  convert! addContent_iUnion (f := ![s, t]) (m := m) (fun i ↦ ?_) (fun i j hij ↦ ?_) ?_ using 2
  · simp [Fin.univ_castSuccEmb, add_comm]
  · fin_cases i <;> simpa
  · #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed all four
    cases. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
    the new canonicalizer; a minimization would help. The original proof was:
    `fin_cases i <;> fin_cases j <;> grind` -/
    fin_cases i <;> fin_cases j
    · grind
    · assumption
    · exact h_dis.symm
    · grind
  · rwa [← A]

Goal state after:
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.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 : WithTop ι
hb : b ∈ Ioi ↑a
⊢ ∃ t ⊆ Ioi ↑a, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ b ∈ t

Tactic:
induction b with
      | top =>
        -- if `b = ⊤`, then either `Ioi a` is empty in `ι` and then we use `Ioi (↑x₁)` which is
        -- in our set and reduced to `⊤`
        rcases eq_empty_or_nonempty (Ioi a) with ha | ha
        · refine ⟨Ioi x₁, ?_, ?_, by simp⟩
          · have : Ioi x₁ = ∅ := by
              have h : ∃ x, Ioi x = ∅ := ⟨a, ha⟩
              simp only [x₁, h, ↓reduceDIte]
              exact h.choose_spec
            simp [WithTop.Ioi_coe, this]
          · apply isOpen_generateFrom_of_mem
            simp [d]
        -- If `Ioi a` is not empty in `ι`, it contains a point `b` in the dense set `c'`, and then
        -- we use `Ioi (↑b)` which is in our set, contained in `Ioi (↑a)` and contains `⊤`.
        · obtain ⟨b, bc', hb⟩ : ∃ b ∈ c', b ∈ Ioi a := hc'.exists_mem_open (isOpen_Ioi' a) ha
          refine ⟨Ioi b, ?_, ?_, by simp⟩
          · apply Ioi_subset_Ioi
            simpa using hb.le
          · apply isOpen_generateFrom_of_mem
            exact ⟨b, by simp [d, bc'], Or.inl rfl⟩
      | coe b =>
        -- if `b` comes from `ι`, then in `ι` we can find a finite intersection of our sets
        -- containing `b` and contained in `Ioi a`. We lift it to `WithTop ι`.
        simp only [mem_Ioi, WithTop.coe_lt_coe] at hb
        obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Ioi a := h_basis.isOpen_iff.1 (isOpen_Ioi' a) b hb
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ ⋂ z ∈ g, Iio z, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp
          | coe w =>
            simp only [mem_Ioi, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind

Goal state after:
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.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 : ι
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi ↑a)

Tactic:
| coe a =>

Goal state after:
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inr.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 : ι
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ↑a)

Tactic:
| coe a =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
⊢ UnifIntegrable (-f) p μ

Tactic:
by
  simp_rw [UnifIntegrable, Pi.neg_apply, Set.indicator_neg', eLpNorm_neg]
  exact hf

Goal state after:
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

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

Tactic:
exact blimsup_cthickening_ae_le_of_eventually_mul_le μ p hM hr
        (Eventually.of_forall fun i => le_refl _)

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

Goal state before:
pp: case h₁
α : 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 ∂μ ≤ ENNReal.ofReal (ε ^ p.toReal)

Tactic:
convert! hM using 3 with x

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 f x‖ₑ ^ p.toReal =
    ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ s.restrictNonposSeq i n.succ = s.someExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)

Tactic:
restrictNonposSeq

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ s.someExistsOneDivLT
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n),
            have this := ⋯;
            s.restrictNonposSeq i k) =
    s.someExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.restrictNonposSeq i 0 ⊆ i

Tactic:
restrictNonposSeq

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.someExistsOneDivLT (i \ ∅) ⊆ i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ s.restrictNonposSeq i (n✝ + 1) ⊆ i

Tactic:
restrictNonposSeq

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ s.someExistsOneDivLT
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n✝),
            have this := ⋯;
            s.restrictNonposSeq i k) ⊆
    i
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.restrictNonposSeq i 0)

Tactic:
restrictNonposSeq

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.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
⊢ restrict 0 i = 0

Tactic:
by_cases hi : MeasurableSet i
  · ext j hj
    rw [restrict_apply 0 hi hj, zero_apply, zero_apply]
  · exact dif_neg hi

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

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

Tactic:
cases n with

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.restrictNonposSeq i 0)

Tactic:
restrictNonposSeq

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.someExistsOneDivLT (i \ ∅))
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasurableSet (s.restrictNonposSeq i (n✝ + 1))

Tactic:
restrictNonposSeq

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasurableSet
    (s.someExistsOneDivLT
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n✝),
            have this := ⋯;
            s.restrictNonposSeq i k))
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
n✝ : ℕ
h : n < n✝ + 1
hx₂ : x ∈ s.restrictNonposSeq i (n✝ + 1)
⊢ False

Tactic:
restrictNonposSeq

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
n✝ : ℕ
h : n < n✝ + 1
hx₂ :
  x ∈
    s.someExistsOneDivLT
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n✝),
            have this := ⋯;
            s.restrictNonposSeq i k)
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid M
inst✝¹ : T2Space M
inst✝ : ContinuousAdd M
v : VectorMeasure α M
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ v.restrict (s ∩ t) + (v.restrict t + v.restrict (s \ t)) = v.restrict (s ∩ t) + v.restrict (s \ t) + v.restrict t

Tactic:
← add_assoc,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid M
inst✝¹ : T2Space M
inst✝ : ContinuousAdd M
v : VectorMeasure α M
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ v.restrict (s ∩ t) + v.restrict t + v.restrict (s \ t) = v.restrict (s ∩ t) + v.restrict (s \ t) + v.restrict t
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
i : Set α
hi : MeasurableSet i
⊢ (-j).posPart.real i - (-j).negPart.real i = -(j.posPart.real i - j.negPart.real i)

Tactic:
neg_sub,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
i : Set α
hi : MeasurableSet i
⊢ (-j).posPart.real i - (-j).negPart.real i = j.negPart.real i - j.posPart.real i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : 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
⊢ v j ≤ w j

Tactic:
by_cases hj₁ : MeasurableSet j
  · exact (restrict_le_restrict_iff _ _ hi).1 hi₂ hj₁ hj
  · rw [v.not_measurable hj₁, w.not_measurable hj₁]

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

Tactic:
have hn' : ∀ n : ℕ, ¬s ≤[i \ ⋃ l ≤ n, restrictNonposSeq s i l] 0 := by
    intro n
    convert! hn (n + 1) using 5 <;>
      · ext l
        simp only [exists_prop, Set.mem_iUnion, and_congr_left_iff]
        exact fun _ => Nat.lt_succ_iff.symm

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
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0
t : Set α
hst : t ⊆ s
ht : ¬MeasurableSet t
⊢ v t = 0

Tactic:
exact not_measurable v ht

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

Goal state before:
pp: case mp.left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
⊢ s.toJordanDecomposition.posPart S = 0

Tactic:
have := h hS₂

Goal state after:
case mp.left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.totalVariation S = 0
⊢ s.toJordanDecomposition.posPart S = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
⊢ s.toJordanDecomposition.negPart S = 0

Tactic:
have := h hS₂

Goal state after:
case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.totalVariation S = 0
⊢ s.toJordanDecomposition.negPart S = 0