mathlib-initiative/mathlib-tactics huggingface dataset:
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
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hv' : v - e v ∈ (↑e).fixedSubmodule
t : V ≃ₗ[K] V := auxTransvection ⋯
ht : t = auxTransvection ⋯
⊢ t⁻¹ * (t * e) = e

Tactic:
by

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
⊢ IsFiniteMeasure μ

Tactic:
by

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 ι), IsProbabilityMeasure (P i)
hμ : IsProjectiveLimit μ P
⊢ IsProbabilityMeasure μ

Tactic:
by

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)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
⊢ μ univ = ν univ

Tactic:
by

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

Goal state after:
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
⊢ IsPiSystem (squareCylinders C)

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
⊢ Set (α j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (eval i) (m i) ≤ generateFrom ((fun t ↦ {i}.pi t) '' univ.pi fun i ↦ {s | MeasurableSet s})

Tactic:
by

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
he : e.fixedReduce = 1
⊢ e ∈ transvections K V ^ (finrank K (V ⧸ (↑e).fixedSubmodule) - 1) * dilatransvections K V

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (squareCylinders fun i ↦ {s | MeasurableSet s}) = MeasurableSpace.pi

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ s ∩ t ∈ C

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
⊢ cylinder s ∅ = ∅

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
⊢ cylinder s univ = univ

Tactic:
by

Goal state after:
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 : S = ∅
⊢ cylinder s S = ∅

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
⊢ ∀ s ∈ C, ∀ t ∈ C, ∃ I, ↑I ⊆ C ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I

Tactic:
by

Goal state after:
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:
by

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 : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
hu' : e u ∈ (↑e).fixedSubmodule ⊔ K ∙ (e u - u)
⊢ False

Tactic:
by

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
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
he : ∀ (v : V ⧸ (↑e).fixedSubmodule), ¬LinearIndependent K ![v, e.fixedReduce v]
a : ↥(Subring.center K)
ha : ↑e.fixedReduce = a • 1
x : V ⧸ (↑e).fixedSubmodule
⊢ e.fixedReduce x = ↑a • x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

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

Tactic:
by

Goal state after:
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)
⊢ cylinder s S = ∅ ↔ S = ∅

Tactic:
by

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
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
⊢ ∃ v, LinearIndependent K ![v, e.fixedReduce v]

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
⊢ (cylinder s S)ᶜ = cylinder s Sᶜ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
S T : Set ((i : ↥s) → α ↑i)
⊢ cylinder s S \ cylinder s T = cylinder s (S \ T)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hS : S.Nonempty
hs : ∀ n ∈ S, s n ∈ C
⊢ ⋂ i ∈ S, s i ∈ C

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
ι : Type u_2
s : ι → Set α
t : Finset ι
hs : ∀ i ∈ t, s i ∈ C
⊢ t.sup s ∈ C

Tactic:
by

Goal state after:
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

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
⊢ S = Finset.restrict₂ hJI ⁻¹' T

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
⊢ ⋃ i, ⋃ (_ : i ≤ n), s i ∈ C

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
J : Finset ι
⊢ cylinder I S = cylinder (I ∪ J) (Finset.restrict₂ ⋯ ⁻¹' S)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
⊢ ⋂ i, ⋂ (_ : i ≤ n), s i ∈ C

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
⊢ accumulate s n ∈ C

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
M : Type u_1
inst✝ : Zero M
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
c : M
x y : (i : ι) → α i
hxy : ∀ i ∈ ↑I, x i = y i
⊢ x ∈ cylinder I S ↔ y ∈ cylinder I S

Tactic:
by

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
⊢ ∃ P, ↑P.parts ⊆ C

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
hS : MeasurableSet S
⊢ cylinder s S ∈ measurableCylinders α

Tactic:
by

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
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
f : Dual K V
hfu : f (e u) ≠ 0
hf : map f ((↑e).fixedSubmodule ⊔ K ∙ (e u - u)) = ⊥
⊢ f u ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
⊢ s ∈ supClosure C → ∃ P, ↑P.parts ⊆ C

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ s ∩ t ∈ measurableCylinders α

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
⊢ (∃ P, ↑P.parts ⊆ C) → s ∈ supClosure C

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
f : Dual K V
hf : map f ((↑e).fixedSubmodule ⊔ K ∙ (e u - u)) = ⊥
hfu : f u ≠ 0
v : V := (f u)⁻¹ • u
v_def : v = (f u)⁻¹ • u
⊢ K ∙ (e v - v) = K ∙ (e u - u)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ s ∪ t ∈ measurableCylinders α

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ s \ t ∈ measurableCylinders α

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (measurableCylinders α) = MeasurableSpace.pi

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
⊢ measurableCylinders X = ⋃ a, ⋃ S, ⋃ (_ : MeasurableSet S), {cylinder (Finset.Iic a) S}

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
⊢ cylinderEvents univ = MeasurableSpace.pi

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
⊢ ∀ ⦃s t : Set α⦄, s ∈ supClosure C → t ∈ supClosure C → s \ t ∈ supClosure C

Tactic:
by

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
⊢ t ∉ hC.disjointOfDiff hs ht

Tactic:
by

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

Tactic:
by

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
hst : t ⊆ s
⊢ ⋃₀ insert t ↑(hC.disjointOfDiff hs ht) = s

Tactic:
by

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
⊢ Disjoint t (⋃₀ ↑(hC.disjointOfDiff hs ht))

Tactic:
by

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
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
f : Dual K V
hfu : f u ≠ 0
v : V := (f u)⁻¹ • u
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
v_def : v = (f u)⁻¹ • u
hspan : K ∙ (e v - v) = K ∙ (e u - u)
⊢ f v = 1

Tactic:
by

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
⊢ (insert t ↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id

Tactic:
by

Goal state after:
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
⊢ ∃ P, ↑P.parts ⊆ C

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
⊢ Measurable fun p ↦ update p.1 i p.2

Tactic:
by

Goal state after:
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
⊢ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI) ⊆ s

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
⊢ ∀ (i : ι), univ ∈ {s | MeasurableSet s}

Tactic:
by

Goal state after:
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
⊢ Disjoint (⋃₀ ↑I) (⋃₀ ↑(hC.disjointOfDiffUnion hs hI))

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
⊢ ∅.Countable ∧ ∅ = ∅.domRestrict ⁻¹' ∅

Tactic:
by

Goal state after:
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
⊢ Disjoint I (hC.disjointOfDiffUnion hs hI)

Tactic:
by

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
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
⊢ ∃ f v,
    LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] ∧
      (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f ∧ f v = 1

Tactic:
by

Goal state after:
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
⊢ (↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Finset ι
t : (i : ι) → Set (α i)
⊢ (↑I).pi t = (↑I).domRestrict ⁻¹' univ.pi fun i ↦ t ↑i

Tactic:
by

Goal state after:
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}
⊢ instWithTopOfOrderTopology = generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}

Tactic:
by

Goal state after:
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) = s

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Set ι
t : Set ((a : ↑I) → α ↑a)
hI : I.Countable
⊢ (I.domRestrict ⁻¹' t)ᶜ = I.domRestrict ⁻¹' tᶜ

Tactic:
by

Goal state after:
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) = s

Tactic:
by

Goal state after:
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}
⊢ {⊤}.Countable

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
j : ↥J
⊢ hC.disjointOfUnion hJ ↑j = ⋯.choose.parts

Tactic:
by

Goal state after:
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}
⊢ {↑x₁}.Countable

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

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

Tactic:
by

Goal state after:
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) ⊆ C

Tactic:
by

Goal state after:
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

Goal state after: