awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
s : Set α
simp_rw :
  (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ a_2 ∈ s \ {a}, a_2)) ↔
    ∀ (x : α) (h : x ∈ s),
      Disjoint x (⨆ (j : { x : α // x ∈ s }), ⨆ (_ : j ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h), (↑j : α))
⊢ sSupIndep s ↔ iSupIndep.{u_5 + 1, u_5} (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
simp_rw [iSupIndep, sSupIndep, SetCoe.forall, sSup_eq_iSup]

Premises used: sSupIndep, iSupIndep, sSup_eq_iSup, SetCoe.forall
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ a_2 ∈ s \ {a}, a_2)) ↔
    ∀ (x : α) (h : x ∈ s),
      Disjoint x (⨆ (j : { x : α // x ∈ s }), ⨆ (_ : j ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h), (↑j : α))

Tactic:
forall₂_congr fun a ha => ?_

Premises used: forall₂_congr
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
s : Set α
refine :
  ∀ (a : α) (ha : a ∈ s),
    Disjoint a (⨆ a_1 ∈ s \ {a}, a_1) ↔
      Disjoint a (⨆ (j : { x : α // x ∈ s }), ⨆ (_ : j ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha), (↑j : α))
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ a_2 ∈ s \ {a}, a_2)) ↔
    ∀ (x : α) (h : x ∈ s),
      Disjoint x (⨆ (j : { x : α // x ∈ s }), ⨆ (_ : j ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h), (↑j : α))

Tactic:
refine forall₂_congr fun a ha => ?_

Premises used: forall₂_congr
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
s : Set α
a : α
ha : a ∈ s
⊢ Disjoint a (⨆ a_1 ∈ s \ {a}, a_1) ↔
    Disjoint a (⨆ (j : { x : α // x ∈ s }), ⨆ (_ : j ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha), (↑j : α))

Tactic:
simp [iSup_subtype, iSup_and]

Premises used: iSup_subtype, iSup_and
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)

Tactic:
Iff.rfl

Premises used: iSupIndep, Iff.rfl
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
simp_rw :
  iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (⨆ (a : ι), ⨆ (_ : Membership.mem (γ := Set ι) {j : ι | j ≠ i} a), t a)
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j : ι | j ≠ i}))

Tactic:
simp_rw [sSup_image]

Premises used: sSup_image
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (⨆ (a : ι), ⨆ (_ : Membership.mem (γ := Set ι) {j : ι | j ≠ i} a), t a)

Tactic:
rfl
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
rw :
  (∀ (i : ι), Disjoint (t i) (sSup (t '' {j : ι | j ≠ i}))) ↔
    ∀ (i : ι), Disjoint (t i) (sSup {a : α | ∃ (j : ι), j ≠ i ∧ t j = a})
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a : α | ∃ (j : ι), j ≠ i ∧ t j = a})

Tactic:
rw [iSupIndep_def']

Premises used: iSupIndep_def'
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
⊢ (∀ (i : ι), Disjoint (t i) (sSup (t '' {j : ι | j ≠ i}))) ↔
    ∀ (i : ι), Disjoint (t i) (sSup {a : α | ∃ (j : ι), j ≠ i ∧ t j = a})

Tactic:
aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : Subsingleton ι
t : ι → α
i : ι
⊢ Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)

Tactic:
simp [← Subsingleton.elim i]

Premises used: Subsingleton.elim
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ Pairwise (Disjoint on t)

Tactic:
fun x y h =>
  disjoint_sSup_right (ht x) ⟨y, iSup_pos h.symm⟩

Premises used: iSup_pos, Ne.symm, disjoint_sSup_right, Pairwise, Exists.intro
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s t : ι → α
hs : iSupIndep s
hst : t ≤ s
⊢ iSupIndep t

Tactic:
fun i => (hs i).mono (hst i) <| iSup₂_mono fun j _ => hst j

Premises used: iSup₂_mono, iSupIndep, Disjoint.mono
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep t
hf : Injective f
i : ι'
⊢ LE.le.{u_1} (α := α) (⨆ (j : ι'), ⨆ (_ : j ≠ i), (t ∘ f) j) (⨆ (j : ι), ⨆ (_ : j ≠ f i), t j)

Tactic:
(iSup_mono fun i => ?_).trans (iSup_comp_le _ f)

Premises used: LE.le.trans, iSup_comp_le, iSup_mono
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep t
hf : Injective f
i : ι'
refine : ∀ (i_1 : ι'), LE.le.{u_1} (α := α) (⨆ (_ : i_1 ≠ i), (t ∘ f) i_1) (⨆ (_ : f i_1 ≠ f i), t (f i_1))
⊢ LE.le.{u_1} (α := α) (⨆ (j : ι'), ⨆ (_ : j ≠ i), (t ∘ f) j) (⨆ (j : ι), ⨆ (_ : j ≠ f i), t j)

Tactic:
refine (iSup_mono fun i => ?_).trans (iSup_comp_le _ f)

Premises used: LE.le.trans, iSup_comp_le, iSup_mono
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep t
hf : Injective f
i_1 i : ι'
⊢ LE.le.{u_1} (α := α) (⨆ (_ : i ≠ i_1), (t ∘ f) i) (⨆ (_ : f i ≠ f i_1), t (f i))

Tactic:
iSup_const_mono hf.ne

Premises used: Function.Injective.ne, iSup_const_mono
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep t
hf : Injective f
i_1 i : ι'
⊢ LE.le.{u_1} (α := α) (⨆ (_ : i ≠ i_1), (t ∘ f) i) (⨆ (_ : f i ≠ f i_1), t (f i))

Tactic:
exact iSup_const_mono hf.ne

Premises used: Function.Injective.ne, iSup_const_mono
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i : ι
obtain : ∀ (i' : ι'), Disjoint (t (f i')) (⨆ (j : ι), ⨆ (_ : j ≠ f i'), t j)
⊢ Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)

Tactic:
obtain ⟨i', rfl⟩ := hf i

Premises used: rfl
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
rw : Disjoint (t (f i')) (⨆ (x : ι'), ⨆ (_ : f x ≠ f i'), t (f x))
⊢ Disjoint (t (f i')) (⨆ (j : ι), ⨆ (_ : j ≠ f i'), t j)

Tactic:
rw [← hf.iSup_comp]

Premises used: Function.Surjective.iSup_comp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ (x : ι'), ⨆ (_ : f x ≠ f i'), t (f x))

Tactic:
(ht i').mono_right (biSup_mono fun j' hij => mt (congr_arg f) hij)

Premises used: biSup_mono, mt, congr_arg, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ (x : ι'), ⨆ (_ : f x ≠ f i'), t (f x))

Tactic:
exact (ht i').mono_right (biSup_mono fun j' hij => mt (congr_arg f) hij)

Premises used: biSup_mono, mt, congr_arg, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
rw : iSupIndep.{u_1 + 1, u_1} (ι := { x : α // x ∈ range t }) (Subtype.val (p := fun (x : α) ↦ x ∈ range t))
⊢ sSupIndep (range t)

Tactic:
rw [sSupIndep_iff]

Premises used: sSupIndep_iff
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ iSupIndep (Subtype.val (p := fun (x : α) ↦ x ∈ range t) ∘ rangeFactorization t)

Tactic:
rw [← coe_comp_rangeFactorization t] at ht

Premises used: Set.coe_comp_rangeFactorization
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep (Subtype.val (p := fun (x : α) ↦ x ∈ range t) ∘ rangeFactorization t)
⊢ iSupIndep.{u_1 + 1, u_1} (ι := { x : α // x ∈ range t }) (Subtype.val (p := fun (x : α) ↦ x ∈ range t))

Tactic:
ht.comp' rangeFactorization_surjective

Premises used: iSupIndep.comp', Set.rangeFactorization_surjective
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep (Subtype.val (p := fun (x : α) ↦ x ∈ range t) ∘ rangeFactorization t)
⊢ iSupIndep.{u_1 + 1, u_1} (ι := { x : α // x ∈ range t }) (Subtype.val (p := fun (x : α) ↦ x ∈ range t))

Tactic:
exact ht.comp' rangeFactorization_surjective

Premises used: iSupIndep.comp', Set.rangeFactorization_surjective
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
⊢ (iSupIndep.{u_3 + 1, u_1} (α := α) fun (i : { i : ι // t i ≠ ⊥ }) ↦ t (↑i : ι)) ↔ iSupIndep t

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.comp Subtype.val_injective⟩

Premises used: Subtype.val_injective, iSupIndep.comp, Iff.intro
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
refine : ∀ (h : iSupIndep.{u_3 + 1, u_1} (α := α) fun (i : { i : ι // t i ≠ ⊥ }) ↦ t (↑i : ι)), iSupIndep t
⊢ (iSupIndep.{u_3 + 1, u_1} (α := α) fun (i : { i : ι // t i ≠ ⊥ }) ↦ t (↑i : ι)) ↔ iSupIndep t

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.comp Subtype.val_injective⟩
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : iSupIndep.{u_3 + 1, u_1} (α := α) fun (i : { i : ι // t i ≠ ⊥ }) ↦ t (↑i : ι)
⊢ ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))

Tactic:
simp only [iSupIndep_def] at h ⊢

Premises used: iSupIndep_def
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i = ⊥
⊢ Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)

Tactic:
simp [hi]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i ≠ ⊥
⊢ Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)

Tactic:
?_
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
⊢ t i ≠ ⊥

Tactic:
cases eq_or_ne (t i) ⊥ with
  | inl hi => simp [hi]
  | inr hi => ?_

Premises used: Bot.bot, eq_or_ne
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i ≠ ⊥
⊢ Disjoint (t (↑(Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i hi) : ι))
    (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i hi), t (↑j : ι))

Tactic:
h ⟨i, hi⟩

Premises used: Subtype.mk
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i ≠ ⊥
h₁ :
  Eq.{u_1 + 1} (α := α) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)
    (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i hi), t (↑j : ι))
⊢ Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)

Tactic:
convert! h ⟨i, hi⟩

Premises used: Subtype.mk
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i ≠ ⊥
j : ι
⊢ Eq.{u_1 + 1} (α := α) (⨆ (_ : t j = ⊥), t j) ⊥

Tactic:
simp only [iSup_eq_bot, imp_self]

Premises used: imp_self, iSup_eq_bot
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i ≠ ⊥
⊢ ∀ (j : ι), Eq.{u_1 + 1} (α := α) (⨆ (_ : t j = ⊥), t j) ⊥

Tactic:
have : ∀ j, ⨆ (_ : t j = ⊥), t j = ⊥ := fun j ↦ by simp only [iSup_eq_bot, imp_self]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), Eq.{u_1 + 1} (α := α) (⨆ (_ : t j = ⊥), t j) ⊥
h₁ :
  Eq.{u_1 + 1} (α := α)
    ((⨆ (i_1 : ι), ⨆ (_ : t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1) ⊔ ⨆ (i_1 : ι), ⨆ (_ : ¬t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1)
    (⨆ (i_1 : ι),
      ⨆ (h : t i_1 ≠ ⊥),
        ⨆ (_ :
          Ne (α := { i : ι // t i ≠ ⊥ }) (Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i_1 h)
            (Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i hi)),
          t (↑(Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i_1 h) : ι))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)
    (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i hi), t (↑j : ι))

Tactic:
rw [iSup_split _ (fun j ↦ t j = ⊥), iSup_subtype]

Premises used: iSup_split, iSup_subtype, Bot.bot, Eq
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), Eq.{u_1 + 1} (α := α) (⨆ (_ : t j = ⊥), t j) ⊥
⊢ Eq.{u_1 + 1} (α := α)
    ((⨆ (i_1 : ι), ⨆ (_ : t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1) ⊔ ⨆ (i_1 : ι), ⨆ (_ : ¬t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1)
    (⨆ (i_1 : ι),
      ⨆ (h : t i_1 ≠ ⊥),
        ⨆ (_ :
          Ne (α := { i : ι // t i ≠ ⊥ }) (Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i_1 h)
            (Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i hi)),
          t (↑(Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i_1 h) : ι))

Tactic:
simp only [iSup_comm (ι' := _ ≠ i), this, ne_eq, sup_of_le_right, Subtype.mk.injEq, iSup_bot,
    bot_le]

Premises used: iSup_comm, ne_eq, sup_of_le_right, Subtype.mk.injEq, bot_le, iSup_bot
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
by_contra! : ∀ (contra : i ≠ j), False
⊢ i = j

Tactic:
by_contra! contra
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
apply : t j = ⊥
⊢ False

Tactic:
apply hj
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ (k : ι), ⨆ (_ : k ≠ i), t k
⊢ Disjoint (t i) (t j)

Tactic:
replace ht := (ht i).mono_right this
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ (k : ι), ⨆ (_ : k ≠ i), t k
ht : Disjoint (t i) (t j)
rwa : ∀ (ht : Disjoint (t j) (t j)), t j = ⊥
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (ht : t j = ⊥), t j = ⊥
⊢ t j = ⊥

Tactic:
rwa [h, disjoint_self] at ht

Premises used: disjoint_self
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
suffices : t j ≤ ⨆ (k : ι), ⨆ (_ : k ≠ i), t k
⊢ t j = ⊥

Tactic:
suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by
    replace ht := (ht i).mono_right this
    rwa [h, disjoint_self] at ht
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ j ≠ i

Tactic:
replace contra : j ≠ i := Ne.symm contra
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : j ≠ i
⊢ t j ≤ ⨆ (k : ι), ⨆ (_ : k ≠ i), t k

Tactic:
le_iSup₂ (f := fun x _ ↦ t x) j contra

Premises used: le_iSup₂
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : j ≠ i
⊢ t j ≤ ⨆ (k : ι), ⨆ (_ : k ≠ i), t k

Tactic:
exact le_iSup₂ (f := fun x _ ↦ t x) j contra

Premises used: le_iSup₂
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₁
b₂ : (i : ι) → β i
hb₂ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₂
h_eq :
  Eq.{u_1 + 1} (α := α) ((fun (b : (i : ι) → β i) ↦ (⨅ (i : ι), t i (b i) : α)) b₁)
    ((fun (b : (i : ι) → β i) ↦ (⨅ (i : ι), t i (b i) : α)) b₂)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b₁ i)) (⨅ (i : ι), t i (b₂ i))

Tactic:
beta_reduce at h_eq
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₁
b₂ : (i : ι) → β i
hb₂ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₂
h_eq : Eq.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b₁ i)) (⨅ (i : ι), t i (b₂ i))
by_contra : ∀ (h_ne : ¬b₁ = b₂), False
⊢ b₁ = b₂

Tactic:
by_contra h_ne
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₁
b₂ : (i : ι) → β i
hb₂ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₂
h_eq : Eq.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b₁ i)) (⨅ (i : ι), t i (b₂ i))
h_ne : ¬b₁ = b₂
⊢ ∃ (i : ι), b₁ i ≠ b₂ i

Tactic:
Function.ne_iff.mp h_ne

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₁
b₂ : (i : ι) → β i
hb₂ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₂
h_eq : Eq.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b₁ i)) (⨅ (i : ι), t i (b₂ i))
h_ne : ¬b₁ = b₂
obtain : ∀ (i : ι) (hi : b₁ i ≠ b₂ i), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ : ∃ i, b₁ i ≠ b₂ i := Function.ne_iff.mp h_ne

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₁
b₂ : (i : ι) → β i
hb₂ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₂
h_eq : Eq.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b₁ i)) (⨅ (i : ι), t i (b₂ i))
h_ne : ¬b₁ = b₂
i : ι
hi : b₁ i ≠ b₂ i
⊢ LE.le.{u_1} (α := α) (⨅ (i : ι), t i (b₁ i)) ⊥

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
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₁
b₂ : (i : ι) → β i
hb₂ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₂
h_eq : Eq.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b₁ i)) (⨅ (i : ι), t i (b₂ i))
h_ne : ¬b₁ = b₂
i : ι
hi : b₁ i ≠ b₂ i
this : LE.le.{u_1} (α := α) (⨅ (i : ι), t i (b₁ i)) ⊥
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
this : Eq.{u_3 + 1} (α := Set ι) univ {i : ι | t i ≠ ⊥}
⊢ Injective t

Tactic:
simpa [← this] using ht.injOn

Premises used: iSupIndep.injOn
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
suffices : Eq.{u_3 + 1} (α := Set ι) univ {i : ι | t i ≠ ⊥}
⊢ Injective t

Tactic:
suffices univ = {i | t i ≠ ⊥} by simpa [← this] using ht.injOn
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ Eq.{u_3 + 1} (α := Set ι) univ {i : ι | t i ≠ ⊥}

Tactic:
simp_all
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
mp : iSupIndep t → Disjoint (t i) (t j)
mpr : Disjoint (t i) (t j) → iSupIndep t
⊢ iSupIndep t ↔ Disjoint (t i) (t j)

Tactic:
constructor
-- Module: Mathlib.Order.SupIndep
Goal:
α : 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)

Tactic:
fun h => h.pairwiseDisjoint hij

Premises used: iSupIndep.pairwiseDisjoint
-- Module: Mathlib.Order.SupIndep
Goal:
α : 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)

Tactic:
exact fun h => h.pairwiseDisjoint hij
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
h : Disjoint (t i) (t j)
k : ι
mpr :
  ∀ (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)
mpr₁ :
  ∀ (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)
⊢ Disjoint (t k) (⨆ (j : ι), ⨆ (_ : j ≠ k), t j)

Tactic:
obtain rfl | rfl := huniv k

Premises used: rfl
-- Module: Mathlib.Order.SupIndep
Goal:
α : 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)

Tactic:
h.mono_right (iSup_le fun i => iSup_le fun hi => Eq.le ?_)

Premises used: Eq.le, iSup_le, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : 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)
mpr : ∀ (i : ι) (hi : i ≠ k), t i = t j
⊢ Disjoint (t k) (⨆ (j : ι), ⨆ (_ : j ≠ k), t j)

Tactic:
refine h.mono_right (iSup_le fun i => iSup_le fun hi => Eq.le ?_)

Premises used: Eq.le, iSup_le, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : 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)
i : ι
hi : i ≠ k
mpr mpr₁ : t j = t j
⊢ t i = t j

Tactic:
rw [(huniv i).resolve_left hi]

Premises used: Or.resolve_left