mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case of.perm.right
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ (addConGen (Rel R ι M)) (r • (PiTensorProduct.tprod R) fun i ↦ f i) (r • (PiTensorProduct.tprod R) fun i ↦ f (e i))

Tactic:
convert!
          AddConGen.Rel.of _ _ <|
            SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)

Goal state after:
case e'_1
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f i) = (PiTensorProduct.tprod R) fun i_1 ↦ Function.update f i (r • f i) i_1

case e'_2
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f (e i)) =
    (PiTensorProduct.tprod R) fun i_1 ↦ Function.update f i (r • f i) (e i_1)
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case e'_1
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f i) = r • (PiTensorProduct.tprod R) (Function.update f i (f i))

Tactic:
Function.update_eq_self

Goal state after:
case e'_1
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f i) = r • (PiTensorProduct.tprod R) f
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case e'_2
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f (e i)) =
    (PiTensorProduct.tprod R) fun i_1 ↦ Function.update f i (r • f i) (e i_1)

Tactic:
[

Goal state after:
case e'_2
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f (e i)) =
    (PiTensorProduct.tprod R) fun i_1 ↦ Function.update f i (r • f i) (e i_1)
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case e'_2
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f (e i)) = r • (PiTensorProduct.tprod R) (Function.update f i (f i) ∘ ⇑e)

Tactic:
Function.update_eq_self

Goal state after:
case e'_2
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f (e i)) = r • (PiTensorProduct.tprod R) (f ∘ ⇑e)
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:
[

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') =
    kroneckerMap (fun x1 x2 ↦ x1 * x2) ((toMatrix bM bM') f) ((toMatrix bN bN') g) (i, j) (i', j')
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 : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
b : α
h : (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) b a
⊢ (toFinsupp s) b = (toFinsupp t) b

Tactic:
[

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
b : α
h : (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) b a
⊢ (toFinsupp s) b = (toFinsupp t) b
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 : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
⊢ (toFinsupp s) a < (toFinsupp t) a

Tactic:
[

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

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

Tactic:
[

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s : Multiset α
⊢ CutExpand r s' s ↔ ∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ ∅ ∈ closedCompactCylinders X

Tactic:
[

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ ∅ ∈ closedCompactCylinders X
Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
⊢ t ∈ closedCompactCylinders X ↔ ∃ s S, IsClosed S ∧ IsCompact S ∧ t = cylinder s S

Tactic:
[

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
⊢ t ∈ closedCompactCylinders X ↔ ∃ s S, IsClosed S ∧ IsCompact S ∧ t = cylinder s S
Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
⊢ t ∈ closedCompactCylinders X ↔ ∃ s S, IsClosed S ∧ IsCompact S ∧ t = cylinder s S

Tactic:
by
  simp_rw [closedCompactCylinders, mem_iUnion, mem_singleton_iff, exists_prop]

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

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ hJI ⁻¹' T
⊢ (P I) S = (P I) (Finset.restrict₂ hJI ⁻¹' T)

pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ hJI ⁻¹' T
⊢ Measurable (Finset.restrict₂ hJI)

Tactic:
this

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ hJI ⁻¹' T
⊢ (P I) (Finset.restrict₂ hJI ⁻¹' T) = (P I) (Finset.restrict₂ hJI ⁻¹' T)

ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ hJI ⁻¹' T
⊢ Measurable (Finset.restrict₂ hJI)
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
a✝ : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ ⋃ i_1 ∈ insert i S, s i_1 ∈ C

Tactic:
[

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
a✝ : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ ⋃ i_1 ∈ insert i S, s i_1 ∈ C
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case cons
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S✝ : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs✝ : S.Nonempty
h : (∀ n ∈ S, s n ∈ C) → ⋂ i ∈ S, s i ∈ C
hs : ∀ n ∈ cons i S hiS, s n ∈ C
⊢ ⋂ i_1 ∈ cons i S hiS, s i_1 ∈ C

Tactic:
[

Goal state after:
case cons
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S✝ : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs✝ : S.Nonempty
h : (∀ n ∈ S, s n ∈ C) → ⋂ i ∈ S, s i ∈ C
hs : ∀ n ∈ cons i S hiS, s n ∈ C
⊢ ⋂ i_1 ∈ cons i S hiS, s i_1 ∈ C
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : Nonempty ((i : ι) → α i)
s t : Finset ι
S : Set ((i : ↥s) → α ↑i)
T : Set ((i : ↥t) → α ↑i)
inst✝ : DecidableEq ι
⊢ Disjoint (cylinder s S) (cylinder t T) ↔ Disjoint (Finset.restrict₂ ⋯ ⁻¹' S) (Finset.restrict₂ ⋯ ⁻¹' T)

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Nonempty ((i : ι) → α i)
s t : Finset ι
S : Set ((i : ↥s) → α ↑i)
T : Set ((i : ↥t) → α ↑i)
inst✝ : DecidableEq ι
⊢ Disjoint (cylinder s S) (cylinder t T) ↔ Disjoint (Finset.restrict₂ ⋯ ⁻¹' S) (Finset.restrict₂ ⋯ ⁻¹' T)
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ ∅ ∈ measurableCylinders α

Tactic:
[

Goal state after:
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ ∅ ∈ measurableCylinders α
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
⊢ t ∈ measurableCylinders α ↔ ∃ s S, MeasurableSet S ∧ t = cylinder s S

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
⊢ t ∈ measurableCylinders α ↔ ∃ s S, MeasurableSet S ∧ t = cylinder s S
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
hs : s ≠ ⊥
⊢ ∀ t ∈ (P.avoid s).parts, ∃ Q, ↑Q.parts ⊆ C

Tactic:
[

Goal state after:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
hs : s ≠ ⊥
⊢ ∀ t ∈ (P.avoid s).parts, ∃ Q, ↑Q.parts ⊆ C
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
a✝ : t ∉ T
ih : ∀ ⦃s : Set α⦄, s ∈ supClosure C → ↑T ⊆ C → s \ T.sup id ∈ supClosure C
s : Set α
hs : s ∈ supClosure C
hTC : ↑(insert t T) ⊆ C
⊢ s \ (insert t T).sup id ∈ supClosure C

Tactic:
[

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
a✝ : t ∉ T
ih : ∀ ⦃s : Set α⦄, s ∈ supClosure C → ↑T ⊆ C → s \ T.sup id ∈ supClosure C
s : Set α
hs : s ∈ supClosure C
hTC : ↑(insert t T) ⊆ C
⊢ s \ (insert t T).sup id ∈ supClosure C
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
⊢ Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable fun a ↦ g a i

Tactic:
[

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
⊢ Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable fun a ↦ g a i
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ t ∉ hC.disjointOfDiff hs ht

Tactic:
intro hs_mem
  cases disjoint_sdiff_self_right.eq_bot_of_le (Finpartition.le _ hs_mem)
  exact hC.empty_notMem_disjointOfDiff hs ht hs_mem

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ Disjoint (id t) (id u)

Tactic:
[

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ Disjoint (id t) (id u)
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
inst✝ : Unique ι
⊢ Measurable uniqueElim

Tactic:
[

Goal state after:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
inst✝ : Unique ι
⊢ Measurable uniqueElim
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
h_dis : (↑I).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑I
v : Set α
hv : v ∈ ↑(hC.disjointOfDiffUnion hs hI)
x✝ : u ≠ v
⊢ Disjoint (id u) (id v)

Tactic:
[

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑I
v : Set α
hv : v ∈ ↑(hC.disjointOfDiffUnion hs hI)
x✝ : u ≠ v
⊢ Disjoint (id u) (id v)
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
hI_ss : ∀ t ∈ I, t ⊆ s
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)

Tactic:
[

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
j k : ↑↑J
hjk : j ≠ k
⊢ Function.onFun Disjoint (hC.disjointOfUnion hJ) ↑j ↑k

Tactic:
[

Goal state after:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
j k : ↑↑J
hjk : j ≠ k
⊢ Function.onFun Disjoint (hC.disjointOfUnion hJ) ↑j ↑k
Module: Mathlib.MeasureTheory.SetSemiring

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

Tactic:
[

Goal state after:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ (⋃ x ∈ J, ↑(hC.disjointOfUnion hJ x)).PairwiseDisjoint id
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 ↦ Function.onFun Disjoint (fun i' ↦ ⨆ i ∈ ↑(hC.disjointOfUnion hJ i'), id i) ↑x ↑y

Tactic:
[

Goal state after:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ Pairwise fun x y ↦ Function.onFun Disjoint (fun i' ↦ ⨆ i ∈ ↑(hC.disjointOfUnion hJ i'), id i) ↑x ↑y
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : 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₁}
H : instWithTopOfOrderTopology = generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
d_count : d.Countable
this : {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d
⊢ {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}.Countable

Tactic:
this

Goal state after:
ι : 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₁}
H : instWithTopOfOrderTopology = generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
d_count : d.Countable
this : {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d
⊢ (Ioi '' d ∪ Iio '' d).Countable
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ ⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion hJ x) = ⋃₀ ↑J

Tactic:
[

Goal state after:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ ⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion hJ x) = ⋃₀ ↑J
Module: Mathlib.MeasureTheory.Measure.AddContent

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

Tactic:
fin_cases j

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

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

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

Tactic:
fin_cases j

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

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

Goal state before:
pp: case union.refine_1.inl
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Au
⊢ a.Finite

Tactic:
exact mem_Au a ha

Goal state after:
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
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
s : Set α
hs : s ∈ J
⊢ s = ⋃ t ∈ J', s ∩ t

Tactic:
[

Goal state after:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
s : Set α
hs : s ∈ J
⊢ s = ⋃ t ∈ J', s ∩ t
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
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
⊢ m s = ∑ t ∈ J', m (s ∩ t)

Tactic:
this

Goal state after:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
⊢ m (⋃ t ∈ J', s ∩ t) = ∑ t ∈ J', m (s ∩ t)
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
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
⊢ t = ⋃ s ∈ J, s ∩ t

Tactic:
[

Goal state after:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
⊢ t = ⋃ s ∈ J, s ∩ t
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
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ ∑ s ∈ J, m (s ∩ t) = m t

Tactic:
this

Goal state after:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ ∑ s ∈ J, m (s ∩ t) = m (⋃ s ∈ J, s ∩ t)