awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
rw rw₁ rw₂ :
  iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
rw₃ :
  ∀ (a : ι) (b : a ∈ s),
    Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
        (⨆ (j : ↥s),
          ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
      Disjoint (f a) ((s.erase a).sup f)
rw₄ :
  ∀ (a : ι) (b : a ∈ s),
    Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
        (⨆ (j : ↥s),
          ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
      Disjoint (f a) (⨆ a_1 ∈ s.erase a, f a_1)
a :
  ∀ (a : ι) (b : a ∈ s),
    Eq.{u_1 + 1} (α := α)
      (⨆ (j : ↥s),
        ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j)
      (⨆ a_1 ∈ s.erase a, f a_1)
a₁ :
  ∀ (a : ι) (b : a ∈ s),
    Eq.{u_1 + 1} (α := α)
      (⨆ (i : ι),
        ⨆ (h : i ∈ s),
          ⨆ (_ : Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b),
            (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h))
      (⨆ a_1 ∈ s.erase a, f a_1)
⊢ iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ s.SupIndep f
have a₂ : ∀ (a : ι) (b : a ∈ s),
  Eq (α := ι → α)
    (fun (i : ι) ↦
      ⨆ (h : i ∈ s),
        ⨆ (_ : Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b),
          (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h))
    fun (a_1 : ι) ↦ ⨆ (_ : a_1 ∈ s.erase a), f a_1
Tactic: classical
    rw [Finset.supIndep_iff_disjoint_erase]
    refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
    rw [Finset.sup_eq_iSup]
    congr! 1
    refine iSup_subtype.trans ?_
    congr! 1
    simp [iSup_and, @iSup_comm _ (_ ∈ s)]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₁ : iSupIndep g
h₂ : iSup f = ⊤
⊢ f ≤ g ↔ f = g
have refine : ∀ (h₃ : f ≤ g) (i : ι), f i = g i
Tactic: refine ⟨fun h₃ ↦ funext fun i ↦ ?_, le_of_eq⟩
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₁ : iSupIndep g
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
⊢ f i = g i
have h₄ : Disjoint (⨆ (j : ι), ⨆ (_ : j ≠ i), f j) (g i)
Tactic: replace h₁ : Disjoint (⨆ (j) (_ : j ≠ i), f j) (g i) :=
    Disjoint.mono_left (iSup₂_mono fun j _ ↦ h₃ j) (h₁ i).symm
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ (j : ι), ⨆ (_ : j ≠ i), f j) (g i)
⊢ Codisjoint (f i) (⨆ (j : ι), ⨆ (_ : j ≠ i), f j)
have rw : f i ⊔ ⨆ (j : ι), ⨆ (_ : j ≠ i), f j = ⊤
Tactic: rw [codisjoint_iff, ← iSup_split_single f i, h₂]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ (j : ι), ⨆ (_ : j ≠ i), f j) (g i)
rw : f i ⊔ ⨆ (j : ι), ⨆ (_ : j ≠ i), f j = ⊤
rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) ⊤
⊢ Codisjoint (f i) (⨆ (j : ι), ⨆ (_ : j ≠ i), f j)
have rw₂ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
Tactic: rw [codisjoint_iff, ← iSup_split_single f i, h₂]
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ (j : ι), ⨆ (_ : j ≠ i), f j) (g i)
⊢ f i = g i
have h₄ : Codisjoint (f i) (⨆ (j : ι), ⨆ (_ : j ≠ i), f j)
Tactic: replace h₂ : Codisjoint (f i) (⨆ (j) (_ : j ≠ i), f j) := by
    rw [codisjoint_iff, ← iSup_split_single f i, h₂]
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
this : ∀ (s : Finset ι) (hst : Disjoint (↑s : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
have this₁ : ∀ (hst : Disjoint (↑(hs.toFinset (s := s)) : Set ι) t),
  Disjoint.{u_1} (α := α) (⨆ i ∈ hs.toFinset (s := s), f i) (⨆ i ∈ t, f i)
Tactic: specialize this hs.toFinset
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
have suffices : ∀ (s : Finset ι) (hst : Disjoint (↑s : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
Tactic: suffices ∀ (s : Finset ι) (hst : Disjoint ↑s t), Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i) by
    specialize this hs.toFinset
    aesop
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hst : Disjoint (↑(insert j s₀) : Set ι) t
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)
have hjt : j ∉ t
Tactic: have hjt : j ∉ t := by aesop
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hst : Disjoint (↑(insert j s₀) : Set ι) t
hjt : j ∉ t
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)
have hst₁ : Disjoint (↑s₀ : Set ι) (insert j t)
Tactic: replace hst : Disjoint ↑s₀ (insert j t) := by aesop
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
⊢ Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
have ih₁ : Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ insert j t, f i)
Tactic: specialize ih hst
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ insert j t, f i)
⊢ Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
have rwa : ∀ (ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ x ∈ t, f x)), Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
Tactic: rwa [iSup_insert] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)
have ih₁ : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
Tactic: replace ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i) := by
      specialize ih hst
      rwa [iSup_insert] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
⊢ Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ (↑s₀ : Set ι), f i)
have rw : Disjoint (f j) (⨆ x ∈ t ∪ (↑s₀ : Set ι), f x)
Tactic: rw [← iSup_union]
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)
have this : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ (↑s₀ : Set ι), f i)
Tactic: have : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ (⨆ i ∈ (s₀ : Set ι), f i)) := by
      rw [← iSup_union]
      exact disjoint_biSup hf <| by aesop
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
this : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ (↑s₀ : Set ι), f i)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)
have insert : Disjoint (⨆ i ∈ t, f i) ((⨆ x ∈ s₀, f x) ⊔ f j)
Tactic: rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
hst : Disjoint (↑s : Set ι) t
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
have empty : ∀ {t : Set ι} (hst : Disjoint (↑∅ : Set ι) t),
  Disjoint.{u_1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) (⨆ i ∈ t, f i)
Tactic: induction s using Finset.induction_on generalizing t with
  | empty => simp
  | insert j s₀ hj ih =>
    have hjt : j ∉ t := by aesop
    replace hst : Disjoint ↑s₀ (insert j t) := by aesop
    replace ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i) := by
      specialize ih hst
      rwa [iSup_insert] at ih
    have : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ (⨆ i ∈ (s₀ : Set ι), f i)) := by
      rw [← iSup_union]
      exact disjoint_biSup hf <| by aesop
    rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]
    exact disjoint_sup_right_of_disjoint_sup_right ih this
Cleared hypotheses: t, s, hst
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
hst : Disjoint (↑s : Set ι) t
empty :
  ∀ {t : Set ι} (hst : Disjoint (↑∅ : Set ι) t),
    Disjoint.{u_1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) (⨆ i ∈ t, f i)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
have insert : ∀ (j : ι) (s₀ : Finset ι) (hj : j ∉ s₀)
  (ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i))
  {t : Set ι} (hst : Disjoint (↑(insert j s₀) : Set ι) t),
  Disjoint.{u_1} (α := α) (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)
Tactic: induction s using Finset.induction_on generalizing t with
  | empty => simp
  | insert j s₀ hj ih =>
    have hjt : j ∉ t := by aesop
    replace hst : Disjoint ↑s₀ (insert j t) := by aesop
    replace ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i) := by
      specialize ih hst
      rwa [iSup_insert] at ih
    have : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ (⨆ i ∈ (s₀ : Set ι), f i)) := by
      rw [← iSup_union]
      exact disjoint_biSup hf <| by aesop
    rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]
    exact disjoint_sup_right_of_disjoint_sup_right ih this
Cleared hypotheses: t, s, hst
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
hst : Disjoint (↑s : Set ι) t
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
have empty : ∀ {t : Set ι} (hst : Disjoint (↑∅ : Set ι) t),
  Disjoint.{u_1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) (⨆ i ∈ t, f i)
Tactic: classical
  induction s using Finset.induction_on generalizing t with
  | empty => simp
  | insert j s₀ hj ih =>
    have hjt : j ∉ t := by aesop
    replace hst : Disjoint ↑s₀ (insert j t) := by aesop
    replace ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i) := by
      specialize ih hst
      rwa [iSup_insert] at ih
    have : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ (⨆ i ∈ (s₀ : Set ι), f i)) := by
      rw [← iSup_union]
      exact disjoint_biSup hf <| by aesop
    rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]
    exact disjoint_sup_right_of_disjoint_sup_right ih this
Cleared hypotheses: t, s, hst
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
hst : Disjoint (↑s : Set ι) t
empty :
  ∀ {t : Set ι} (hst : Disjoint (↑∅ : Set ι) t),
    Disjoint.{u_1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) (⨆ i ∈ t, f i)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
have insert : ∀ (j : ι) (s₀ : Finset ι) (hj : j ∉ s₀)
  (ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i))
  {t : Set ι} (hst : Disjoint (↑(insert j s₀) : Set ι) t),
  Disjoint.{u_1} (α := α) (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)
Tactic: classical
  induction s using Finset.induction_on generalizing t with
  | empty => simp
  | insert j s₀ hj ih =>
    have hjt : j ∉ t := by aesop
    replace hst : Disjoint ↑s₀ (insert j t) := by aesop
    replace ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i) := by
      specialize ih hst
      rwa [iSup_insert] at ih
    have : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ (⨆ i ∈ (s₀ : Set ι), f i)) := by
      rw [← iSup_union]
      exact disjoint_biSup hf <| by aesop
    rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]
    exact disjoint_sup_right_of_disjoint_sup_right ih this
Cleared hypotheses: t, s, hst
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set ι
h₁ : iSupIndep f
h₂ : Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : f i ≠ ⊥
⊢ i ∈ s
have by_contra : ∀ (contra : i ∉ s), False
Tactic: by_contra contra
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set ι
h₁ : iSupIndep f
h₂ : Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : f i ≠ ⊥
contra : i ∉ s
⊢ False
have h₃ : Disjoint (f i) (⨆ i ∈ s, f i)
Tactic: replace h₁ : Disjoint (f i) (⨆ i ∈ s, f i) := (h₁ i).mono_right <| biSup_mono <| by aesop
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
⊢ a ∆ a = ⊥
have rw : a \ a ⊔ a \ a = ⊥
Tactic: rw [symmDiff, sup_idem, sdiff_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
rw : a \ a ⊔ a \ a = ⊥
⊢ a ∆ a = ⊥
have rw₁ : a \ a = ⊥
Tactic: rw [symmDiff, sup_idem, sdiff_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
rw : a \ a ⊔ a \ a = ⊥
rw₁ : a \ a = ⊥
⊢ a ∆ a = ⊥
have rw₂ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
Tactic: rw [symmDiff, sup_idem, sdiff_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
⊢ a ∆ ⊥ = a
have rw : a \ ⊥ ⊔ ⊥ \ a = a
Tactic: rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
rw : a \ ⊥ ⊔ ⊥ \ a = a
⊢ a ∆ ⊥ = a
have rw₁ : a ⊔ ⊥ \ a = a
Tactic: rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
rw : a \ ⊥ ⊔ ⊥ \ a = a
rw₁ : a ⊔ ⊥ \ a = a
⊢ a ∆ ⊥ = a
have rw₂ : a ⊔ ⊥ = a
Tactic: rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
rw : a \ ⊥ ⊔ ⊥ \ a = a
rw₁ : a ⊔ ⊥ \ a = a
rw₂ : a ⊔ ⊥ = a
⊢ a ∆ ⊥ = a
have rw₃ : a = a
Tactic: rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
⊢ ⊥ ∆ a = a
have rw : a ∆ ⊥ = a
Tactic: rw [symmDiff_comm, symmDiff_bot]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
rw : a ∆ ⊥ = a
⊢ ⊥ ∆ a = a
have rw₁ : a = a
Tactic: rw [symmDiff_comm, symmDiff_bot]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = ⊥ ↔ a = b
have simp_rw : a \ b ⊔ b \ a = ⊥ ↔ a = b
Tactic: simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
simp_rw : a \ b ⊔ b \ a = ⊥ ↔ a = b
⊢ a ∆ b = ⊥ ↔ a = b
have simp_rw₁ : a \ b = ⊥ ∧ b \ a = ⊥ ↔ a = b
Tactic: simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
simp_rw : a \ b ⊔ b \ a = ⊥ ↔ a = b
simp_rw₁ : a \ b = ⊥ ∧ b \ a = ⊥ ↔ a = b
⊢ a ∆ b = ⊥ ↔ a = b
have simp_rw₂ : a ≤ b ∧ b ≤ a ↔ a = b
Tactic: simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : a ≤ b
⊢ a ∆ b = b \ a
have rw : a \ b ⊔ b \ a = b \ a
Tactic: rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : a ≤ b
rw : a \ b ⊔ b \ a = b \ a
⊢ a ∆ b = b \ a
have rw₁ : ⊥ ⊔ b \ a = b \ a
Tactic: rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : a ≤ b
rw : a \ b ⊔ b \ a = b \ a
rw₁ : ⊥ ⊔ b \ a = b \ a
⊢ a ∆ b = b \ a
have rw₂ : b \ a = b \ a
Tactic: rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ a ∆ b = a \ b
have rw : a \ b ⊔ b \ a = a \ b
Tactic: rw [symmDiff, sdiff_eq_bot_iff.2 h, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
rw : a \ b ⊔ b \ a = a \ b
⊢ a ∆ b = a \ b
have rw₁ : a \ b ⊔ ⊥ = a \ b
Tactic: rw [symmDiff, sdiff_eq_bot_iff.2 h, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
rw : a \ b ⊔ b \ a = a \ b
rw₁ : a \ b ⊔ ⊥ = a \ b
⊢ a ∆ b = a \ b
have rw₂ : a \ b = a \ b
Tactic: rw [symmDiff, sdiff_eq_bot_iff.2 h, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
have simp_rw : a \ b ⊔ b \ a ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
Tactic: simp_rw [symmDiff, sup_le_iff, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
simp_rw : a \ b ⊔ b \ a ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
⊢ a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
have simp_rw₁ : a \ b ≤ c ∧ b \ a ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
Tactic: simp_rw [symmDiff, sup_le_iff, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a ∆ b = a ⊔ b
have rw : a \ b ⊔ b \ a = a ⊔ b
Tactic: rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ b ⊔ b \ a = a ⊔ b
⊢ a ∆ b = a ⊔ b
have rw₁ : a ⊔ b \ a = a ⊔ b
Tactic: rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ b ⊔ b \ a = a ⊔ b
rw₁ : a ⊔ b \ a = a ⊔ b
⊢ a ∆ b = a ⊔ b
have rw₂ : a ⊔ b = a ⊔ b
Tactic: rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
have rw : (a \ b ⊔ b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
Tactic: rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : (a \ b ⊔ b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
⊢ a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
have rw₁ : (a \ b) \ c ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
Tactic: rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : (a \ b ⊔ b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
rw₁ : (a \ b) \ c ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
⊢ a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
have rw₂ : a \ (b ⊔ c) ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
Tactic: rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : (a \ b ⊔ b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
rw₁ : (a \ b) \ c ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
rw₂ : a \ (b ⊔ c) ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
⊢ a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
have rw₃ : a \ (b ⊔ c) ⊔ b \ (a ⊔ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
Tactic: rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b \ (a ⊓ b) = a ∆ b
have rw : a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b
Tactic: rw [symmDiff_sdiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ (b \ a) = a ⊔ b
have rw : a \ (b \ a) ⊔ b \ a = a ⊔ b
Tactic: rw [symmDiff, sdiff_idem]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a \ b) ∆ b = a ⊔ b
have rw : b ∆ (a \ b) = a ⊔ b
Tactic: rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : b ∆ (a \ b) = a ⊔ b
⊢ (a \ b) ∆ b = a ⊔ b
have rw₁ : b ⊔ a = a ⊔ b
Tactic: rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : b ∆ (a \ b) = a ⊔ b
rw₁ : b ⊔ a = a ⊔ b
⊢ (a \ b) ∆ b = a ⊔ b
have rw₂ : a ⊔ b = a ⊔ b
Tactic: rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b
have refine : a ⊔ b ≤ a ∆ b ⊔ a ⊓ b
Tactic: refine le_antisymm (sup_le symmDiff_le_sup inf_le_sup) ?_
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ a ∆ b ⊔ a ⊓ b
have rw : a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
Tactic: rw [sup_inf_left, symmDiff]