awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLinearOrder α
f : ι → α
⊢ iSup f = ⊤ ↔ ∀ b < ⊤, ∃ (i : ι), b < f i
have rw : ⊤ ≤ iSup f ↔ ∀ b < ⊤, ∃ (i : ι), b < f i
Tactic: rw [eq_top_iff, le_iSup_iff_forall_lt]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLinearOrder α
f : ι → α
rw : ⊤ ≤ iSup f ↔ ∀ b < ⊤, ∃ (i : ι), b < f i
⊢ iSup f = ⊤ ↔ ∀ b < ⊤, ∃ (i : ι), b < f i
have rw₁ : (∀ b < ⊤, ∃ (i : ι), b < f i) ↔ ∀ b < ⊤, ∃ (i : ι), b < f i
Tactic: rw [eq_top_iff, le_iSup_iff_forall_lt]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Group (goal)
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : CompleteLattice α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
u v : (i : ι) → κ i → α
⊢ ⨆ (i : ι), ⨆ (j : κ i), u i j * v i j ≤
    HMul.hMul (α := α) (⨆ (i : ι), ⨆ (j : κ i), u i j) (⨆ (i : ι), ⨆ (j : κ i), v i j)
have refine : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), u i j * v i j)
  (⨆ (i : ι), HMul.hMul (α := α) (⨆ (j : κ i), u i j) (⨆ (j : κ i), v i j))
Tactic: refine le_trans ?_ (iSup_mul_le ..)
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Group (goal)
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : CompleteLattice α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
u v : (i : ι) → κ i → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), u i j * v i j)
    (⨆ (i : ι), HMul.hMul (α := α) (⨆ (j : κ i), u i j) (⨆ (j : κ i), v i j))
have h : ∀ (i : ι), ⨆ (j : κ i), u i j * v i j ≤ HMul.hMul (α := α) (⨆ (j : κ i), u i j) (⨆ (j : κ i), v i j)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : Bool → α
⊢ ⨆ (b : Bool), f b = f true ⊔ f false
have rw : sSup (range fun (b : Bool) ↦ f b) = f true ⊔ f false
Tactic: rw [iSup, Bool.range_eq, sSup_pair, sup_comm]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : Bool → α
rw : sSup (range fun (b : Bool) ↦ f b) = f true ⊔ f false
⊢ ⨆ (b : Bool), f b = f true ⊔ f false
have rw₁ : sSup {f false, f true} = f true ⊔ f false
Tactic: rw [iSup, Bool.range_eq, sSup_pair, sup_comm]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : Bool → α
rw : sSup (range fun (b : Bool) ↦ f b) = f true ⊔ f false
rw₁ : sSup {f false, f true} = f true ⊔ f false
⊢ ⨆ (b : Bool), f b = f true ⊔ f false
have rw₂ : f false ⊔ f true = f true ⊔ f false
Tactic: rw [iSup, Bool.range_eq, sSup_pair, sup_comm]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : Bool → α
rw : sSup (range fun (b : Bool) ↦ f b) = f true ⊔ f false
rw₁ : sSup {f false, f true} = f true ⊔ f false
rw₂ : f false ⊔ f true = f true ⊔ f false
⊢ ⨆ (b : Bool), f b = f true ⊔ f false
have rw₃ : f true ⊔ f false = f true ⊔ f false
Tactic: rw [iSup, Bool.range_eq, sSup_pair, sup_comm]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
x y : α
⊢ x ⊔ y = ⨆ (b : Bool), bif b then x else y
have rw : x ⊔ y = (bif true then x else y) ⊔ bif false then x else y
Tactic: rw [iSup_bool_eq, Bool.cond_true, Bool.cond_false]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
x y : α
rw : x ⊔ y = (bif true then x else y) ⊔ bif false then x else y
⊢ x ⊔ y = ⨆ (b : Bool), bif b then x else y
have rw₁ : x ⊔ y = x ⊔ bif false then x else y
Tactic: rw [iSup_bool_eq, Bool.cond_true, Bool.cond_false]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
x y : α
rw : x ⊔ y = (bif true then x else y) ⊔ bif false then x else y
rw₁ : x ⊔ y = x ⊔ bif false then x else y
⊢ x ⊔ y = ⨆ (b : Bool), bif b then x else y
have rw₂ : x ⊔ y = x ⊔ y
Tactic: rw [iSup_bool_eq, Bool.cond_true, Bool.cond_false]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i) (⨆ (i : ℕ), u (i + n))
have a : LE.le.{u_1} (α := α) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i) (⨆ (i : ℕ), u (i + n))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
a : LE.le.{u_1} (α := α) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i) (⨆ (i : ℕ), u (i + n))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i) (⨆ (i : ℕ), u (i + n))
have a₁ : LE.le.{u_1} (α := α) (⨆ (i : ℕ), u (i + n)) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ LE.le.{u_1} (α := α) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i) (⨆ (i : ℕ), u (i + n))
have a : ∀ (i : ℕ) (i_1 : i ≥ n), u i ≤ ⨆ (i : ℕ), u (i + n)
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ LE.le.{u_1} (α := α) (⨆ (i : ℕ), u (i + n)) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i)
have a : ∀ (i : ℕ), u (i + n) ≤ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ) (i_1 : i ≥ n), u i ≤ ⨆ (i : ℕ), u (i + n)
have a : ∀ (i : ℕ) (hi : i ≥ n), (fun (i : ℕ) ↦ u (i + n)) (i - n) = u i
Tactic: refine fun i hi => le_sSup ⟨i - n, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ u (i - n + n) = u i
have a : u i = u i
Tactic: rw [Nat.sub_add_cancel hi]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f (i + k)) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i)
have hf : Monotone.{0, u_1} (β := α) fun (n : ℕ) ↦ ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i
Tactic: have hf : Monotone fun n => ⨅ i ≥ n, f i := fun n m h => biInf_mono fun i => h.trans
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone.{0, u_1} (β := α) fun (n : ℕ) ↦ ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i
⊢ Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f (i + k)) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i)
have rw : Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f (i + k)) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n + k), f i)
Tactic: rw [← Monotone.iSup_nat_add hf k]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone.{0, u_1} (β := α) fun (n : ℕ) ↦ ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i
⊢ Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f (i + k)) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n + k), f i)
have simp_rw : Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), ⨅ (i : ℕ), f (i + n + k)) (⨆ (n : ℕ), ⨅ (i : ℕ), f (i + (n + k)))
Tactic: simp_rw [iInf_ge_eq_iInf_nat_add, ← Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x
have rw : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) {0} x), u x) ⊔ ⨆ x ∈ range Nat.succ, u x
Tactic: rw [iSup_union, iSup_singleton, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
rw :
  u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) {0} x), u x) ⊔ ⨆ x ∈ range Nat.succ, u x
⊢ u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x
have rw₁ : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = u 0 ⊔ ⨆ x ∈ range Nat.succ, u x
Tactic: rw [iSup_union, iSup_singleton, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
rw :
  u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) {0} x), u x) ⊔ ⨆ x ∈ range Nat.succ, u x
rw₁ : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = u 0 ⊔ ⨆ x ∈ range Nat.succ, u x
⊢ u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x
have rw₂ : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = u 0 ⊔ ⨆ (i : ℕ), u i.succ
Tactic: rw [iSup_union, iSup_singleton, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x
have rw : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) {0} x), u x) ⊔ ⨆ x ∈ range Nat.succ, u x
Tactic: { rw [iSup_union, iSup_singleton, iSup_range] }
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
rw :
  u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) {0} x), u x) ⊔ ⨆ x ∈ range Nat.succ, u x
⊢ u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x
have rw₁ : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = u 0 ⊔ ⨆ x ∈ range Nat.succ, u x
Tactic: { rw [iSup_union, iSup_singleton, iSup_range] }
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
rw :
  u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) {0} x), u x) ⊔ ⨆ x ∈ range Nat.succ, u x
rw₁ : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = u 0 ⊔ ⨆ x ∈ range Nat.succ, u x
⊢ u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x
have rw₂ : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = u 0 ⊔ ⨆ (i : ℕ), u i.succ
Tactic: { rw [iSup_union, iSup_singleton, iSup_range] }
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ {0} ∪ range Nat.succ, u x) (⨆ (i : ℕ), u i)
have rw : Eq.{u_1 + 1} (α := α) (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) univ x), u x) (⨆ (i : ℕ), u i)
Tactic: rw [Nat.zero_union_range_succ, iSup_univ]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
rw : Eq.{u_1 + 1} (α := α) (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) univ x), u x) (⨆ (i : ℕ), u i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ {0} ∪ range Nat.succ, u x) (⨆ (i : ℕ), u i)
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (x : ℕ), u x) (⨆ (i : ℕ), u i)
Tactic: rw [Nat.zero_union_range_succ, iSup_univ]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨅ (_ : i > 0), f i) (⨅ (i : ℕ), f (i + 1))
have rw : Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨅ (_ : i > 0), f i)
  (⨅ (b : ℕ), ⨅ (_ : Membership.mem (γ := Set ℕ) {i : ℕ | 0 < i} b), f b)
Tactic: rw [← iInf_range, Nat.range_succ]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : CompleteLattice α
s : Set (ULift.{v, u_1} α)
⊢ down.{v, u_1} (sSup s) = ⨆ a ∈ s, a.down
have rw : Eq.{u_1 + 1} (α := α) (down.{v, u_1} (⨆ (a : (↑s : Type (max u_1 v))), (↑a : ULift α))) (⨆ a ∈ s, a.down)
Tactic: rw [sSup_eq_iSup', down_iSup, iSup_subtype'']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : CompleteLattice α
s : Set (ULift.{v, u_1} α)
rw : Eq.{u_1 + 1} (α := α) (down.{v, u_1} (⨆ (a : (↑s : Type (max u_1 v))), (↑a : ULift α))) (⨆ a ∈ s, a.down)
⊢ down.{v, u_1} (sSup s) = ⨆ a ∈ s, a.down
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (i : (↑s : Type (max u_1 v))), down.{v, u_1} (↑i : ULift α)) (⨆ a ∈ s, a.down)
Tactic: rw [sSup_eq_iSup', down_iSup, iSup_subtype'']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : CompleteLattice α
s : Set (ULift.{v, u_1} α)
rw : Eq.{u_1 + 1} (α := α) (down.{v, u_1} (⨆ (a : (↑s : Type (max u_1 v))), (↑a : ULift α))) (⨆ a ∈ s, a.down)
rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (i : (↑s : Type (max u_1 v))), down.{v, u_1} (↑i : ULift α)) (⨆ a ∈ s, a.down)
⊢ down.{v, u_1} (sSup s) = ⨆ a ∈ s, a.down
have rw₂ : Eq.{u_1 + 1} (α := α) (⨆ t ∈ s, t.down) (⨆ a ∈ s, a.down)
Tactic: rw [sSup_eq_iSup', down_iSup, iSup_subtype'']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : CompleteLattice α
s : Set (ULift.{v, u_1} α)
⊢ down.{v, u_1} (sInf s) = ⨅ a ∈ s, a.down
have rw : Eq.{u_1 + 1} (α := α) (down.{v, u_1} (⨅ (a : (↑s : Type (max u_1 v))), (↑a : ULift α))) (⨅ a ∈ s, a.down)
Tactic: rw [sInf_eq_iInf', down_iInf, iInf_subtype'']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : CompleteLattice α
s : Set (ULift.{v, u_1} α)
rw : Eq.{u_1 + 1} (α := α) (down.{v, u_1} (⨅ (a : (↑s : Type (max u_1 v))), (↑a : ULift α))) (⨅ a ∈ s, a.down)
⊢ down.{v, u_1} (sInf s) = ⨅ a ∈ s, a.down
have rw₁ : Eq.{u_1 + 1} (α := α) (⨅ (i : (↑s : Type (max u_1 v))), down.{v, u_1} (↑i : ULift α)) (⨅ a ∈ s, a.down)
Tactic: rw [sInf_eq_iInf', down_iInf, iInf_subtype'']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : CompleteLattice α
s : Set (ULift.{v, u_1} α)
rw : Eq.{u_1 + 1} (α := α) (down.{v, u_1} (⨅ (a : (↑s : Type (max u_1 v))), (↑a : ULift α))) (⨅ a ∈ s, a.down)
rw₁ : Eq.{u_1 + 1} (α := α) (⨅ (i : (↑s : Type (max u_1 v))), down.{v, u_1} (↑i : ULift α)) (⨅ a ∈ s, a.down)
⊢ down.{v, u_1} (sInf s) = ⨅ a ∈ s, a.down
have rw₂ : Eq.{u_1 + 1} (α := α) (⨅ t ∈ s, t.down) (⨅ a ∈ s, a.down)
Tactic: rw [sInf_eq_iInf', down_iInf, iInf_subtype'']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.MulticoequalizerDiagram (goal)
Goal:
T : Type u
inst : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ (⨆ (i : Bool), bif i then x₃ else x₂) = x₄
have rw : (⨆ (i : Bool), bif i then x₃ else x₂) = x₂ ⊔ x₃
Tactic: rw [← sq.sup_eq, sup_comm, sup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.MulticoequalizerDiagram (goal)
Goal:
T : Type u
inst : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
rw : (⨆ (i : Bool), bif i then x₃ else x₂) = x₂ ⊔ x₃
⊢ (⨆ (i : Bool), bif i then x₃ else x₂) = x₄
have rw₁ : (⨆ (i : Bool), bif i then x₃ else x₂) = x₃ ⊔ x₂
Tactic: rw [← sq.sup_eq, sup_comm, sup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.MulticoequalizerDiagram (goal)
Goal:
T : Type u
inst : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
rw : (⨆ (i : Bool), bif i then x₃ else x₂) = x₂ ⊔ x₃
rw₁ : (⨆ (i : Bool), bif i then x₃ else x₂) = x₃ ⊔ x₂
⊢ (⨆ (i : Bool), bif i then x₃ else x₂) = x₄
have rw₂ : Eq.{u + 1} (α := T) (⨆ (i : Bool), bif i then x₃ else x₂) (⨆ (b : Bool), bif b then x₃ else x₂)
Tactic: rw [← sq.sup_eq, sup_comm, sup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
h : ∀ j < i, e j = sInf s j
⊢ sInf s i ≤ e i
have rw : ⨅ (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))),
    (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i ≤
  e i
Tactic: rw [sInf_apply]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i
⊢ e i ≤ sInf s i
have rw : e i ≤
  ⨅ (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))),
    (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i
Tactic: rw [sInf_apply]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i
⊢ e i ≤
    ⨅ (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))),
      (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i
have h₁ : ∀ (b : (fun (i : ι) ↦ α i) i),
  Membership.mem (γ := Set ((fun (i : ι) ↦ α i) i))
      (Set.range
        fun
          (e : (↑{e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j} : Type (max u_1 u_2))) ↦
        (↑e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) i)
      b →
    e i ≤ b
Tactic: apply le_sInf
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
⊢ IsGLB s (sInf s)
have refine_1 : ∀ (e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (he : e ∈ s), sInf s ≤ e
Tactic: refine ⟨fun e he ↦ ?_, fun e h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
refine_1 : ∀ (e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (he : e ∈ s), sInf s ≤ e
⊢ IsGLB s (sInf s)
have refine_2 : ∀ (e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (h : e ∈ lowerBounds s), e ≤ sInf s
Tactic: refine ⟨fun e he ↦ ?_, fun e h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
⊢ sInf s ≤ e
have refine_1 : ∀ (hs : e < sInf s), False
Tactic: by_contra! hs
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
hs : e < sInf s
⊢ False
have refine_1 : ∀ (a : ι)
  (ha :
    (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → e j = sInf s j) ∧
      (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (e a) (sInf s a)),
  False
Tactic: obtain ⟨a, ha⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ lowerBounds s
⊢ e ≤ sInf s
have refine_2 : ∀ (hs : sInf s < e), False
Tactic: by_contra! hs
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ lowerBounds s
hs : sInf s < e
⊢ False
have refine_2 : ∀ (a : ι)
  (ha :
    (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → sInf s j = e j) ∧
      (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (sInf s a) (e a)),
  False
Tactic: obtain ⟨a, ha⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ lowerBounds s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → sInf s j = e j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (sInf s a) (e a)
⊢ False
have refine_2 : ∀ (f : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (hf : f ∈ s) (hf' : ∀ j < a, f j = sInf s j), ∀ j < a, e j = f j
Tactic: refine ha.2.not_ge <| le_sInf_apply fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
⊢ IsLUB s (sSup s)
have refine_1 : ∀ (e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (he : e ∈ s), e ≤ sSup s
Tactic: refine ⟨fun e he ↦ ?_, fun e h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
refine_1 : ∀ (e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (he : e ∈ s), e ≤ sSup s
⊢ IsLUB s (sSup s)
have refine_2 : ∀ (e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (h : e ∈ upperBounds s), sSup s ≤ e
Tactic: refine ⟨fun e he ↦ ?_, fun e h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
⊢ e ≤ sSup s
have refine_1 : ∀ (hs : sSup s < e), False
Tactic: by_contra! hs
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
he : e ∈ s
hs : sSup s < e
⊢ False
have refine_1 : ∀ (a : ι)
  (ha :
    (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → sSup s j = e j) ∧
      (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (sSup s a) (e a)),
  False
Tactic: obtain ⟨a, ha⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ upperBounds s
⊢ sSup s ≤ e
have refine_2 : ∀ (hs : e < sSup s), False
Tactic: by_contra! hs
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ upperBounds s
hs : e < sSup s
⊢ False
have refine_2 : ∀ (a : ι)
  (ha :
    (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → e j = sSup s j) ∧
      (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (e a) (sSup s a)),
  False
Tactic: obtain ⟨a, ha⟩ := hs
Cleared hypotheses: hs