mathlib-initiative/mathlib-tactics huggingface dataset:
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) * (3 * (B.form (shortRoot P)) (shortRoot P)) =
    (P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (shortAddLongRoot P)) (shortAddLongRoot P)

Tactic:
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.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
n : ℕ
hn : e i ^ n = 0
⊢ ω b * f i ^ n = e i ^ n * ω b

Tactic:
clear hn

Goal state after:
ι : 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
n : ℕ
⊢ ω b * f i ^ n = e i ^ n * ω b
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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
this : ∃ d, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d) ∧ diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
⊢ (w (Sum.inr i))⁻¹ • w = v b i

Tactic:
obtain ⟨d, hd₀, hd₁, hd₂⟩ := this

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.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
⊢ (w (Sum.inr i))⁻¹ • w = v b i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case h₀
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i✝ : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
i : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hi : v b i ∈ ωConjLieSubmodule U
⊢ ∃ j, u j ∈ U

Tactic:
obtain ⟨j, hj⟩ := h hi

Goal state after:
case h₀
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i✝ : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
i : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hi : v b i ∈ ωConjLieSubmodule U
j : ↥b.support
hj : u j ∈ ωConjLieSubmodule U
⊢ ∃ j, u j ∈ U
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this✝ : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
this :
  (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)

Tactic:
have h₁ : ∀ x ∈ Finset.univ, ¬ ((x = i ∧ l = -i) ∧ k = -j) := by
        rintro - - ⟨⟨-, contra⟩, -⟩; contradiction

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this✝ : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
this :
  (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
h₁ : ∀ x ∈ Finset.univ, ¬((x = i ∧ l = -↑i) ∧ k = -↑j)
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
he : count a (s + {a}) = count a (t + u)
⊢ count a s < count a t

Tactic:
simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)),
      add_zero] at he

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
he : count a s + 1 = count a t
⊢ count a s < count 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 f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(e * f)).fixedSubmodule

Tactic:
have := finrank_fixedSubmodule_add_le e f
  have := finrank_le_one_add_finrank_fixedSubmodule_dilatransvection f hf
  have : finrank K ↥(e.fixedSubmodule ⊔ f.fixedSubmodule) ≤ finrank K V :=
    finrank_le _
  linarith

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 : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
x : V
hx : x ∈ (↑e).fixedSubmodule
⊢ x ∈ (↑(transvection hfv)).fixedSubmodule

Tactic:
rw [mem_fixedSubmodule_transvection_iff, smul_eq_zero]

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 : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
x : V
hx : x ∈ (↑e).fixedSubmodule
⊢ f x = 0 ∨ v - e v = 0
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ f ∈ (↑s₂).pi t₂'
⊢ (t₁' i ∩ t₂' i).Nonempty

Tactic:
mem_pi

Goal state after:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
⊢ (t₁' i ∩ t₂' i).Nonempty
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
t : Set α
ht : t ∈ ↑(hC.disjointOfDiffUnion hs hI)
⊢ t ⊆ s \ ⋃₀ ↑I

Tactic:
revert t ht

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ∀ t ∈ ↑(hC.disjointOfDiffUnion hs hI), t ⊆ s \ ⋃₀ ↑I
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
hj : j ∈ J
⊢ (↑(hC.disjointOfUnion hJ j)).PairwiseDisjoint id

Tactic:
by
  lift j to J using hj
  rw [disjointOfUnion_coe, ← supIndep_iff_pairwiseDisjoint]
  exact Finpartition.supIndep _

Goal state after:
Module: Mathlib.MeasureTheory.SetAlgebra

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

Tactic:
intro s

Goal state after:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
⊢ s ∈ generateSetAlgebra 𝒜 → s ∈ generateSetAlgebra ℬ
Module: Mathlib.MeasureTheory.SetAlgebra

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

Tactic:
intro s

Goal state after:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
⊢ s ∈ generateSetAlgebra 𝒜 → s ∈ ℬ
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ∑ u ∈ I ∪ hC.disjointOfDiffUnion hs hI, m u = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i

pp: case h_ss
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ⊆ C

pp: case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

pp: case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C

Tactic:
· rw [sum_union]
    exact hC.disjoint_disjointOfDiffUnion hs hI

Goal state after:
case h_ss
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ⊆ C

case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C
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

Tactic:
← hC.sUnion_insert_disjointOfDiff ht hs hst

Goal state after:
α : 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 (⋃₀ insert s ↑(hC.disjointOfDiff ht hs))
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 𝒜 ⊆ f '' 𝒟

Tactic:
intro s

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
s : Set α
⊢ s ∈ generateSetAlgebra 𝒜 → s ∈ f '' 𝒟
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 ℕ
⊢ (f '' ↑I).PairwiseDisjoint id

Tactic:
intro s

Goal state after:
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 ℕ
s : Set α
⊢ s ∈ f '' ↑I → ∀ ⦃y : Set α⦄, y ∈ f '' ↑I → s ≠ y → (Disjoint on id) s y
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
⊢ ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u

Tactic:
intro I

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
I : Finset (Set α)
⊢ ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
    (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u : α
huv : u ≤ u
h'uv : ⋃₀ ↑I = Set.Ioc u u
this : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0
i : Set α
hi : i ∈ I
⊢ 0 = onIocAux f i

Tactic:
have : i = ∅ := by grind [sUnion_eq_empty]

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u : α
huv : u ≤ u
h'uv : ⋃₀ ↑I = Set.Ioc u u
this✝ : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0
i : Set α
hi : i ∈ I
this : i = ∅
⊢ 0 = onIocAux f i
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 α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := ⋯
Y₂ : ℕ → Set α := ⋯
Z : ℕ → Set α := ⋯
i : ℕ
W : Set α := ⋯
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type} {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₁ : ∀ (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)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := ⋯
hC : C ≠ 0
b : ℕ → Set α := ⋯
B : ℕ → Set α := ⋯
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
⊢ ∀ᶠ (x : ℕ) in atTop, M * r₁ (f x) ≤ r₂ (f x) → Disjoint (b x) (W ∩ B x)

Tactic:
rw [eventually_atTop]

Goal state after:
α : 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₂ : ℕ → ℝ
hrp : 0 ≤ 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} {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₁ : ∀ (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)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun j ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun j ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
⊢ ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → M * r₁ (f b_1) ≤ r₂ (f b_1) → Disjoint (b b_1) (W ∩ B b_1)
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
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
⊢ ∀ (s : Set Ω) (c : F) (f : Ω → E),
    (fun ω ↦ (B (s.indicator (Function.const Ω c) ω)) (f ω)) = s.indicator fun ω ↦ (B c) (f ω)

Tactic:
intro s

Goal state after:
Ω : 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Ω
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
⊢ ∀ (c : F) (f : Ω → E), (fun ω ↦ (B (s.indicator (Function.const Ω c) ω)) (f ω)) = s.indicator fun ω ↦ (B c) (f ω)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
hmsn : ∀ (n : ℕ), m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)
h_tendsto : Tendsto (fun n ↦ m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 0)
n : ℕ
⊢ m (accumulate f n) ≤ m (⋃ i, f i)

Tactic:
exact addContent_mono hC.isSetSemiring (hC.accumulate_mem hf n) hUf
    (Set.accumulate_subset_iUnion _)

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
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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ ⋃ i, (partialSups f) i ∈ C

Tactic:
rwa [← iSup_eq_iUnion, iSup_partialSups_eq]

Goal state after: