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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a + coheight a)

pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a + coheight a)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, ⋯⟩ + i
⊢ j < p.length

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
this : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], krullDim α < ⊤ → ↑(⨆ a, height a + coheight a) ≤ krullDim α
hnottop : ¬krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

pp: α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

Tactic:
·

Goal state after:
case a.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
this : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], krullDim α < ⊤ → ↑(⨆ a, height a + coheight a) ≤ krullDim α
hnottop : ¬krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℤ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + ↑j ≤ p.toFun ⟨j, ⋯⟩ + ↑i
⊢ j < p.length

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
this : ∀ (i j : Fin (s.length + 1)), i ≠ j → s.toFun i = s.toFun j → i < j → False
hl : ¬i < j
⊢ False

pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
hl : i < j
⊢ False

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
this : ∀ (i j : Fin (s.length + 1)), i ≠ j → s.toFun i = s.toFun j → i < j → False
hl : ¬i < j
⊢ False
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
this : ∀ (i j : Fin (s.length + 1)), i ≠ j → s.toFun i = s.toFun j → i < j → False
hl : ¬i < j
⊢ j < i

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ height ⊤ ≤ ⨆ p, ↑p.length

pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ⨆ p, ↑p.length ≤ height ⊤

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ height ⊤ ≤ ⨆ p, ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ⨆ p, ↑p.length ≤ height ⊤

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ⨆ p, ↑p.length ≤ height ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

pp: case neg
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg.mp
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

pp: case neg.mpr
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α

Tactic:
·

Goal state after:
case neg.mp
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg.mpr
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α

Tactic:
·

Goal state after:
case neg.mpr
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ height n ≤ ↑n

pp: case a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ ↑n ≤ height n

Tactic:
·

Goal state after:
case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ height n ≤ ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ ↑n ≤ height n

Tactic:
·

Goal state after:
case a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ ↑n ≤ height n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : i = 0
⊢ (if ⟨i, hi⟩.castSucc = 0 then a else ↑(f ↑⟨i, hi⟩.castSucc), if ⟨i, hi⟩.succ = 0 then a else ↑(f ↑⟨i, hi⟩.succ)) ∈
    {(a, b) | a < b}

pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ (if ⟨i, hi⟩.castSucc = 0 then a else ↑(f ↑⟨i, hi⟩.castSucc), if ⟨i, hi⟩.succ = 0 then a else ↑(f ↑⟨i, hi⟩.succ)) ∈
    {(a, b) | a < b}

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : i = 0
⊢ (if ⟨i, hi⟩.castSucc = 0 then a else ↑(f ↑⟨i, hi⟩.castSucc), if ⟨i, hi⟩.succ = 0 then a else ↑(f ↑⟨i, hi⟩.succ)) ∈
    {(a, b) | a < b}
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ (if ⟨i, hi⟩.castSucc = 0 then a else ↑(f ↑⟨i, hi⟩.castSucc), if ⟨i, hi⟩.succ = 0 then a else ↑(f ↑⟨i, hi⟩.succ)) ∈
    {(a, b) | a < b}

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ (if ⟨i, hi⟩.castSucc = 0 then a else ↑(f ↑⟨i, hi⟩.castSucc), if ⟨i, hi⟩.succ = 0 then a else ↑(f ↑⟨i, hi⟩.succ)) ∈
    {(a, b) | a < b}
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x + 1

pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x + 1 ≤ height ↑x

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.inr
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
this :
  ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α)),
    RelSeries.last p = ↑x → p.length ≠ 0 → ↑p.length ≤ height x + 1
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x + 1

pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ height x + 1

Tactic:
·

Goal state after:
case a.inr
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
this :
  ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α)),
    RelSeries.last p = ↑x → p.length ≠ 0 → ↑p.length ≤ height x + 1
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
x✝ : Fin (p.length - 1 + 1)
i : ℕ
hi : i < p.length - 1 + 1
⊢ i + 1 < p.length + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
i : Fin (p.length - 1)
⊢ ↑i + 1 < p.length

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x + 1 ≤ height ↑x

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x + 1 ≤ height ↑x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x

pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ height ↑x

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case hab
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun i ≤ ?b

pp: case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ ?b < ⊤

pp: case b
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ WithTop α

Tactic:
·

Goal state after:
case hab
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun i ≤ ?b
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun (Fin.last p.length) < ⊤

Tactic:
·

Goal state after:
case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun (Fin.last p.length) < ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x

pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ height ↑x

Tactic:
· apply height_le
    intro p hlast
    -- essentially p' := p.map untop
    let p' : LTSeries α := {
      length := p.length
      toFun := fun i => (p i).untop (by
        apply WithTop.lt_top_iff_ne_top.mp
        apply lt_of_le_of_lt
        · exact p.monotone (Fin.le_last _)
        · rw [RelSeries.last] at hlast
          simp [hlast])
      step := fun i => by simpa [WithTop.untop_lt_iff, WithTop.coe_untop] using p.step i }
    have hlast' : p'.last = x := by
      simp only [p', RelSeries.last, WithTop.untop_eq_iff, ← hlast]
    suffices p'.length ≤ height p'.last by
      rw [hlast'] at this
      simpa [p'] using this
    apply length_le_height_last

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ height ↑x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ height ↑x

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ height ↑x
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mp
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a) →
    ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a

pp: case insert.mpr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a) →
    ∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a

Tactic:
·

Goal state after:
case insert.mp
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a) →
    ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case closed_under_smul
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄,
    r ∈ sR →
      n ∈ N → r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

pp: case le
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR) ≤ sR • N

Tactic:
·

Goal state after:
case closed_under_smul
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄,
    r ∈ sR →
      n ∈ N → r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR) ≤ sR • N

Tactic:
·

Goal state after:
case le
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR) ≤ sR • N
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le.refine_1
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ ∀ c_1 ∈ c.support, ↑((DistribSMul.toLinearMap R (↥N) c_1) (c c_1)) ∈ sR • N

pp: case le.refine_2
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ (fun s ↦ ⋂ (_ : s ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}), ↑s) (sR • N) = ↑(sR • N)

Tactic:
·

Goal state after:
case le.refine_1
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ ∀ c_1 ∈ c.support, ↑((DistribSMul.toLinearMap R (↥N) c_1) (c c_1)) ∈ sR • N
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i is → update g i x i_1 ∈ f i_1

pp: case insert.mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ update g i x i * ∏ i_1 ∈ is, update g i x i_1 = x * ∏ i ∈ is, g i

Tactic:
·

Goal state after:
case insert.mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i is → update g i x i_1 ∈ f i_1
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mp.refine_1.inl
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
is : Finset ι
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hi : j ∉ is
y : x ∈ f j
hj : j ∈ insert j is
⊢ update g j x j ∈ f j

pp: case insert.mp.refine_1.inr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ update g i x j ∈ f j

Tactic:
·

Goal state after:
case insert.mp.refine_1.inl
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
is : Finset ι
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hi : j ∉ is
y : x ∈ f j
hj : j ∈ insert j is
⊢ update g j x j ∈ f j
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le.refine_2
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ (fun s ↦ ⋂ (_ : s ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}), ↑s) (sR • N) = ↑(sR • N)

Tactic:
·

Goal state after:
case le.refine_2
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ (fun s ↦ ⋂ (_ : s ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}), ↑s) (sR • N) = ↑(sR • N)
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le.refine_2.mp
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ (sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N) → x ∈ sR • N

pp: case le.refine_2.mpr
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ x ∈ sR • N → sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N

Tactic:
·

Goal state after:
case le.refine_2.mp
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ (sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N) → x ∈ sR • N
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mp.refine_1.inr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ update g i x j ∈ f j

Tactic:
·

Goal state after:
case insert.mp.refine_1.inr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ update g i x j ∈ f j
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ update g i x i * ∏ i_1 ∈ is, update g i x i_1 = x * ∏ i ∈ is, g i

Tactic:
·

Goal state after:
case insert.mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ update g i x i * ∏ i_1 ∈ is, update g i x i_1 = x * ∏ i ∈ is, g i
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le.refine_2.mpr
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ x ∈ sR • N → sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N

Tactic:
·

Goal state after:
case le.refine_2.mpr
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ x ∈ sR • N → sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mpr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a) →
    ∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a

Tactic:
·

Goal state after:
case insert.mpr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a) →
    ∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a