awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Coframe.MinimalAxioms β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
have rw : f (sInf (max a '' s)) ≤ ⨅ i ∈ s, f a ⊔ f i
Tactic: rw [← le, ← sInf_image, map_sup, map_sInf s, minAx.sup_iInf₂_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Coframe.MinimalAxioms β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
⊢ f (sInf (max a '' s)) ≤ ⨅ i ∈ s, f a ⊔ f i
have simp_rw : f (sInf (max a '' s)) ≤ ⨅ i ∈ s, f (a ⊔ i)
Tactic: simp_rw [← map_sup]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : Compl α
inst_9 : HImp α
inst_10 : HNot α
inst_11 : SDiff α
inst_12 : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι_1 : Type u
κ_1 : ι_1 → Type u
g : (a : ι_1) → κ_1 a → α
⊢ f (⨅ (a : ι_1), ⨆ (b : κ_1 a), g a b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), g a (g_1 a))
have simp_rw : f (sInf (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b)) =
  f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
Tactic: simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : Compl α
inst_9 : HImp α
inst_10 : HNot α
inst_11 : SDiff α
inst_12 : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι_1 : Type u
κ_1 : ι_1 → Type u
g : (a : ι_1) → κ_1 a → α
simp_rw :
  f (sInf (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b)) =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
⊢ f (⨅ (a : ι_1), ⨆ (b : κ_1 a), g a b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), g a (g_1 a))
have simp_rw₁ : ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b) a), f a =
  f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
Tactic: simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : Compl α
inst_9 : HImp α
inst_10 : HNot α
inst_11 : SDiff α
inst_12 : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι_1 : Type u
κ_1 : ι_1 → Type u
g : (a : ι_1) → κ_1 a → α
simp_rw :
  f (sInf (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b)) =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₁ :
  ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b) a), f a =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
⊢ f (⨅ (a : ι_1), ⨆ (b : κ_1 a), g a b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), g a (g_1 a))
have simp_rw₂ : ⨅ (i : ι_1), f (⨆ (b : κ_1 i), g i b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
Tactic: simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : Compl α
inst_9 : HImp α
inst_10 : HNot α
inst_11 : SDiff α
inst_12 : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι_1 : Type u
κ_1 : ι_1 → Type u
g : (a : ι_1) → κ_1 a → α
simp_rw :
  f (sInf (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b)) =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₁ :
  ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b) a), f a =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₂ :
  ⨅ (i : ι_1), f (⨆ (b : κ_1 i), g i b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
⊢ f (⨅ (a : ι_1), ⨆ (b : κ_1 a), g a b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), g a (g_1 a))
have simp_rw₃ : ⨅ (i : ι_1), f (sSup (range fun (b : κ_1 i) ↦ g i b)) =
  f (sSup (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))))
Tactic: simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : Compl α
inst_9 : HImp α
inst_10 : HNot α
inst_11 : SDiff α
inst_12 : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι_1 : Type u
κ_1 : ι_1 → Type u
g : (a : ι_1) → κ_1 a → α
simp_rw :
  f (sInf (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b)) =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₁ :
  ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b) a), f a =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₂ :
  ⨅ (i : ι_1), f (⨆ (b : κ_1 i), g i b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₃ :
  ⨅ (i : ι_1), f (sSup (range fun (b : κ_1 i) ↦ g i b)) =
    f (sSup (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))))
⊢ f (⨅ (a : ι_1), ⨆ (b : κ_1 a), g a b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), g a (g_1 a))
have simp_rw₄ : Eq.{v + 1} (α := β) (⨅ (i : ι_1), ⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (range fun (b : κ_1 i) ↦ g i b) a), f a)
  (⨆ (a : α),
    ⨆ (_ :
      Membership.mem (γ := Set α) (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))) a),
      f a)
Tactic: simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : Compl α
inst_9 : HImp α
inst_10 : HNot α
inst_11 : SDiff α
inst_12 : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι_1 : Type u
κ_1 : ι_1 → Type u
g : (a : ι_1) → κ_1 a → α
simp_rw :
  f (sInf (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b)) =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₁ :
  ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b) a), f a =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₂ :
  ⨅ (i : ι_1), f (⨆ (b : κ_1 i), g i b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₃ :
  ⨅ (i : ι_1), f (sSup (range fun (b : κ_1 i) ↦ g i b)) =
    f (sSup (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))))
simp_rw₄ :
  Eq.{v + 1} (α := β)
    (⨅ (i : ι_1), ⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (range fun (b : κ_1 i) ↦ g i b) a), f a)
    (⨆ (a : α),
      ⨆ (_ :
        Membership.mem (γ := Set α) (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))) a),
        f a)
⊢ f (⨅ (a : ι_1), ⨆ (b : κ_1 a), g a b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), g a (g_1 a))
have simp_rw₅ : Eq.{v + 1} (α := β) (⨅ (i : ι_1), ⨆ (i_1 : κ_1 i), f (g i i_1))
  (⨆ (i : (a : ι_1) → κ_1 a), f (sInf (range fun (a : ι_1) ↦ g a (i a))))
Tactic: simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : Compl α
inst_9 : HImp α
inst_10 : HNot α
inst_11 : SDiff α
inst_12 : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι_1 : Type u
κ_1 : ι_1 → Type u
g : (a : ι_1) → κ_1 a → α
simp_rw :
  f (sInf (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b)) =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₁ :
  ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b) a), f a =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₂ :
  ⨅ (i : ι_1), f (⨆ (b : κ_1 i), g i b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₃ :
  ⨅ (i : ι_1), f (sSup (range fun (b : κ_1 i) ↦ g i b)) =
    f (sSup (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))))
simp_rw₄ :
  Eq.{v + 1} (α := β)
    (⨅ (i : ι_1), ⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (range fun (b : κ_1 i) ↦ g i b) a), f a)
    (⨆ (a : α),
      ⨆ (_ :
        Membership.mem (γ := Set α) (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))) a),
        f a)
simp_rw₅ :
  Eq.{v + 1} (α := β) (⨅ (i : ι_1), ⨆ (i_1 : κ_1 i), f (g i i_1))
    (⨆ (i : (a : ι_1) → κ_1 a), f (sInf (range fun (a : ι_1) ↦ g a (i a))))
⊢ f (⨅ (a : ι_1), ⨆ (b : κ_1 a), g a b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), g a (g_1 a))
have simp_rw₆ : Eq.{v + 1} (α := β) (⨅ (i : ι_1), ⨆ (i_1 : κ_1 i), f (g i i_1))
  (⨆ (i : (a : ι_1) → κ_1 a), ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ g a (i a)) a), f a)
Tactic: simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : Compl α
inst_9 : HImp α
inst_10 : HNot α
inst_11 : SDiff α
inst_12 : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι_1 : Type u
κ_1 : ι_1 → Type u
g : (a : ι_1) → κ_1 a → α
simp_rw :
  f (sInf (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b)) =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₁ :
  ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b) a), f a =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₂ :
  ⨅ (i : ι_1), f (⨆ (b : κ_1 i), g i b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₃ :
  ⨅ (i : ι_1), f (sSup (range fun (b : κ_1 i) ↦ g i b)) =
    f (sSup (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))))
simp_rw₄ :
  Eq.{v + 1} (α := β)
    (⨅ (i : ι_1), ⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (range fun (b : κ_1 i) ↦ g i b) a), f a)
    (⨆ (a : α),
      ⨆ (_ :
        Membership.mem (γ := Set α) (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))) a),
        f a)
simp_rw₅ :
  Eq.{v + 1} (α := β) (⨅ (i : ι_1), ⨆ (i_1 : κ_1 i), f (g i i_1))
    (⨆ (i : (a : ι_1) → κ_1 a), f (sInf (range fun (a : ι_1) ↦ g a (i a))))
simp_rw₆ :
  Eq.{v + 1} (α := β) (⨅ (i : ι_1), ⨆ (i_1 : κ_1 i), f (g i i_1))
    (⨆ (i : (a : ι_1) → κ_1 a), ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ g a (i a)) a), f a)
⊢ f (⨅ (a : ι_1), ⨆ (b : κ_1 a), g a b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), g a (g_1 a))
have simp_rw₇ : Eq.{v + 1} (α := β) (⨅ (i : ι_1), ⨆ (i_1 : κ_1 i), f (g i i_1))
  (⨆ (i : (a : ι_1) → κ_1 a), ⨅ (i_1 : ι_1), f (g i_1 (i i_1)))
Tactic: simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
⊢ Frame α
have le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.frame
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ Frame α
have lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.frame
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
⊢ Frame α
have map_sup : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.frame
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
⊢ Frame α
have map_inf : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.frame
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ Frame α
have map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
Tactic: apply e.injective.frame
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
⊢ Frame α
have map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
Tactic: apply e.injective.frame
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
⊢ Frame α
have map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: apply e.injective.frame
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ Frame α
have map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: apply e.injective.frame
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ Frame α
have map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
Tactic: apply e.injective.frame