awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
⊢ Set.Finite.{u_1} (α := ι) {i : ι | (s i).Nonempty}
have u_inj : Injective u
Tactic: have u_inj : Function.Injective u := by
      rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
      ext
      refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩
      rw [hij]
      exact hj.choose_spec
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
u_inj : Injective u
⊢ Set.Finite.{u_1} (α := ι) {i : ι | (s i).Nonempty}
have this : Finite.{u + 1} (↑(⋃ (i : ι), s i) : Type u)
Tactic: have : Finite (⋃ i, s i) := h
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Sort u_1
inst : Subsingleton ι
s : ι → Set α
⊢ Set.Finite.{u} (α := α) (⋃ (i : ι), s i) ↔ ∀ (i : ι), (s i).Finite
have rw : (∀ (i : PLift ι), (s i.down).Finite) ∧ Set.Finite.{u_1} (α := PLift ι) {i : PLift ι | (s i.down).Nonempty} ↔
  ∀ (i : ι), (s i).Finite
Tactic: rw [← iUnion_plift_down, finite_iUnion_iff _root_.Subsingleton.pairwise]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ Set.Finite.{u} (α := α) (⋃ i ∈ s, f i) ↔
    (∀ i ∈ s, (f i).Finite) ∧ Set.Finite.{v} (α := β) {i : β | i ∈ s ∧ (f i).Nonempty}
have rw : (∀ (i : β), Set.Finite.{u} (α := α) (⋃ (_ : i ∈ s), f i)) ∧
    Set.Finite.{v} (α := β) {i : β | Set.Nonempty.{u} (α := α) (⋃ (_ : i ∈ s), f i)} ↔
  (∀ i ∈ s, (f i).Finite) ∧ Set.Finite.{v} (α := β) {i : β | i ∈ s ∧ (f i).Nonempty}
Tactic: rw [finite_iUnion_iff (by aesop (add unfold safe [Pairwise, PairwiseDisjoint, Set.Pairwise]))]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ (f ⁻¹' s).Finite
have rw : Set.Finite.{u} (α := α) (⋃ y ∈ s, f ⁻¹' {y})
Tactic: rw [← Set.biUnion_preimage_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ Set.Finite.{v} (α := β) (⋃ (a : α), (↑(f a) : Set β))
have rw : Set.Finite.{v} (α := β) (⋃ x ∈ range f, (↑x : Set β))
Tactic: rw [← biUnion_range]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
⊢ ∃ (I : Set ι), I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
have this : Finite.{u + 1} (↑s : Type u)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
this : Finite.{u + 1} (↑s : Type u)
⊢ ∃ (I : Set ι), I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
have choose : ∀ (f : (x : (↑s : Type u)) → ι) (hf : ∀ (x : (↑s : Type u)), (↑x : α) ∈ t (f x)),
  ∃ (I : Set ι), I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
Tactic: choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i by simpa [subset_def] using h
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
this : Finite.{u + 1} (↑s : Type u)
f : (x : (↑s : Type u)) → ι
hf : ∀ (x : (↑s : Type u)), (↑x : α) ∈ t (f x)
⊢ ∃ (I : Set ι), I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
have refine : ∀ (x : α) (hx : x ∈ s), Membership.mem (γ := Set α) (⋃ i ∈ range f, t i) x
Tactic: refine ⟨range f, finite_range f, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
this : Finite.{u + 1} (↑s : Type u)
f : (x : (↑s : Type u)) → ι
hf : ∀ (x : (↑s : Type u)), (↑x : α) ∈ t (f x)
x : α
hx : x ∈ s
⊢ Membership.mem (γ := Set α) (⋃ i ∈ range f, t i) x
have rw : ∃ (i : (↑s : Type u)), x ∈ t (f i)
Tactic: rw [biUnion_range, mem_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
⊢ t = ⋃ (i : (↑{i : ι | i ∈ I} : Type u_1)), (fun (x : (↑{i : ι | i ∈ I} : Type u_1)) ↦ s (↑x : ι) ∩ t) i
have h₁ : ∀ (x : α),
  x ∈ t ↔
    Membership.mem (γ := Set α)
      (⋃ (i : (↑{i : ι | i ∈ I} : Type u_1)), (fun (x : (↑{i : ι | i ∈ I} : Type u_1)) ↦ s (↑x : ι) ∩ t) i) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t ↔
    Membership.mem (γ := Set α)
      (⋃ (i : (↑{i : ι | i ∈ I} : Type u_1)), (fun (x : (↑{i : ι | i ∈ I} : Type u_1)) ↦ s (↑x : ι) ∩ t) i) x
have h₁ : x ∈ t ↔ ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t
Tactic: rw [mem_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t ↔ ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t
have h₁ : x ∈ t → ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
h₁ : x ∈ t → ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t
⊢ x ∈ t ↔ ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t
have h₂ : (∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t) → x ∈ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
⊢ ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t
have h₁ : ∀ (i : ι) (hi : i ∈ I) (H : Membership.mem (γ := Set α) ((fun (h : i ∈ I) ↦ s i) hi) x),
  ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t
Tactic: rcases mem_iUnion.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ Set.Infinite.{u} (α := α) (⋃ i ∈ a, s i)
have rw : Set.Infinite.{u} (α := α) (⋃ (x : (↑a : Type u_1)), s (↑x : ι))
Tactic: rw [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ Set.Infinite.{u} (α := α) (⋃ (x : (↑a : Type u_1)), s (↑x : ι))
have x : Infinite.{u_1 + 1} (↑a : Type u_1)
Tactic: have _ := ha.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
s : Set (Set α)
hs : s.Infinite
⊢ (⋃₀ s).Infinite
have rw : Set.Infinite.{u} (α := α) (⋃ (i : (↑s : Type u)), (↑i : Set α))
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
s : Set (Set α)
hs : s.Infinite
⊢ Set.Infinite.{u} (α := α) (⋃ (i : (↑s : Type u)), (↑i : Set α))
have x : Infinite.{u + 1} (↑s : Type u)
Tactic: have _ := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : FunLike F α β
inst_3 : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ x ∈ s, g x) : β) (⨆ x ∈ s, (f : (a : α) → β) (g x) : β)
have this : Eq.{v + 1} (α := β) ((f : (a : α) → β) (hs.toFinset (s := s).sup g) : β)
  (hs.toFinset (s := s).sup ((⇑f : (a : α) → β) ∘ g) : β)
Tactic: have := map_finset_sup f hs.toFinset g
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : FunLike F α β
inst_3 : SupBotHomClass F α β
inst_4 : Finite ι
f : F
g : ι → α
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ (i : ι), g i) : β) (⨆ (i : ι), (f : (a : α) → β) (g i) : β)
have rw : Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) univ x), g x) : β)
  (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) univ x), (f : (a : α) → β) (g x) : β)
Tactic: rw [← iSup_univ (f := g), ← iSup_univ (f := fun i ↦ f (g i))]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
f : ι → ι' → α
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
ihs :
  ∀ (hf : ∀ i ∈ s_1, Monotone (f i)),
    Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s_1, f i j) (⨅ i ∈ s_1, ⨆ (j : ι'), f i j)
hf : ∀ i ∈ insert a s_1, Monotone (f i)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ insert a s_1, f i j) (⨅ i ∈ insert a s_1, ⨆ (j : ι'), f i j)
have hf₁ : Monotone (f a) ∧ ∀ x ∈ s_1, Monotone (f x)
Tactic: rw [forall_mem_insert] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
f : ι → ι' → α
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
ihs :
  ∀ (hf : ∀ i ∈ s_1, Monotone (f i)),
    Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s_1, f i j) (⨅ i ∈ s_1, ⨆ (j : ι'), f i j)
hf : Monotone (f a) ∧ ∀ x ∈ s_1, Monotone (f x)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ insert a s_1, f i j) (⨅ i ∈ insert a s_1, ⨆ (j : ι'), f i j)
have insert : Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), f a j ⊓ ⨅ x ∈ s_1, f x j) ((⨆ (j : ι'), f a j) ⊓ ⨆ (j : ι'), ⨅ i ∈ s_1, f i j)
Tactic: simp only [iInf_insert, ← ihs hf.2]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
hs : s.Finite
f : ι → ι' → α
hf : ∀ i ∈ s, Monotone (f i)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s, f i j) (⨅ i ∈ s, ⨆ (j : ι'), f i j)
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Monotone (f i)),
  Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), f i j)
    (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), ⨆ (j : ι'), f i j)
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => simp [iSup_const]
  | insert _ _ ihs =>
    rw [forall_mem_insert] at hf
    simp only [iInf_insert, ← ihs hf.2]
    exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj
Cleared hypotheses: hs, hf
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
hs : s.Finite
f : ι → ι' → α
hf : ∀ i ∈ s, Monotone (f i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Monotone (f i)),
    Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), f i j)
      (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), ⨆ (j : ι'), f i j)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s, f i j) (⨅ i ∈ s, ⨆ (j : ι'), f i j)
have insert : ∀ {a : ι} {s : Set ι},
  a ∉ s →
    s.Finite →
      ∀
        (ihs :
          ∀ (hf : ∀ i ∈ s, Monotone (f i)),
            Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s, f i j) (⨅ i ∈ s, ⨆ (j : ι'), f i j))
        (hf : ∀ i ∈ insert a s, Monotone (f i)),
        Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ insert a s, f i j) (⨅ i ∈ insert a s, ⨆ (j : ι'), f i j)
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => simp [iSup_const]
  | insert _ _ ihs =>
    rw [forall_mem_insert] at hf
    simp only [iInf_insert, ← ihs hf.2]
    exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj
Cleared hypotheses: hs, hf
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
ι : Type u_1
ι' : Type u_2
inst : LinearOrder ι'
inst_1 : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
⊢ Eq (α := Set ((i : ι) → α i)) (⋃ (j : ι'), I.pi (α := α) fun (i : ι) ↦ s i j)
    (I.pi (α := α) fun (i : ι) ↦ ⋃ (j : ι'), s i j)
have simp : Eq (α := Set ((i : ι) → α i)) (⋃ (j : ι'), ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) j)
  (⋂ (x : (↑I : Type u_1)), ⋃ (i : ι'), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) i)
Tactic: simp only [pi_def, biInter_eq_iInter, preimage_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
inst : LinearOrder ι'
inst_1 : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
⊢ Eq (α := Set ((i : ι) → α i)) (⋃ (j : ι'), ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) j)
    (⋂ (x : (↑I : Type u_1)), ⋃ (i : ι'), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) i)
have this : Finite.{u_1 + 1} (↑I : Type u_1)
Tactic: haveI := hI.fintype.finite
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
ι : Type u_1
ι' : Type u_2
inst : LinearOrder ι'
inst_1 : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
this : Finite.{u_1 + 1} (↑I : Type u_1)
⊢ Eq (α := Set ((i : ι) → α i)) (⋃ (j : ι'), ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) j)
    (⋂ (x : (↑I : Type u_1)), ⋃ (i : ι'), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) i)
have refine : ∀ (i : (↑I : Type u_1)) (j₁ j₂ : ι') (h : j₁ ≤ j₂),
  eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) j₁ ≤ eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) j₂
Tactic: refine iUnion_iInter_of_monotone (ι' := ι') (fun (i : I) j₁ j₂ h => ?_)
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Sort v
κ : ι → Sort w
inst : Order.Frame α
inst_1 : Finite ι
f : (a : ι) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))
have suffices : ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : (a : ι) → κ a → α),
  Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))
Tactic: suffices ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : Π a, κ a → α),
      ⨅ a, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a, f a (g a) by
    simpa [← Equiv.plift.symm.iInf_comp, ← Equiv.plift.symm.iSup_comp,
        ← (Equiv.plift.piCongr fun a => @Equiv.plift (κ a.down)).symm.iSup_comp] using
      this (κ := fun a => PLift (κ a.down)) fun (a : PLift ι) b => f a.down b.down
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι_1 : Sort v
κ_1 : ι_1 → Sort w
inst : Order.Frame α
inst_1 : Finite ι_1
f_1 : (a : ι_1) → κ_1 a → α
ι : Type v
κ : ι → Type w
inst_2 : Finite ι
f : (a : ι) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))
have of_equiv : ∀ {α_1 β : Type v} (e : α_1 ≃ β)
  (h :
    ∀ {κ : α_1 → Type w} (f : (a : α_1) → κ a → α),
      Eq.{u + 1} (α := α) (⨅ (a : α_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : α_1) → κ a), ⨅ (a : α_1), f a (g a)))
  {κ : β → Type w} (f : (a : β) → κ a → α),
  Eq.{u + 1} (α := α) (⨅ (a : β), ⨆ (b : κ a), f a b) (⨆ (g : (a : β) → κ a), ⨅ (a : β), f a (g a))
Tactic: induction ι using Finite.induction_empty_option with
  | of_equiv e h => simp [← e.iInf_comp, ← e.piCongrLeft κ |>.iSup_comp, h]
  | h_empty => simp [iInf_of_empty, iSup_const]
  | h_option h =>
    simp only [iInf_option, h, ← (Equiv.piOptionEquivProd (β := κ)).symm.iSup_comp,
      Equiv.piOptionEquivProd_symm_apply, iSup_prod, ← inf_iSup_eq, ← iSup_inf_eq]
Cleared hypotheses: κ, f
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι_1 : Sort v
κ_1 : ι_1 → Sort w
inst : Order.Frame α
inst_1 : Finite ι_1
f_1 : (a : ι_1) → κ_1 a → α
ι : Type v
κ : ι → Type w
inst_2 : Finite ι
f : (a : ι) → κ a → α
of_equiv :
  ∀ {α_1 β : Type v} (e : α_1 ≃ β)
    (h :
      ∀ {κ : α_1 → Type w} (f : (a : α_1) → κ a → α),
        Eq.{u + 1} (α := α) (⨅ (a : α_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : α_1) → κ a), ⨅ (a : α_1), f a (g a)))
    {κ : β → Type w} (f : (a : β) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : β), ⨆ (b : κ a), f a b) (⨆ (g : (a : β) → κ a), ⨅ (a : β), f a (g a))
⊢ Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))
have h_empty : ∀ {κ : PEmpty.{v + 1} → Type w} (f : (a : PEmpty.{v + 1}) → κ a → α),
  Eq.{u + 1} (α := α) (⨅ (a : PEmpty.{v + 1}), ⨆ (b : κ a), f a b)
    (⨆ (g : (a : PEmpty.{v + 1}) → κ a), ⨅ (a : PEmpty.{v + 1}), f a (g a))
Tactic: induction ι using Finite.induction_empty_option with
  | of_equiv e h => simp [← e.iInf_comp, ← e.piCongrLeft κ |>.iSup_comp, h]
  | h_empty => simp [iInf_of_empty, iSup_const]
  | h_option h =>
    simp only [iInf_option, h, ← (Equiv.piOptionEquivProd (β := κ)).symm.iSup_comp,
      Equiv.piOptionEquivProd_symm_apply, iSup_prod, ← inf_iSup_eq, ← iSup_inf_eq]
Cleared hypotheses: κ, f
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι_1 : Sort v
κ_1 : ι_1 → Sort w
inst : Order.Frame α
inst_1 : Finite ι_1
f_1 : (a : ι_1) → κ_1 a → α
ι : Type v
κ : ι → Type w
inst_2 : Finite ι
f : (a : ι) → κ a → α
of_equiv :
  ∀ {α_1 β : Type v} (e : α_1 ≃ β)
    (h :
      ∀ {κ : α_1 → Type w} (f : (a : α_1) → κ a → α),
        Eq.{u + 1} (α := α) (⨅ (a : α_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : α_1) → κ a), ⨅ (a : α_1), f a (g a)))
    {κ : β → Type w} (f : (a : β) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : β), ⨆ (b : κ a), f a b) (⨆ (g : (a : β) → κ a), ⨅ (a : β), f a (g a))
h_empty :
  ∀ {κ : PEmpty.{v + 1} → Type w} (f : (a : PEmpty.{v + 1}) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : PEmpty.{v + 1}), ⨆ (b : κ a), f a b)
      (⨆ (g : (a : PEmpty.{v + 1}) → κ a), ⨅ (a : PEmpty.{v + 1}), f a (g a))
⊢ Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))
have h_option : ∀ {α_1 : Type v} [Fintype α_1]
  (h :
    ∀ {κ : α_1 → Type w} (f : (a : α_1) → κ a → α),
      Eq.{u + 1} (α := α) (⨅ (a : α_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : α_1) → κ a), ⨅ (a : α_1), f a (g a)))
  {κ : Option α_1 → Type w} (f : (a : Option α_1) → κ a → α),
  Eq.{u + 1} (α := α) (⨅ (a : Option α_1), ⨆ (b : κ a), f a b)
    (⨆ (g : (a : Option α_1) → κ a), ⨅ (a : Option α_1), f a (g a))
Tactic: induction ι using Finite.induction_empty_option with
  | of_equiv e h => simp [← e.iInf_comp, ← e.piCongrLeft κ |>.iSup_comp, h]
  | h_empty => simp [iInf_of_empty, iSup_const]
  | h_option h =>
    simp only [iInf_option, h, ← (Equiv.piOptionEquivProd (β := κ)).symm.iSup_comp,
      Equiv.piOptionEquivProd_symm_apply, iSup_prod, ← inf_iSup_eq, ← iSup_inf_eq]
Cleared hypotheses: κ, f
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
ι : Type v
κ : ι → Sort w
inst : Nonempty ((a : ι) → κ a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
h :
  ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
have this : Nonempty ((a : ι) → PLift (κ a))
Tactic: haveI : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type v
κ : ι → Sort w
inst : Nonempty ((a : ι) → κ a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
have suffices : ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
  Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
Tactic: suffices h : ∀ {κ : ι → Type w} [Nonempty (Π a, κ a)] (f : Π a, κ a → α),
      ⨅ a ∈ s, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a ∈ s, f a (g a) by
    haveI : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
ι : Type v
κ_1 : ι → Sort w
inst : Nonempty ((a : ι) → κ_1 a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f_1 : (a : ι) → κ_1 a → α
κ : ι → Type w
inst_2 : Nonempty ((a : ι) → κ a)
f : (a : ι) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
have this : Finite.{v + 1} (↑s : Type v)
Tactic: haveI := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
ι : Type v
κ_1 : ι → Sort w
inst : Nonempty ((a : ι) → κ_1 a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f_1 : (a : ι) → κ_1 a → α
κ : ι → Type w
inst_2 : Nonempty ((a : ι) → κ a)
f : (a : ι) → κ a → α
this : Finite.{v + 1} (↑s : Type v)
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
have this₁ : Nonempty ((a : { a : ι // a ∉ s }) → κ (↑a : ι))
Tactic: haveI : Nonempty (Π a : { a // a ∉ s }, κ ↑a) := ‹Nonempty (Π a, κ a)›.map fun f a ↦ f a
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type v
κ : ι → Sort w
inst : Nonempty ((a : ι) → κ a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
have suffices : ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
  Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
Tactic: classical
  suffices h : ∀ {κ : ι → Type w} [Nonempty (Π a, κ a)] (f : Π a, κ a → α),
      ⨅ a ∈ s, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a ∈ s, f a (g a) by
    haveI : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down
  intro κ _ f
  haveI := hs.to_subtype
  haveI : Nonempty (Π a : { a // a ∉ s }, κ ↑a) := ‹Nonempty (Π a, κ a)›.map fun f a ↦ f a
  simp [← iInf_subtype'', iInf_iSup_eq_of_finite (ι := s),
    ← Equiv.piEquivPiSubtypeProd (· ∈ s) _ |>.symm.iSup_comp, iSup_prod, iSup_const]