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

Goal state before:
pp: R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊤ = ⊤

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst✝¹⁴ : DecidableEq ι
inst✝¹³ : DecidableEq κ
inst✝¹² : Fintype ι
inst✝¹¹ : Fintype κ
inst✝¹⁰ : Finite ι'
inst✝⁹ : Finite κ'
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
A : Matrix ι' ι R
B : Matrix κ' κ R
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) A B = kroneckerMap (fun x1 x2 ↦ x1 * x2) A B

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
x' x : α
h✝ : r x' x
a : α
h : a ∈ {x'}
⊢ r x' x

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
x' x : α
h✝ : r x' x
a : α
h : a ∈ {x'}
⊢ r x' x
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
t u s x✝¹ : Multiset α
x✝ : α
⊢ t + {x✝} = u + x✝¹ ↔ t + {x✝} = u + x✝¹

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Hydra

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

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
s : Multiset α
⊢ ¬∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ 0 ∧ s = erase 0 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
this✝ : finrank K ↥((↑e).fixedSubmodule ⊓ (↑f).fixedSubmodule) ≤ finrank K ↥(↑e ∘ₗ ↑f).fixedSubmodule
this :
  finrank K ↥(↑e).fixedSubmodule + finrank K ↥(↑f).fixedSubmodule ≤
    finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + finrank K ↥(↑e ∘ₗ ↑f).fixedSubmodule
⊢ finrank K ↥(↑e).fixedSubmodule + finrank K ↥(↑f).fixedSubmodule ≤
    finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + finrank K ↥(↑(e * f)).fixedSubmodule

Tactic:
]

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 f : V ≃ₗ[K] V
this✝ : finrank K ↥((↑e).fixedSubmodule ⊓ (↑f).fixedSubmodule) ≤ finrank K ↥(↑e ∘ₗ ↑f).fixedSubmodule
this :
  finrank K ↥(↑e).fixedSubmodule + finrank K ↥(↑f).fixedSubmodule ≤
    finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + finrank K ↥(↑e ∘ₗ ↑f).fixedSubmodule
⊢ finrank K ↥(↑e).fixedSubmodule + finrank K ↥(↑f).fixedSubmodule ≤
    finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + finrank K ↥(↑(e * f)).fixedSubmodule
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
he : e ∈ dilatransvections K V
⊢ finrank K V + finrank K ↥(↑e - LinearMap.id).range ≤ finrank K V + 1

Tactic:
]

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
he : e ∈ dilatransvections K V
⊢ finrank K V + finrank K ↥(↑e - LinearMap.id).range ≤ finrank K V + 1
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s₁ ∨ a ∈ s₂ + t
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s₁ ∨ a ∈ s₂ + t
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
Module: Mathlib.Logic.Hydra

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

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Category.MeasCat

Goal state before:
pp: μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ ∫⁻ (μ : MeasureTheory.Measure ℝ≥0∞), ∫⁻ (x : ℝ≥0∞), x ∂μ ∂μ =
    ∫⁻ (a : MeasureTheory.Measure ℝ≥0∞), ∫⁻ (x : ℝ≥0∞), x ∂a ∂μ

pp: case hf
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun x ↦ x

pp: case hg
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun m ↦ ∫⁻ (x : ℝ≥0∞), x ∂m

pp: μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ AEMeasurable (fun x ↦ x) μ.join

Tactic:
]

Goal state after:
case hf
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun x ↦ x

case hg
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun m ↦ ∫⁻ (x : ℝ≥0∞), x ∂m

μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ AEMeasurable (fun x ↦ x) μ.join
Module: Mathlib.Logic.Hydra

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

Tactic:
]

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 f : V ≃ₗ[K] V
hf : f⁻¹ ∈ dilatransvections K V
⊢ finrank K ↥(↑(f * e)).fixedSubmodule ≤ 1 + finrank K ↥(↑(f⁻¹ * (f * e))).fixedSubmodule

Tactic:
]

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 f : V ≃ₗ[K] V
hf : f⁻¹ ∈ dilatransvections K V
⊢ finrank K ↥(↑(f * e)).fixedSubmodule ≤ 1 + finrank K ↥(↑(f⁻¹ * (f * e))).fixedSubmodule
Module: Mathlib.Logic.Hydra

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

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Hydra

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

Tactic:
]

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 f : V ≃ₗ[K] V
hf : f⁻¹ ∈ dilatransvections K V
⊢ finrank K ↥(↑(e * f)).fixedSubmodule ≤ 1 + finrank K ↥(↑(e * f * f⁻¹)).fixedSubmodule

Tactic:
]

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 f : V ≃ₗ[K] V
hf : f⁻¹ ∈ dilatransvections K V
⊢ finrank K ↥(↑(e * f)).fixedSubmodule ≤ 1 + finrank K ↥(↑(e * f * f⁻¹)).fixedSubmodule
Module: Mathlib.Logic.Hydra

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

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
⊢ (∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t) → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
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
this : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑(transvection hfv * e)).fixedSubmodule
⊢ finrank K ↥(↑(transvection hfv * e)).fixedSubmodule ≤ 1 + finrank K ↥(↑e).fixedSubmodule

Tactic:
]

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
this : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑(transvection hfv * e)).fixedSubmodule
⊢ finrank K ↥(↑(transvection hfv * e)).fixedSubmodule ≤ 1 + finrank K ↥(↑e).fixedSubmodule
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) ({a} + s)

Tactic:
]

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) ({a} + s)
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : Acc (CutExpand r) {a} ∧ ∀ x ∈ s, Acc (CutExpand r) {x}
⊢ Acc (CutExpand r) ({a} + s)

Tactic:
]

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : Acc (CutExpand r) {a} ∧ ∀ x ∈ s, Acc (CutExpand r) {x}
⊢ Acc (CutExpand r) ({a} + s)
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
⊢ f x = 0 ∨ v - e v = 0

Tactic:
]

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.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
⊢ f x ∈ map f (↑e).fixedSubmodule

Tactic:
]

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 ∈ map f (↑e).fixedSubmodule
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case intro
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a✝ : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ t → Acc (CutExpand r) {a'}

Tactic:
]

Goal state after:
case intro
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a✝ : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ t → Acc (CutExpand r) {a'}
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case left
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
ht : (↑e).fixedSubmodule ≤ (↑(transvection hfv)).fixedSubmodule
x : V
hx : x ∈ (↑e).fixedSubmodule
⊢ x ∈ (↑(transvection hfv)).fixedSubmodule

Tactic:
]

Goal state after:
case left
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
ht : (↑e).fixedSubmodule ≤ (↑(transvection hfv)).fixedSubmodule
x : V
hx : x ∈ (↑e).fixedSubmodule
⊢ x ∈ (↑(transvection hfv)).fixedSubmodule
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
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
⊢ ∃ a, a • (e u - u) = u - e u

Tactic:
]

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 f✝ : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
⊢ ∃ a, a • (e u - u) = u - e u
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case hv
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
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
hu' : f u = 0
⊢ False

Tactic:
]

Goal state after:
case hv
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
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
hu' : f u = 0
⊢ False
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case hf
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
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ map f (↑e).fixedSubmodule ≤ ⊥

Tactic:
]

Goal state after:
case hf
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
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ map f (↑e).fixedSubmodule ≤ ⊥
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case hf
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
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ (↑e).fixedSubmodule ≤ ker f

Tactic:
]

Goal state after:
case hf
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
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ (↑e).fixedSubmodule ≤ ker f
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case hfv'
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
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ e u - u ∈ ker f

Tactic:
]

Goal state after:
case hfv'
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
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ e u - u ∈ ker f
Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Finset ι
S : Set ((i : ↥s) → X ↑i)
hS_closed : IsClosed S
hS_compact : IsCompact S
⊢ ∃ s_1 S_1, IsClosed S_1 ∧ IsCompact S_1 ∧ cylinder s S = cylinder s_1 S_1

Tactic:
]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Finset ι
S : Set ((i : ↥s) → X ↑i)
hS_closed : IsClosed S
hS_compact : IsCompact S
⊢ ∃ s_1 S_1, IsClosed S_1 ∧ IsCompact S_1 ∧ cylinder s S = cylinder s_1 S_1
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 + 1) = 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)

Tactic:
]

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 + 1) = 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.ClosedCompactCylinders

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
ht : t ∈ closedCompactCylinders X
⊢ ∃ s S, MeasurableSet 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)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
ht : t ∈ closedCompactCylinders X
⊢ ∃ s S, MeasurableSet 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)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
ht : t ∈ closedCompactCylinders X
⊢ t ∈ measurableCylinders X

Tactic:
rw [mem_measurableCylinders]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
ht : t ∈ closedCompactCylinders X
⊢ ∃ s S, MeasurableSet S ∧ t = cylinder s S
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
hW : 1 < finrank K (V ⧸ W)
⊢ W ⊔ K ∙ v ≠ ⊤

Tactic:
]

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
hW : 1 < finrank K (V ⧸ W)
⊢ W ⊔ K ∙ v ≠ ⊤
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
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
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
⊢ ((↑s₁ ∪ ↑s₂).pi fun i ↦ t₁' i ∩ t₂' i) ∈ squareCylinders C

Tactic:
]

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
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
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
⊢ ((↑s₁ ∪ ↑s₂).pi fun i ↦ t₁' i ∩ t₂' i) ∈ squareCylinders C
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
hW : 1 < finrank K (V ⧸ W)
htop : W ⊔ K ∙ v = ⊤
h1 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
h2 : finrank K V ≤ finrank K ↥W + 1
⊢ False

Tactic:
]

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
hW : 1 < finrank K (V ⧸ W)
htop : W ⊔ K ∙ v = ⊤
h1 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
h2 : finrank K V ≤ finrank K ↥W + 1
⊢ False
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case refine_1
ι : 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
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
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 : ι), t₁' i ∩ t₂' i ∈ C i

Tactic:
]

Goal state after:
case refine_1
ι : 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
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
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 : ι), t₁' i ∩ t₂' i ∈ C i
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
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
hu : u ∉ (↑e).fixedSubmodule
⊢ finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ u) + 1 = finrank K (V ⧸ (↑e).fixedSubmodule)

Tactic:
]

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
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
hu : u ∉ (↑e).fixedSubmodule
⊢ finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ u) + 1 = finrank K (V ⧸ (↑e).fixedSubmodule)