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

Goal state before:
pp: R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (m : R) (x : α ⊕ β → M),
    (Equiv.sumArrowEquivProdArrow α β M).toFun (m • x) = (RingHom.id R) m • (Equiv.sumArrowEquivProdArrow α β M).toFun x

Tactic:
intro r f

Goal state after:
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
f : α ⊕ β → M
⊢ (Equiv.sumArrowEquivProdArrow α β M).toFun (r • f) = (RingHom.id R) r • (Equiv.sumArrowEquivProdArrow α β M).toFun f
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
k : ι'
⊢ x (Sum.inr k) = 0

pp: case refine_2
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
⊢ x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)

Tactic:
·

Goal state after:
case refine_1
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
k : ι'
⊢ x (Sum.inr k) = 0
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
⊢ x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)

Tactic:
·

Goal state after:
case refine_2
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
⊢ x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2.inl
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι
⊢ x (Sum.inl i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inl i)

pp: case refine_2.inr
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι'
⊢ x (Sum.inr i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inr i)

Tactic:
·

Goal state after:
case refine_2.inl
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι
⊢ x (Sum.inl i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inl i)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2.inr
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι'
⊢ x (Sum.inr i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inr i)

Tactic:
·

Goal state after:
case refine_2.inr
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι'
⊢ x (Sum.inr i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inr i)
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case h₁
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (m, 0) ∈ fst R M M₂ ⊔ snd R M M₂

pp: case h₂
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (0, n) ∈ fst R M M₂ ⊔ snd R M M₂

Tactic:
·

Goal state after:
case h₁
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (m, 0) ∈ fst R M M₂ ⊔ snd R M M₂
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case h₂
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (0, n) ∈ fst R M M₂ ⊔ snd R M M₂

Tactic:
·

Goal state after:
case h₂
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (0, n) ∈ fst R M M₂ ⊔ snd R M M₂
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ q ≤ p₁.prod p₂ → map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂

pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂ → q ≤ p₁.prod p₂

Tactic:
·

Goal state after:
case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ q ≤ p₁.prod p₂ → map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.left
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.fst R M M₂) q ≤ p₁

pp: case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.snd R M M₂) q ≤ p₂

Tactic:
·

Goal state after:
case mp.left
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.fst R M M₂) q ≤ p₁
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ ⨆ i, f i ≤ ⨆ i, f i ⊔ a

pp: case refine_2
α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ≤ ⨆ i, f i ⊔ a

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ ⨆ i, f i ≤ ⨆ i, f i ⊔ a
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ≤ ⨆ i, f i ⊔ a

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ≤ ⨆ i, f i ⊔ a
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.snd R M M₂) q ≤ p₂

Tactic:
·

Goal state after:
case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.snd R M M₂) q ≤ p₂
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂ → q ≤ p₁.prod p₂

Tactic:
·

Goal state after:
case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂ → q ≤ p₁.prod p₂
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ p₁.prod p₂ ≤ q → map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q

pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q → p₁.prod p₂ ≤ q

Tactic:
·

Goal state after:
case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ p₁.prod p₂ ≤ q → map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.left
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
⊢ map (inl R M M₂) p₁ ≤ q

pp: case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
⊢ map (inr R M M₂) p₂ ≤ q

Tactic:
·

Goal state after:
case mp.left
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
⊢ map (inl R M M₂) p₁ ≤ q
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
⊢ map (inr R M M₂) p₂ ≤ q

Tactic:
·

Goal state after:
case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
⊢ map (inr R M M₂) p₂ ≤ q
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q → p₁.prod p₂ ≤ q

Tactic:
·

Goal state after:
case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q → p₁.prod p₂ ≤ q
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)

pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)

Tactic:
·

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)

Tactic:
·

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ Order.succ i → a✝ ≤ i ∨ a✝ = Order.succ i

pp: case mpr
α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ i ∨ a✝ = Order.succ i → a✝ ≤ Order.succ i

Tactic:
·

Goal state after:
case mp
α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ Order.succ i → a✝ ≤ i ∨ a✝ = Order.succ i
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ i ∨ a✝ = Order.succ i → a✝ ≤ Order.succ i

Tactic:
·

Goal state after:
case mpr
α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ i ∨ a✝ = Order.succ i → a✝ ≤ Order.succ i
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ (Iic i).sup' ⋯ f ≤ ⨆ i_1, f ↑i_1

pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨆ i_1, f ↑i_1 ≤ (Iic i).sup' ⋯ f

Tactic:
·

Goal state after:
case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ (Iic i).sup' ⋯ f ≤ ⨆ i_1, f ↑i_1
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨆ i_1, f ↑i_1 ≤ (Iic i).sup' ⋯ f

Tactic:
·

Goal state after:
case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨆ i_1, f ↑i_1 ≤ (Iic i).sup' ⋯ f
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

pp: case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : ¬Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
·

Goal state after:
case pos
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case pos.refine_1
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
i : ι
⊢ (partialSups f) i ≤ ⨆ i, f i

pp: case pos.refine_2
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range fun i ↦ (partialSups f) i)

Tactic:
·

Goal state after:
case pos.refine_1
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
i : ι
⊢ (partialSups f) i ≤ ⨆ i, f i
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case pos.refine_2
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range fun i ↦ (partialSups f) i)

Tactic:
·

Goal state after:
case pos.refine_2
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range fun i ↦ (partialSups f) i)
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : ¬Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
·

Goal state after:
case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : ¬Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

pp: case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
·

Goal state after:
case pos
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
·

Goal state after:
case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f ≤ partialSups g
⊢ ⨆ i, f i ≤ ⨆ i, g i

Tactic:
← iSup_partialSups_eq f,

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f ≤ partialSups g
⊢ ⨆ i, (partialSups f) i ≤ ⨆ i, g i
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f = partialSups g
⊢ ⨆ i, f i = ⨆ i, g i

Tactic:
← iSup_partialSups_eq f,

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f = partialSups g
⊢ ⨆ i, (partialSups f) i = ⨆ i, g i
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case refine_1
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ x' + x - x ∈ f.ker

pp: case refine_2
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ g (x' + x) = g y

Tactic:
·

Goal state after:
case refine_1
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ x' + x - x ∈ f.ker
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case right.a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ (partialSups f) i ≤ f j

pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ f j ≤ (partialSups f) i

Tactic:
·

Goal state after:
case right.a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ (partialSups f) i ≤ f j
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ f j ≤ (partialSups f) i

Tactic:
·

Goal state after:
case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ f j ≤ (partialSups f) i