mathlib-initiative/mathlib-tactics huggingface dataset:
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✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ Bool.casesOn x ⊥ ⊤) ((fun x ↦ decide (x = ⊤)) ⊥) = ⊥

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✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ Bool.casesOn x ⊥ ⊤) ((fun x ↦ decide (x = ⊤)) ⊤) = ⊤

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✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ Bool.casesOn x ⊥ ⊤) ((fun x ↦ decide (x = ⊤)) ⊥) = ⊥

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✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ Bool.casesOn x ⊥ ⊤) ((fun x ↦ decide (x = ⊤)) ⊤) = ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case false
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ decide (x = ⊤)) ((fun x ↦ Bool.casesOn x ⊥ ⊤) false) = false

pp: case true
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ decide (x = ⊤)) ((fun x ↦ Bool.casesOn x ⊥ ⊤) true) = true

Tactic:
<;>

Goal state after:
case false
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ decide (x = ⊤)) ((fun x ↦ Bool.casesOn x ⊥ ⊤) false) = false

case true
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ decide (x = ⊤)) ((fun x ↦ Bool.casesOn x ⊥ ⊤) true) = true
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 ⊥

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.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 α
y : α
⊢ (if ⊥ = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = ⊥ ⊓ if y = ⊥ 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 α
y : α
⊢ (if ⊤ = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = ⊤ ⊓ if y = ⊥ 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 α
y : α
⊢ (if ⊥ = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = ⊥ ⊓ if y = ⊥ then ⊤ else ⊥

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 α
y : α
⊢ (if ⊤ = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = ⊤ ⊓ if y = ⊥ then ⊤ else ⊥
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1
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
⊢ span R (range (update v j (v j + r • v i))) ≤ span R (range v)

pp: case refine_2
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
⊢ span R (range v) ≤ span R (range (update v j (v j + r • v i)))

Tactic:
<;>

Goal state after:
case refine_1
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
⊢ span R (range (update v j (v j + r • v i))) ≤ span R (range v)

case refine_2
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
⊢ span R (range v) ≤ span R (range (update v j (v j + r • v i)))
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1
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
⊢ ∀ (y : ι), update v j (v j + r • v i) y ∈ span R (range v)

pp: case refine_2
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
⊢ ∀ (y : ι), v y ∈ span R (range (update v j (v j + r • v i)))

Tactic:
<;>

Goal state after:
case refine_1
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
⊢ ∀ (y : ι), update v j (v j + r • v i) y ∈ span R (range v)

case refine_2
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
⊢ ∀ (y : ι), v y ∈ span R (range (update v j (v j + r • v i)))
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1
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 : ι
⊢ update v j (v j + r • v i) k ∈ span R (range v)

pp: case refine_2
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 : ι
⊢ v k ∈ span R (range (update v j (v j + r • v i)))

Tactic:
<;>

Goal state after:
case refine_1
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 : ι
⊢ update v j (v j + r • v i) k ∈ span R (range v)

case refine_2
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 : ι
⊢ v k ∈ span R (range (update v j (v j + r • v i)))
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Iic b ↔ x ∈ Iic (e.symm b)

Tactic:
simp [← e.le_iff_le]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
i : ι
hi : i ∈ image g s
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
hit : i ∉ image g t
⊢ Disjoint (f i) ((image g t).sup f)

Tactic:
rcases mem_image.mp hi with ⟨i, his, rfl⟩

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) ((image g t).sup f)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case mp
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∃ a, ⊤ = R ∙ a) → ∃ a, p = R ∙ a

pp: case mpr
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∃ a, p = R ∙ a) → ∃ a, ⊤ = R ∙ a

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∃ a, ⊤ = R ∙ a) → ∃ a, p = R ∙ a

case mpr
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∃ a, p = R ∙ a) → ∃ a, ⊤ = R ∙ a
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (map g s).SupIndep f

Tactic:
classical
    rw [map_eq_image]
    exact hs.image

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1.hu
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
u : Finset ((x : ι) × β x) := ⋯
v : Finset ((x : ι) × β x) := ⋯
⊢ u ⊆ s.sigma g

pp: case refine_1.hv
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
u : Finset ((x : ι) × β x) := ⋯
v : Finset ((x : ι) × β x) := ⋯
⊢ v ⊆ s.sigma g

pp: case refine_1.huv
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
u : Finset ((x : ι) × β x) := ⋯
v : Finset ((x : ι) × β x) := ⋯
⊢ Disjoint u v

Tactic:
<;>

Goal state after:
case refine_1.hu
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
u : Finset ((x : ι) × β x) := ⋯
v : Finset ((x : ι) × β x) := ⋯
⊢ u ⊆ s.sigma g

case refine_1.hv
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
u : Finset ((x : ι) × β x) := ⋯
v : Finset ((x : ι) × β x) := ⋯
⊢ v ⊆ s.sigma g

case refine_1.huv
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
u : Finset ((x : ι) × β x) := ⋯
v : Finset ((x : ι) × β x) := ⋯
⊢ Disjoint u v
Module: Mathlib.Order.CompactlyGenerated.Basic

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

Tactic:
obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ t.sup id
t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y
x : α
hxs : x ∈ s
hsupx : t.sup id ≤ x
⊢ ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_4.«0»
α : 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)
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 ((fun i ↦ i) ⟨0, ⋯⟩)) (⨆ j, ⨆ (_ : j ≠ (fun i ↦ i) ⟨0, ⋯⟩), f j)

pp: case refine_4.«1»
α : 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)
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 ((fun i ↦ i) ⟨1, ⋯⟩)) (⨆ j, ⨆ (_ : j ≠ (fun i ↦ i) ⟨1, ⋯⟩), f j)

pp: case refine_4.«2»
α : 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)
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 ((fun i ↦ i) ⟨2, ⋯⟩)) (⨆ j, ⨆ (_ : j ≠ (fun i ↦ i) ⟨2, ⋯⟩), f j)

Tactic:
<;>

Goal state after:
case refine_4.«0»
α : 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)
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 ((fun i ↦ i) ⟨0, ⋯⟩)) (⨆ j, ⨆ (_ : j ≠ (fun i ↦ i) ⟨0, ⋯⟩), f j)

case refine_4.«1»
α : 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)
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 ((fun i ↦ i) ⟨1, ⋯⟩)) (⨆ j, ⨆ (_ : j ≠ (fun i ↦ i) ⟨1, ⋯⟩), f j)

case refine_4.«2»
α : 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)
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 ((fun i ↦ i) ⟨2, ⋯⟩)) (⨆ j, ⨆ (_ : j ≠ (fun i ↦ i) ⟨2, ⋯⟩), f j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
ih : Disjoint (⨆ i ∈ s₀, f i) (⨆ i ∈ insert j t, f i)
hjt : j ∉ t
hst : Disjoint (↑s₀) (insert j t)
⊢ Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)

Tactic:
iSup_insert

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ x ∈ t, f x)
hjt : j ∉ t
hst : Disjoint (↑s₀) (insert j t)
⊢ Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
h✝ : a ∈ s
⊢ s.mulIndicator f a = t.mulIndicator g b

pp: case neg
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
h✝ : ¬a ∈ s
⊢ s.mulIndicator f a = t.mulIndicator g b

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
h✝ : a ∈ s
⊢ s.mulIndicator f a = t.mulIndicator g b

case neg
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
h✝ : ¬a ∈ s
⊢ s.mulIndicator f a = t.mulIndicator g b
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : x ∈ t
h✝ : x ∈ s ∩ t
⊢ f x = f x

pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : x ∈ t
h✝ : ¬x ∈ s ∩ t
⊢ f x = 1

pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : ¬x ∈ t
h✝ : x ∈ s ∩ t
⊢ 1 = f x

pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : ¬x ∈ t
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1

pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : x ∈ s ∩ t
⊢ 1 = f x

pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : x ∈ t
h✝ : x ∈ s ∩ t
⊢ f x = f x

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : x ∈ t
h✝ : ¬x ∈ s ∩ t
⊢ f x = 1

case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : ¬x ∈ t
h✝ : x ∈ s ∩ t
⊢ 1 = f x

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : ¬x ∈ t
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1

case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : x ∈ s ∩ t
⊢ 1 = f x

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
h✝ : x✝ ∈ s
⊢ (g ∘ f) x✝ = (g ∘ s.mulIndicator f) x✝

pp: case neg
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = (g ∘ s.mulIndicator f) x✝

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
h✝ : x✝ ∈ s
⊢ (g ∘ f) x✝ = (g ∘ s.mulIndicator f) x✝

case neg
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = (g ∘ s.mulIndicator f) x✝
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
a : α
f : α → β → M
b : β
h : a ∈ s
⊢ s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a

pp: case neg
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
a : α
f : α → β → M
b : β
h : ¬a ∈ s
⊢ s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
a : α
f : α → β → M
b : β
h : a ∈ s
⊢ s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a

case neg
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
a : α
f : α → β → M
b : β
h : ¬a ∈ s
⊢ s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
h✝ : 1 ∈ s
⊢ univ ∈ {univ, ∅}

pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
h✝ : ¬1 ∈ s
⊢ ∅ ∈ {univ, ∅}

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
h✝ : 1 ∈ s
⊢ univ ∈ {univ, ∅}

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
h✝ : ¬1 ∈ s
⊢ ∅ ∈ {univ, ∅}
Module: Mathlib.Order.CompactlyGenerated.Basic

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

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

Tactic:
<;>

Goal state after:
case a
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ sSup s ≤ t.sup id

case a
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ 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
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : a ∈ s
h✝ : 1 ∈ s
⊢ U.ite univ univ = U ∪ Uᶜ

pp: case neg
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : a ∈ s
h✝ : ¬1 ∈ s
⊢ U.ite univ ∅ = U ∪ ∅

pp: case pos
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : ¬a ∈ s
h✝ : 1 ∈ s
⊢ U.ite ∅ univ = ∅ ∪ Uᶜ

pp: case neg
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : ¬a ∈ s
h✝ : ¬1 ∈ s
⊢ U.ite ∅ ∅ = ∅ ∪ ∅

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : a ∈ s
h✝ : 1 ∈ s
⊢ U.ite univ univ = U ∪ Uᶜ

case neg
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : a ∈ s
h✝ : ¬1 ∈ s
⊢ U.ite univ ∅ = U ∪ ∅

case pos
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : ¬a ∈ s
h✝ : 1 ∈ s
⊢ U.ite ∅ univ = ∅ ∪ Uᶜ

case neg
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : ¬a ∈ s
h✝ : ¬1 ∈ s
⊢ U.ite ∅ ∅ = ∅ ∪ ∅
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : a ∈ s
h✝ : 1 ∈ s
⊢ U ∪ Uᶜ ∈ {univ, U, Uᶜ, ∅}

pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : a ∈ s
h✝ : ¬1 ∈ s
⊢ U ∪ ∅ ∈ {univ, U, Uᶜ, ∅}

pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : ¬a ∈ s
h✝ : 1 ∈ s
⊢ ∅ ∪ Uᶜ ∈ {univ, U, Uᶜ, ∅}

pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : ¬a ∈ s
h✝ : ¬1 ∈ s
⊢ ∅ ∪ ∅ ∈ {univ, U, Uᶜ, ∅}

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : a ∈ s
h✝ : 1 ∈ s
⊢ U ∪ Uᶜ ∈ {univ, U, Uᶜ, ∅}

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : a ∈ s
h✝ : ¬1 ∈ s
⊢ U ∪ ∅ ∈ {univ, U, Uᶜ, ∅}

case pos
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : ¬a ∈ s
h✝ : 1 ∈ s
⊢ ∅ ∪ Uᶜ ∈ {univ, U, Uᶜ, ∅}

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : ¬a ∈ s
h✝ : ¬1 ∈ s
⊢ ∅ ∪ ∅ ∈ {univ, U, Uᶜ, ∅}