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

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
x✝² : u ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ u
⊢ Disjoint ((fun i ↦ t.sup fun i' ↦ f (i, i')) i) (u.sup fun i ↦ t.sup fun i' ↦ f (i, i'))

pp: case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
x✝² : u ⊆ t
i : ι'
x✝¹ : i ∈ t
x✝ : i ∉ u
⊢ Disjoint ((fun i' ↦ s.sup fun i ↦ f (i, i')) i) (u.sup fun i' ↦ s.sup fun i ↦ f (i, i'))

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
x✝² : u ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ u
⊢ Disjoint ((fun i ↦ t.sup fun i' ↦ f (i, i')) i) (u.sup fun i ↦ t.sup fun i' ↦ f (i, i'))
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
x✝² : u ⊆ t
i : ι'
x✝¹ : i ∈ t
x✝ : i ∉ u
⊢ Disjoint ((fun i' ↦ s.sup fun i ↦ f (i, i')) i) (u.sup fun i' ↦ s.sup fun i ↦ f (i, i'))

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
x✝² : u ⊆ t
i : ι'
x✝¹ : i ∈ t
x✝ : i ∉ u
⊢ Disjoint ((fun i' ↦ s.sup fun i ↦ f (i, i')) i) (u.sup fun i' ↦ s.sup fun i ↦ f (i, i'))
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) →
    ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id) →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) →
    ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mp
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ sSupIndep {a, b} → Disjoint a b

pp: case mpr
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ Disjoint a b → sSupIndep {a, b}

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ sSupIndep {a, b} → Disjoint a b
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ Disjoint a b → sSupIndep {a, b}

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ Disjoint a b → sSupIndep {a, b}
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inl
α : Type u_1
inst✝ : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ Disjoint c (sSup ({c, b} \ {c}))

pp: case mpr.inr
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))

Tactic:
·

Goal state after:
case mpr.inl
α : Type u_1
inst✝ : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ Disjoint c (sSup ({c, b} \ {c}))
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inr
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))

Tactic:
·

Goal state after:
case mpr.inr
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case h.left
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ x ⊔ y ∈ S

pp: case h.right
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ (fun x1 x2 ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun x1 x2 ↦ x1 ≤ x2) y (x ⊔ y)

Tactic:
·

Goal state after:
case h.left
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ x ⊔ y ∈ S
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case h.left
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ ↑(c ∪ d) ⊆ s

pp: case h.right
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ x ⊔ y = (c ∪ d).sup id

Tactic:
·

Goal state after:
case h.left
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ ↑(c ∪ d) ⊆ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case h.right
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ x ⊔ y = (c ∪ d).sup id

Tactic:
·

Goal state after:
case h.right
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ x ⊔ y = (c ∪ d).sup id
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
h_eq : ⨅ i, t i (b₁ i) = ⨅ i, t i (b₂ i)
h_ne : ¬b₁ = b₂
i : ι
hi : b₁ i ≠ b₂ i
⊢ False

Tactic:
have := calc
    ⨅ i, t i (b₁ i) ≤ t i (b₁ i) ⊓ t i (b₂ i) := le_inf (iInf_le ..) (h_eq ▸ iInf_le ..)
    _ = ⊥ := (ht i (b₁ i) |>.mono_right <| le_iSup₂_of_le (b₂ i) hi.symm le_rfl).eq_bot

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
h_eq : ⨅ i, t i (b₁ i) = ⨅ i, t i (b₂ i)
h_ne : ¬b₁ = b₂
i : ι
hi : b₁ i ≠ b₂ i
this : ⨅ i, t i (b₁ i) ≤ ⊥
⊢ False
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep t → Disjoint (t i) (t j)

pp: case mpr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (t i) (t j) → iSupIndep t

Tactic:
·

Goal state after:
case mp
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep t → Disjoint (t i) (t j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (t i) (t j) → iSupIndep t

Tactic:
·

Goal state after:
case mpr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (t i) (t j) → iSupIndep t
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inl
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
⊢ Disjoint (t k) (⨆ j, ⨆ (_ : j ≠ k), t j)

pp: case mpr.inr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
⊢ Disjoint (t k) (⨆ j, ⨆ (_ : j ≠ k), t j)

Tactic:
·

Goal state after:
case mpr.inl
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
⊢ Disjoint (t k) (⨆ j, ⨆ (_ : j ≠ k), t j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
⊢ Disjoint (t k) (⨆ j, ⨆ (_ : j ≠ k), t j)

Tactic:
·

Goal state after:
case mpr.inr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
⊢ Disjoint (t k) (⨆ j, ⨆ (_ : j ≠ k), t j)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id) →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id) →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id) →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
intro hk s hne hdir hsup
      obtain ⟨t, ht⟩ := hk s hsup
      -- certainly every element of t is below something in s, since ↑t ⊆ s.
      have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
      obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
      exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 0) (f 1 ⊔ f 2)

pp: case refine_2
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 1) (f 0 ⊔ f 2)

pp: case refine_3
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)

pp: case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)

Tactic:
·

Goal state after:
case refine_1
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 0) (f 1 ⊔ f 2)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 1) (f 0 ⊔ f 2)

pp: case refine_3
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)

pp: case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)

Tactic:
·

Goal state after:
case refine_2
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 1) (f 0 ⊔ f 2)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id) → ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s

pp: case mpr
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ (∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s) → ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
·

Goal state after:
case mp
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id) → ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_3
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)

pp: case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)

Tactic:
·

Goal state after:
case refine_3
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)

Tactic:
·

Goal state after:
case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mpr
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ (∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s) → ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
·

Goal state after:
case mpr
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ (∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s) → ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ y ≤ t.sup id

pp: case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ t.sup id ≤ sSup s

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ y ≤ t.sup id
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ t.sup id ≤ sSup s

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ t.sup id ≤ sSup s
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : ¬a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : ¬a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
·

Goal state after:
case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : ¬a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x

pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : ¬x ∈ s
⊢ 1 = 1

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ∅.sup id
⊢ sSup s ∈ s

pp: case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ∅.sup id
⊢ sSup s ∈ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s

Tactic:
·

Goal state after:
case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

pp: case refine_2
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
tfae_1_to_2 : WellFoundedGT α → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFoundedGT α
tfae_2_iff_4 : IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_1
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ 0 • y ∈ span R (s • t)

pp: case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ ∀ (x y_1 : S),
    x ∈ span R s → y_1 ∈ span R s → x • y ∈ span R (s • t) → y_1 • y ∈ span R (s • t) → (x + y_1) • y ∈ span R (s • t)

pp: case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ ∀ (a : R), ∀ x ∈ span R s, x • y ∈ span R (s • t) → (a • x) • y ∈ span R (s • t)

Tactic:
·

Goal state after:
case refine_1
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ 0 • y ∈ span R (s • t)
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: case pos
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = ∏ i ∈ s, f i

pp: case neg
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ¬∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0

Tactic:
·

Goal state after:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = ∏ i ∈ s, f i
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: case neg
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ¬∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0

Tactic:
·

Goal state after:
case neg
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ¬∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0