mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inr.coe.coe.refine_2.hs.ht
ι : 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₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ g, Iio ↑z)

Tactic:
·

Goal state after:
case a.inr.coe.coe.refine_2.hs.ht
ι : 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₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ g, Iio ↑z)
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inr.coe.coe.refine_2.hs.ht.hs
ι : 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₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ g.Finite

pp: case a.inr.coe.coe.refine_2.hs.ht.h
ι : 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₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ ∀ i ∈ g, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ↑i)

Tactic:
·

Goal state after:
case a.inr.coe.coe.refine_2.hs.ht.hs
ι : 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₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ g.Finite
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inr.coe.coe.refine_2.hs.ht.h
ι : 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₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ ∀ i ∈ g, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ↑i)

Tactic:
·

Goal state after:
case a.inr.coe.coe.refine_2.hs.ht.h
ι : 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₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ ∀ i ∈ g, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ↑i)
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: case inr
α : 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₂ : ℕ → ℝ
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 ?u.192} {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₀ : ∀ (j : ℕ), d ∈ cthickening (r₁ (f j)) (s (f j))
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)
j : ℕ
hrp : 0 ≤ r₁ (f j)
hrp' : 0 < r₁ (f j)
⊢ ∃ w ∈ s (f j), d ∈ closedBall w (2 * r₁ (f j))

Tactic:
·

Goal state after:
case inr
α : 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₂ : ℕ → ℝ
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 ?u.192} {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₀ : ∀ (j : ℕ), d ∈ cthickening (r₁ (f j)) (s (f j))
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)
j : ℕ
hrp : 0 ≤ r₁ (f j)
hrp' : 0 < r₁ (f j)
⊢ ∃ w ∈ s (f j), d ∈ closedBall w (2 * r₁ (f j))
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case inl
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn0 : n = 0
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e

pp: case inr
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e

Tactic:
·

Goal state after:
case inl
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn0 : n = 0
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case inl.refine_1
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn0 : n = 0
⊢ (auxTransvection hf)⁻¹ ∈ transvections K V

pp: case inl.refine_2
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn0 : n = 0
⊢ auxTransvection hf * e ∈ dilatransvections K V

Tactic:
·

Goal state after:
case inl.refine_1
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn0 : n = 0
⊢ (auxTransvection hf)⁻¹ ∈ transvections K V
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
h : IsEmpty ι
⊢ Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, ↑i < x a

pp: case inr
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
h : Nonempty ι
⊢ Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, ↑i < x a

Tactic:
·

Goal state after:
case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
h : IsEmpty ι
⊢ Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, ↑i < x a
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : NoMaxOrder ι
h : IsEmpty ι
⊢ Tendsto some atTop (𝓝 ⊤)

pp: case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : NoMaxOrder ι
h : Nonempty ι
⊢ Tendsto some atTop (𝓝 ⊤)

Tactic:
·

Goal state after:
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : NoMaxOrder ι
h : IsEmpty ι
⊢ Tendsto some atTop (𝓝 ⊤)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case succ.inr
α : 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 v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ ↑I
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left✝ : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ ↑I' = Set.Ioc u u'
IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u
⊢ f v - f u = f v - f u' + (f u' - f u)

pp: case succ.inr
α : 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 v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ ↑I
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left✝ : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ ↑I' = Set.Ioc u u'
IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u
⊢ Set.Ioc u' v ∉ I'

Tactic:
·

Goal state after:
case succ.inr
α : 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 v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ ↑I
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left✝ : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ ↑I' = Set.Ioc u u'
IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u
⊢ f v - f u = f v - f u' + (f u' - f u)
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case inl.refine_2
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn0 : n = 0
⊢ auxTransvection hf * e ∈ dilatransvections K V

Tactic:
·

Goal state after:
case inl.refine_2
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn0 : n = 0
⊢ auxTransvection hf * e ∈ dilatransvections K V
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case succ.inr
α : 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 v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ ↑I
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left✝ : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ ↑I' = Set.Ioc u u'
IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u
⊢ Set.Ioc u' v ∉ I'

Tactic:
·

Goal state after:
case succ.inr
α : 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 v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ ↑I
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left✝ : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ ↑I' = Set.Ioc u u'
IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u
⊢ Set.Ioc u' v ∉ I'
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ ⋃₀ ↑I ∈ C

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
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ m (⋃₀ ↑I) = ∑ u ∈ I, extend (fun x x_1 ↦ m x) u

Tactic:
·

Goal state after:
case h
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ ⋃₀ ↑I ∈ C
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case pos
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∈ transvections K V ^ n * dilatransvections K V
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e

pp: case neg
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∉ transvections K V ^ n * dilatransvections K V
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e

Tactic:
·

Goal state after:
case pos
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∈ transvections K V ^ n * dilatransvections K V
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e