mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := ⋯
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
x : ℕ
hk₂ : (e i ^ 0).col (Sum.inr j) = x • Pi.single (Sum.inr (-↑i)) 1
hk₁ : P.root (-j) = (0 + 1) • P.root ↑i
⊢ j = -↑i

Tactic:
zero_add,

Goal state after:
case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
x : ℕ
hk₂ : (e i ^ 0).col (Sum.inr j) = x • Pi.single (Sum.inr (-↑i)) 1
hk₁ : P.root (-j) = 1 • P.root ↑i
⊢ j = -↑i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
⊢ P.root k ≠ 2 • P.root ↑i

Tactic:
exact fun contra ↦ P.nsmul_notMem_range_root (n := 2) (i := i) ⟨k, contra⟩

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

Goal state before:
pp: case inr.inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
k l : ι
hkl : k ≠ l
⊢ (if P.root k = P.root ↑i + P.root l then
      ↑(P.pairingIn ℤ k ↑j) * (↑(chainBotCoeff (↑i) l) + 1) - (↑(chainBotCoeff (↑i) l) + 1) * ↑(P.pairingIn ℤ l ↑j)
    else 0) =
    if P.root k = P.root ↑i + P.root l then ↑(P.pairingIn ℤ ↑i ↑j) * ↑(chainBotCoeff (↑i) l) + ↑(P.pairingIn ℤ ↑i ↑j)
    else 0

Tactic:
refine ite_congr rfl (fun hkil ↦ ?_) (fun _ ↦ rfl)

Goal state after:
case inr.inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
k l : ι
hkl : k ≠ l
hkil : P.root k = P.root ↑i + P.root l
⊢ ↑(P.pairingIn ℤ k ↑j) * (↑(chainBotCoeff (↑i) l) + 1) - (↑(chainBotCoeff (↑i) l) + 1) * ↑(P.pairingIn ℤ l ↑j) =
    ↑(P.pairingIn ℤ ↑i ↑j) * ↑(chainBotCoeff (↑i) l) + ↑(P.pairingIn ℤ ↑i ↑j)
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.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
this : ⨆ χ, ⨆ (_ : χ ≠ 0), ⊥ = ⊥
⊢ genWeightSpace (↥U) 0 = ⊤

Tactic:
rw [← iSup_genWeightSpace_eq_top K H U, iSup_split_single _ 0, biSup_congr hU, this, sup_bot_eq]

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
this :
  LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀) =
    LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ range e₀ ∪ range f₀)
⊢ LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀) = ⊤

Tactic:
have hr : range h₀ ∪ range e₀ ∪ range f₀ = Subtype.val ⁻¹' (range h ∪ range e ∪ range f) := by
        aesop

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
this :
  LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀) =
    LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ range e₀ ∪ range f₀)
hr : range h₀ ∪ range e₀ ∪ range f₀ = Subtype.val ⁻¹' (range h ∪ range e ∪ range f)
⊢ LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀) = ⊤
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
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
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✝² : InvolutiveNeg ι := P.indexNeg
this✝¹ : P.IsNotG2
this✝ : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
this : P.pairing l j = P.pairing i j + P.pairing k j
⊢ (algebraMap ℤ R) (P.pairingIn ℤ l j) = (algebraMap ℤ R) (P.pairingIn ℤ i j + P.pairingIn ℤ k j)

Tactic:
by simpa only [algebraMap_pairingIn, map_add]

Goal state after:
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: case add
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
a✝ b✝ : SymmetricAlgebra R M
hx : motive ((SymmetricAlgebra.lift f) a✝)
hy : motive ((SymmetricAlgebra.lift f) b✝)
⊢ motive ((SymmetricAlgebra.lift f) (a✝ + b✝))

Tactic:
simpa using add _ _ hx hy

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
W : Submodule K V
v : V
hv : v ∉ W
h1 : finrank K (V ⧸ W ⊔ K ∙ v) + finrank K ↥(W ⊔ K ∙ v) = finrank K V
⊢ finrank K (V ⧸ W ⊔ K ∙ v) + 1 = finrank K (V ⧸ W)

Tactic:
have h2 := finrank_quotient_add_finrank W

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
W : Submodule K V
v : V
hv : v ∉ W
h1 : finrank K (V ⧸ W ⊔ K ∙ v) + finrank K ↥(W ⊔ K ∙ v) = finrank K V
h2 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
⊢ finrank K (V ⧸ W ⊔ K ∙ v) + 1 = finrank K (V ⧸ W)
Module: Mathlib.MeasureTheory.Constructions.Projective

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

Tactic:
by
  rw [← cylinder_univ I, hμ.measure_cylinder _ MeasurableSet.univ]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders α
⊢ μ (cylinder I S) = ν (cylinder I S)

Tactic:
rw [hμ.measure_cylinder _ hS, hν.measure_cylinder _ hS]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
⊢ μ = ν

Tactic:
by
  have : IsFiniteMeasure μ := hμ.isFiniteMeasure
  refine ext_of_generate_finite (measurableCylinders α) generateFrom_measurableCylinders.symm
    isPiSystem_measurableCylinders (fun s hs ↦ ?_) (hμ.measure_univ_unique hν)
  obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders _).mp hs
  rw [hμ.measure_cylinder _ hS, hν.measure_cylinder _ hS]

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
e : V ≃ₗ[K] V
u y : V
hy : y ∈ (↑e).fixedSubmodule
a : K
hu' : y + a • (e u - u) = e u
hu : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ u + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ u) = 0 → s = 0 ∧ t = 0
⊢ a • u + e ((1 - a) • u) ∈ (↑e).fixedSubmodule

Tactic:
convert hy

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
u y : V
hy : y ∈ (↑e).fixedSubmodule
a : K
hu' : y + a • (e u - u) = e u
hu : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ u + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ u) = 0 → s = 0 ∧ t = 0
⊢ a • u + e ((1 - a) • u) = y
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
⊢ f' ∈ cylinder s S

Tactic:
rw [mem_cylinder]

Goal state after:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
⊢ s.restrict f' ∈ S
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
hC : IsSetRing C
s : ι → Set α
hs : ∀ (n : ι), s n ∈ C
n : ι
⊢ (partialSups s) n ∈ C

Tactic:
by
  simpa only [partialSups_apply, sup'_eq_sup] using hC.finsetSup_mem (fun i hi ↦ hs i)

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

Goal state before:
pp: case refine_1.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (Finset.restrict₂ ⋯ ⁻¹' S₁)

Tactic:
exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₁

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

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
x : (x : ι) → α x
⊢ x ∈ eval i ⁻¹' t i ↔ x ∈ cylinder {i} {f | f ⟨i, ⋯⟩ ∈ t i}

Tactic:
simp only [mem_preimage, Function.eval, mem_cylinder, mem_ofPred_eq, Finset.restrict]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
X : ι → Type u_3
mα : MeasurableSpace α
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
g : α → (i : ι) → X i
⊢ MeasurableSpace.comap g (cylinderEvents Δ) ≤ mα ↔ ∀ ⦃i : ι⦄, i ∈ Δ → MeasurableSpace.comap (fun a ↦ g a i) (m i) ≤ mα

Tactic:
cylinderEvents,

Goal state after:
α : Type u_1
ι : Type u_2
X : ι → Type u_3
mα : MeasurableSpace α
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
g : α → (i : ι) → X i
⊢ MeasurableSpace.comap g (⨆ i ∈ Δ, MeasurableSpace.comap (fun σ ↦ σ i) (m i)) ≤ mα ↔
    ∀ ⦃i : ι⦄, i ∈ Δ → MeasurableSpace.comap (fun a ↦ g a i) (m i) ≤ mα
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ Pairwise fun x y ↦ Disjoint (⨆ i ∈ ⋯.choose.parts, id i) (⨆ i ∈ ⋯.choose.parts, id i)

Tactic:
← Finset.sup_eq_iSup,

Goal state after:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ Pairwise fun x y ↦ Disjoint (⋯.choose.parts.sup id) (⋯.choose.parts.sup id)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ m (⋃ i ∈ a, f i) = ∑ i ∈ a, m (f i)

Tactic:
A,

Goal state after:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ m (⋃₀ ↑(Finset.image f a)) = ∑ i ∈ a, m (f i)
Module: Mathlib.MeasureTheory.SetAlgebra

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

Tactic:
by_cases! h : S = ∅
  · rw [h, ← Finset.set_biInter_coe, Finset.coe_empty, biInter_empty]
    exact h𝒜.univ_mem
  · exact h𝒜.isSetRing.biInter_mem S h hs

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

Goal state before:
pp: case h_dis
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (↑(insert s (hC.disjointOfDiff ht hs))).PairwiseDisjoint id

Tactic:
rw [coe_insert]
    exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs

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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ m t = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i

Tactic:
conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]
  rw [← coe_insert, addContent_sUnion]
  · rw [sum_insert]
    exact hC.notMem_disjointOfDiff ht hs
  · rw [coe_insert]
    exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)
  · rw [coe_insert]
    exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs
  · rw [coe_insert]
    rwa [hC.sUnion_insert_disjointOfDiff ht hs hst]

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

Goal state before:
pp: case refine_2
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ (↑(Finset.image f I)).PairwiseDisjoint id

pp: case refine_3
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ ∀ s ∈ Finset.image f I, s ⊆ ⋃ i, f i

Tactic:
· simp only [coe_image]
    intro s hs t ht hst
    rw [Set.mem_image] at hs ht
    obtain ⟨i, _, rfl⟩ := hs
    obtain ⟨j, _, rfl⟩ := ht
    have hij : i ≠ j := by intro h_eq; rw [h_eq] at hst; exact hst rfl
    exact hf_disj hij

Goal state after:
case refine_3
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ ∀ s ∈ Finset.image f I, s ⊆ ⋃ i, f i
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
⊢ onIocAux f ∅ = 0

Tactic:
classical
  rw [onIocAux, dite_eq_right_iff]
  grind [Set.Ioc_eq_empty_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case neg.refine_9.hfi
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝¹ : CompleteSpace E
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
this : μ[fun ω ↦ (B (f ω)) (μ[g | m] ω) | m] = fun ω ↦ (B (f ω)) (μ[g | m] ω)
n : ℕ
⊢ Integrable (fun ω ↦ (B ((fs n) ω)) (μ[g | m] ω)) μ

Tactic:
exact B.integrable_of_bilin_of_bdd_left c
      ((fs n).stronglyMeasurable.mono hm).aestronglyMeasurable (ae_of_all _ <| hfs_bound n)
      integrable_condExp

Goal state after:
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
⊢ v ≤ w ↔ ∀ (i : Set α), v i ≤ w i

Tactic:
refine ⟨fun h i => ?_, fun h i _ => h i⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
⊢ v i ≤ w i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ (v.restrict i) j ≤ (w.restrict i) j

Tactic:
exact h j hj₁

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

Goal state before:
pp: case refine_4
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ Summable fun i ↦ w (a ∩ disjointed f i)

Tactic:
· refine (w.m_iUnion (fun n => ?_) ?_).summable
      · exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
      · exact (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : s ≤[v] 0
hs : s (u ∆ v) = 0
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0

Tactic:
rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : s (u ∆ v) = 0
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0
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
hsv : s ≤[v] 0
hs : s (u ∆ v) = 0
⊢ s (w ∩ u) = s (w ∩ v)

Tactic:
rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv

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
hsv : 0 ≤[v] -s
hs : s (u ∆ v) = 0
⊢ s (w ∩ u) = s (w ∩ v)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

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

Tactic:
obtain ⟨⟨f', hf', heq⟩, _⟩ := hf

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

Goal state before:
pp: case refine_2
α : 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₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ (u ∩ v)ᶜ
hmt : MeasurableSet t
⊢ w t = 0

Tactic:
· rw [Set.compl_inter] at ht
    rw [(_ : t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t),
      of_union _ (hmu.compl.inter hmt) ((hmv.compl.diff hmu.compl).inter hmt), hu₂, hv₂, add_zero]
    · exact Set.Subset.trans Set.inter_subset_left sdiff_subset
    · exact Set.inter_subset_left
    · exact disjoint_sdiff_self_right.mono Set.inter_subset_left Set.inter_subset_left
    · apply Set.Subset.antisymm <;> intro x hx
      · by_cases hxu' : x ∈ uᶜ
        · exact Or.inl ⟨hxu', hx⟩
        rcases ht hx with (hxu | hxv)
        exacts [False.elim (hxu' hxu), Or.inr ⟨⟨hxv, hxu'⟩, hx⟩]
      · rcases hx with hx | hx <;> exact hx.2

Goal state after: