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

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder α
⊢ IsSimpleOrder αᵒᵈ

pp: case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder α
⊢ IsSimpleOrder αᵒᵈ
Module: Mathlib.Order.Atoms

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ 0 ∈ span R ↑T

pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (x y : M),
    x ∈ span R S →
      y ∈ span R S → (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → (∃ T, ↑T ⊆ S ∧ y ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T

pp: case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (a : R), ∀ x ∈ span R S, (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ 0 ∈ span R ↑T
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure s,
    ∀ b ∈ latticeClosure s,
      a ∈ f ⁻¹' latticeClosure (f '' s) → b ∈ f ⁻¹' latticeClosure (f '' s) → a ⊔ b ∈ f ⁻¹' latticeClosure (f '' s)

Tactic:
rintro a - b - ha hb
    simpa [map_sup] using isSublattice_latticeClosure.supClosed ha hb

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (x y : M),
    x ∈ span R S →
      y ∈ span R S → (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → (∃ T, ↑T ⊆ S ∧ y ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T

pp: case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (a : R), ∀ x ∈ span R S, (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (x y : M),
    x ∈ span R S →
      y ∈ span R S → (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → (∃ T, ↑T ⊆ S ∧ y ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_3.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ↑(X ∪ Y) ⊆ S

pp: case refine_3.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ x + y ∈ span R ↑(X ∪ Y)

Tactic:
·

Goal state after:
case refine_3.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ↑(X ∪ Y) ⊆ S
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case left.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure s,
    ∀ b ∈ latticeClosure s,
      a ∈ f ⁻¹' latticeClosure (f '' s) → b ∈ f ⁻¹' latticeClosure (f '' s) → a ⊓ b ∈ f ⁻¹' latticeClosure (f '' s)

pp: case right.mem
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ f '' s, a ∈ f '' latticeClosure s

pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s

pp: case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s

Tactic:
·

Goal state after:
case left.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure s,
    ∀ b ∈ latticeClosure s,
      a ∈ f ⁻¹' latticeClosure (f '' s) → b ∈ f ⁻¹' latticeClosure (f '' s) → a ⊓ b ∈ f ⁻¹' latticeClosure (f '' s)
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b c : α
⊢ ⊥ ≤ b → b ≤ c → ⊥ ≤ c

pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b c : α
⊢ ⊤ ≤ b → b ≤ c → ⊤ ≤ c

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b c : α
⊢ ⊥ ≤ b → b ≤ c → ⊥ ≤ c
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b c : α
⊢ ⊤ ≤ b → b ≤ c → ⊤ ≤ c

Tactic:
·

Goal state after:
case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b c : α
⊢ ⊤ ≤ b → b ≤ c → ⊤ ≤ c
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ c → ⊤ ≤ c

pp: case inr.inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊤ → ⊤ ≤ c → ⊤ ≤ c

Tactic:
·

Goal state after:
case inr.inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ c → ⊤ ≤ c
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊤ → ⊤ ≤ c → ⊤ ≤ c

Tactic:
·

Goal state after:
case inr.inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊤ → ⊤ ≤ c → ⊤ ≤ c
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case left.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure s,
    ∀ b ∈ latticeClosure s,
      a ∈ f ⁻¹' latticeClosure (f '' s) → b ∈ f ⁻¹' latticeClosure (f '' s) → a ⊓ b ∈ f ⁻¹' latticeClosure (f '' s)

pp: case right.mem
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ f '' s, a ∈ f '' latticeClosure s

pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s

pp: case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s

Tactic:
· rintro a - b - ha hb
    simpa [map_inf] using isSublattice_latticeClosure.infClosed ha hb

Goal state after:
case right.mem
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ f '' s, a ∈ f '' latticeClosure s

case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s

case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (a : R), ∀ x ∈ span R S, (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T

Tactic:
·

Goal state after:
case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (a : R), ∀ x ∈ span R S, (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case right.mem
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ f '' s, a ∈ f '' latticeClosure s

pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s

pp: case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s

Tactic:
·

Goal state after:
case right.mem
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ f '' s, a ∈ f '' latticeClosure s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s

pp: case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s

Tactic:
·

Goal state after:
case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s

Tactic:
·

Goal state after:
case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
⊢ equivBool ⊥ ≤ equivBool b ↔ ⊥ ≤ b

pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
⊢ equivBool ⊤ ≤ equivBool b ↔ ⊤ ≤ b

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
⊢ equivBool ⊥ ≤ equivBool b ↔ ⊥ ≤ b
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
⊢ equivBool ⊤ ≤ equivBool b ↔ ⊤ ≤ b

Tactic:
·

Goal state after:
case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
⊢ equivBool ⊤ ≤ equivBool b ↔ ⊤ ≤ b
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ equivBool ⊤ ≤ equivBool ⊥ ↔ ⊤ ≤ ⊥

pp: case inr.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ equivBool ⊤ ≤ equivBool ⊤ ↔ ⊤ ≤ ⊤

Tactic:
·

Goal state after:
case inr.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ equivBool ⊤ ≤ equivBool ⊥ ↔ ⊤ ≤ ⊥
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ equivBool ⊤ ≤ equivBool ⊤ ↔ ⊤ ≤ ⊤

Tactic:
·

Goal state after:
case inr.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ equivBool ⊤ ≤ equivBool ⊤ ↔ ⊤ ≤ ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (⊥ ⊓ if ⊥ = ⊥ then ⊤ else ⊥) ≤ ⊥

pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (⊤ ⊓ if ⊤ = ⊥ then ⊤ else ⊥) ≤ ⊥

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (⊥ ⊓ if ⊥ = ⊥ then ⊤ else ⊥) ≤ ⊥
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case mp
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, ∃ z ∈ span R s, x = a • y + z) → ∃ a, x + a • y ∈ span R s

pp: case mpr
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, x + a • y ∈ span R s) → ∃ a, ∃ z ∈ span R s, x = a • y + z

Tactic:
·

Goal state after:
case mp
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, ∃ z ∈ span R s, x = a • y + z) → ∃ a, x + a • y ∈ span R s
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (⊤ ⊓ if ⊤ = ⊥ then ⊤ else ⊥) ≤ ⊥

Tactic:
·

Goal state after:
case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (⊤ ⊓ if ⊤ = ⊥ then ⊤ else ⊥) ≤ ⊥
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, x + a • y ∈ span R s) → ∃ a, ∃ z ∈ span R s, x = a • y + z

Tactic:
·

Goal state after:
case mpr
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, x + a • y ∈ span R s) → ∃ a, ∃ z ∈ span R s, x = a • y + z
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
⊢ x ≤ if ⊤ ∈ s then ⊤ else ⊥

pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ x

Tactic:
·

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
⊢ x ≤ if ⊤ ∈ s then ⊤ else ⊥
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ s
⊢ ⊥ ≤ if ⊤ ∈ s then ⊤ else ⊥

pp: case refine_1.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ s
⊢ ⊤ ≤ if ⊤ ∈ s then ⊤ else ⊥

Tactic:
·

Goal state after:
case refine_1.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ s
⊢ ⊥ ≤ if ⊤ ∈ s then ⊤ else ⊥
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ s
⊢ ⊤ ≤ if ⊤ ∈ s then ⊤ else ⊥

Tactic:
·

Goal state after:
case refine_1.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ s
⊢ ⊤ ≤ if ⊤ ∈ s then ⊤ else ⊥
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ x

Tactic:
·

Goal state after:
case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ x
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊥

pp: case refine_2.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊤

Tactic:
·

Goal state after:
case refine_2.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊥
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊤

Tactic:
·

Goal state after:
case refine_2.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
⊢ (if ⊥ ∈ s then ⊥ else ⊤) ≤ x

pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ lowerBounds s
⊢ x ≤ if ⊥ ∈ s then ⊥ else ⊤

Tactic:
·

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
⊢ (if ⊥ ∈ s then ⊥ else ⊤) ≤ x
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ update v j (v j + r • v i) j ∈ span R (range v)

pp: case refine_1.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ update v j (v j + r • v i) k ∈ span R (range v)

pp: case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j ∈ span R (range (update v j (v j + r • v i)))

pp: case refine_2.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ v k ∈ span R (range (update v j (v j + r • v i)))

Tactic:
·

Goal state after:
case refine_1.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ update v j (v j + r • v i) j ∈ span R (range v)