awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
inr : f (i, i') ≤ (fun (i : ι) ↦ (⨆ i' ∈ t, f (i, i') : α)) (i, i').1
⊢ (Disjoint on f) (i, i') (j, j')
have inr₁ : f (j, j') ≤ (fun (i : ι) ↦ (⨆ i' ∈ t, f (i, i') : α)) (j, j').1
Tactic: refine (hs hi.1 hj.1 hij).mono ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') ≤ (fun (i : ι) ↦ (⨆ i' ∈ t, f (i, i') : α)) (i, i').1
have h₁ : f (i, i') = f ((i, i').1, i')
Tactic: convert! le_iSup₂ (α := α) i' hi.2
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') ≤ (fun (i : ι) ↦ (⨆ i' ∈ t, f (i, i') : α)) (j, j').1
have h₁ : f (j, j') = f ((j, j').1, j')
Tactic: convert! le_iSup₂ (α := α) j' hj.2
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
⊢ (s ×ˢ t).PairwiseDisjoint f ↔
    (PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')) ∧
      PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
have refine_1 : ∀ (h : (s ×ˢ t).PairwiseDisjoint f) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i ≠ j),
  onFun.{u_2 + 1, u_1 + 1, 1} (β := α) Disjoint (fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')) i j
Tactic: refine
      ⟨fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩, fun h => h.1.prod_left h.2⟩
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
refine_1 :
  ∀ (h : (s ×ˢ t).PairwiseDisjoint f) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i ≠ j),
    onFun.{u_2 + 1, u_1 + 1, 1} (β := α) Disjoint (fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')) i j
⊢ (s ×ˢ t).PairwiseDisjoint f ↔
    (PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')) ∧
      PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
have refine_2 : ∀ (h : (s ×ˢ t).PairwiseDisjoint f) (i : ι') (hi : i ∈ t) (j : ι') (hj : j ∈ t) (hij : i ≠ j),
  onFun.{u_3 + 1, u_1 + 1, 1} (β := α) Disjoint (fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')) i j
Tactic: refine
      ⟨fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩, fun h => h.1.prod_left h.2⟩
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ onFun.{u_2 + 1, u_1 + 1, 1} (β := α) Disjoint (fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')) i j
have refine_1 : ∀ (i_1 : ι') (i_2 : i_1 ∈ t) (i_3 : ι') (i_4 : i_3 ∈ t), Disjoint (f (i, i_1)) (f (j, i_3))
Tactic: simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ onFun.{u_3 + 1, u_1 + 1, 1} (β := α) Disjoint (fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')) i j
have refine_2 : ∀ (i_1 : ι) (i_2 : i_1 ∈ s) (i_3 : ι) (i_4 : i_3 ∈ s), Disjoint (f (i_1, i)) (f (i_3, j))
Tactic: simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
⊢ Eq.{u_1 + 1} (α := Set α) ((⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i) (⋃ i ∈ s \ t, f i)
have f₁ : ∀ (i : ι) (hi : i ∈ s \ t) (a : α) (ha : a ∈ f i), a ∉ ⋃ x ∈ t, f x
Tactic: refine
    (biUnion_diff_biUnion_subset f s t).antisymm
      (iUnion₂_subset fun i hi a ha => (mem_diff _).2 ⟨mem_biUnion hi.1 ha, ?_⟩)
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ a ∉ ⋃ x ∈ t, f x
have rw : ¬∃ (i : ι) (_ : i ∈ t), a ∈ f i
Tactic: rw [mem_iUnion₂]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ (𝒫 s).PairwiseDisjoint (α := Set (Set α)) fun (t : Set α) ↦ {t, insert a t}
have rw : ∀ ⦃i : Set α⦄, i ∈ 𝒫 s → ∀ ⦃j : Set α⦄, j ∈ 𝒫 s → Set.Nonempty (α := Set α) ({i, insert a i} ∩ {j, insert a j}) → i = j
Tactic: rw [pairwiseDisjoint_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (hypothesis)
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
⊢ Set.Nonempty (α := Set α) ({i, insert a i} ∩ {j, insert a j}) → i = j
have this : insert a i = insert a j → i = j
Tactic: have := insert_erase_invOn.2.injOn (notMem_subset hi ha) (notMem_subset hj ha)
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : Subset.{u_1} (α := Set α) (⋃ i ∈ s, f i) (⋃ i ∈ t, f i)
i : ι
hi : i ∈ s
⊢ i ∈ t
have obtain : ∀ (a : α) (hai : a ∈ f i), i ∈ t
Tactic: obtain ⟨a, hai⟩ := h₁ i hi
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : Subset.{u_1} (α := Set α) (⋃ i ∈ s, f i) (⋃ i ∈ t, f i)
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
⊢ i ∈ t
have obtain : ∀ (j : ι) (hj : j ∈ t) (haj : a ∈ f j), i ∈ t
Tactic: obtain ⟨j, hj, haj⟩ := mem_iUnion₂.1 (h <| mem_iUnion₂_of_mem hi hai)
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : Membership.mem (γ := Set α) (⋃ i ∈ s, f i) y
⊢ ∃! i : ι, i ∈ s ∧ y ∈ f i
have ex : ∃ x ∈ s, y ∈ f x
Tactic: refine existsUnique_of_exists_of_unique ?ex ?unique
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : Membership.mem (γ := Set α) (⋃ i ∈ s, f i) y
ex : ∃ x ∈ s, y ∈ f x
⊢ ∃! i : ι, i ∈ s ∧ y ∈ f i
have unique : ∀ (y₁ y₂ : ι), y₁ ∈ s ∧ y ∈ f y₁ → y₂ ∈ s ∧ y ∈ f y₂ → y₁ = y₂
Tactic: refine existsUnique_of_exists_of_unique ?ex ?unique
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.List (goal)
Goal:
α : Type u_1
r : α → α → Prop
l : List α
inst : Std.Symm r
hl : l.Nodup
⊢ Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l
have cons : ∀ (a : α) (l : List α) (ih : ∀ (hl : l.Nodup), Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l) (hl : (a :: l).Nodup),
  Set.Pairwise {a_1 : α | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
Tactic: induction l with | nil => simp | cons a l ih => ?_
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.List (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
l_1 : List α
inst : Std.Symm r
a : α
l : List α
ih : ∀ (hl : l.Nodup), Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l
hl : (a :: l).Nodup
⊢ Set.Pairwise {a_1 : α | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
have hl₁ : ¬a ∈ l ∧ l.Nodup
Tactic: rw [List.nodup_cons] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.List (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
l_1 : List α
inst : Std.Symm r
a : α
l : List α
ih : ∀ (hl : l.Nodup), Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l
hl : ¬a ∈ l ∧ l.Nodup
⊢ Set.Pairwise {a_1 : α | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
have this : ∀ (b : α), b ∈ l → (¬a = b → r a b ↔ r a b)
Tactic: have : ∀ b ∈ l, ¬a = b → r a b ↔ r a b := fun b hb =>
    imp_iff_right (ne_of_mem_of_not_mem hb hl.1).symm
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst : (i : α) → Decidable (Membership.mem (γ := Set α) ∅ i)
⊢ piecewise (β := δ) ∅ f g = g
have h : ∀ (i : α), piecewise (β := δ) ∅ f g i = g i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst : (i : α) → Decidable (Membership.mem (γ := Set α) univ i)
⊢ piecewise (β := δ) univ f g = f
have h : ∀ (i : α), piecewise (β := δ) univ f g i = f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise (β := δ) f g = update (β := δ) (s.piecewise (β := δ) f g) j (f j)
have simp : (fun (i : α) ↦ if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j)
Tactic: simp +unfoldPartialApp only [piecewise, mem_insert_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
⊢ (fun (i : α) ↦ if i = j ∨ i ∈ s then f i else g i) =
    update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j)
have h : ∀ (i : α), (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
have pos : ∀ (h : i = j),
  (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
pos :
  ∀ (h : i = j),
    (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
have neg : ∀ (h : ¬i = j),
  (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
have pos : (if j = j ∨ j ∈ s then f j else g j) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) j
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
have pos : ∀ (h' : i ∈ s),
  (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
Tactic: by_cases h' : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
pos :
  ∀ (h' : i ∈ s),
    (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
have neg : ∀ (h' : ¬i ∈ s),
  (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
Tactic: by_cases h' : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
inst : (y : α) → Decidable (Membership.mem (γ := Set α) {x} y)
inst_1 : DecidableEq α
f g : α → β
⊢ piecewise (β := fun (i : α) ↦ β) {x} f g = update (β := fun (a : α) ↦ β) g x (f x)
have h : ∀ (y : α), piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
inst : (y : α) → Decidable (Membership.mem (γ := Set α) {x} y)
inst_1 : DecidableEq α
f g : α → β
y : α
⊢ piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y
have pos : ∀ (hy : y = x), piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y
Tactic: by_cases hy : y = x
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
inst : (y : α) → Decidable (Membership.mem (γ := Set α) {x} y)
inst_1 : DecidableEq α
f g : α → β
y : α
pos : ∀ (hy : y = x), piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y
⊢ piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y
have neg : ∀ (hy : ¬y = x), piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y
Tactic: by_cases hy : y = x
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
inst : (y : α) → Decidable (Membership.mem (γ := Set α) {x} y)
inst_1 : DecidableEq α
f g : α → β
y : α
hy : y = x
⊢ piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y
have pos : piecewise (β := fun (i : α) ↦ β) {x} f g x = update (β := fun (a : α) ↦ β) g x (f x) x
Tactic: subst y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Type u_8
inst : (i : α) → Preorder (δ i)
s : Set α
inst_1 : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ s.piecewise (β := δ) f₁ f₂ ≤ s.piecewise (β := δ) g₁ g₂
have h₃ : ∀ (i : α), i ∈ s → f₁ i ≤ s.piecewise (β := δ) g₁ g₂ i
Tactic: apply piecewise_le
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Type u_8
inst : (i : α) → Preorder (δ i)
s : Set α
inst_1 : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
h₃ : ∀ (i : α), i ∈ s → f₁ i ≤ s.piecewise (β := δ) g₁ g₂ i
⊢ s.piecewise (β := δ) f₁ f₂ ≤ s.piecewise (β := δ) g₁ g₂
have h₄ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ s.piecewise (β := δ) g₁ g₂ i
Tactic: apply piecewise_le
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ MapsTo (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)
have refine_1 : EqOn f₁ (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s₁ ∩ s)
Tactic: refine (h₁.congr ?_).union_union (h₂.congr ?_)
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
refine_1 : EqOn f₁ (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s₁ ∩ s)
⊢ MapsTo (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)
have refine_2 : EqOn f₂ (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s₂ ∩ sᶜ)
Tactic: refine (h₁.congr ?_).union_union (h₂.congr ?_)
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ EqOn (s.piecewise (β := fun (a : α) ↦ β) f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)
have simp : (∀ ⦃x : α⦄, x ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' x = g x) ↔
  ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)
Tactic: simp only [EqOn, ← forall_and]
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ (∀ ⦃x : α⦄, x ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' x = g x) ↔
    ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)
have refine : ∀ (a : α), a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
Tactic: refine forall_congr' fun a => ?_
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
⊢ a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
have pos : a ∈ s → (a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a))
Tactic: by_cases a ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
pos :
  a ∈ s →
    (a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a))
⊢ a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
have neg : ¬a ∈ s → (a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a))
Tactic: by_cases a ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
⊢ x ∈ s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)
have pos : x ∈ s → (x ∈ s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t))
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
pos : x ∈ s → (x ∈ s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t))
⊢ x ∈ s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)
have neg : ¬x ∈ s → (x ∈ s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t))
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
⊢ h x (s.piecewise (β := δ) f g x) = s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) (fun (x : α) ↦ h x (g x)) x
have pos : ∀ (hx : x ∈ s),
  h x (s.piecewise (β := δ) f g x) = s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) (fun (x : α) ↦ h x (g x)) x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
pos :
  ∀ (hx : x ∈ s),
    h x (s.piecewise (β := δ) f g x) = s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) (fun (x : α) ↦ h x (g x)) x
⊢ h x (s.piecewise (β := δ) f g x) = s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) (fun (x : α) ↦ h x (g x)) x
have neg : ∀ (hx : ¬x ∈ s),
  h x (s.piecewise (β := δ) f g x) = s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) (fun (x : α) ↦ h x (g x)) x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
⊢ h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x) =
    s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) (fun (x : α) ↦ h x (g x) (g' x)) x
have pos : ∀ (hx : x ∈ s),
  h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x) =
    s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) (fun (x : α) ↦ h x (g x) (g' x)) x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
pos :
  ∀ (hx : x ∈ s),
    h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x) =
      s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) (fun (x : α) ↦ h x (g x) (g' x)) x
⊢ h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x) =
    s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) (fun (x : α) ↦ h x (g x) (g' x)) x
have neg : ∀ (hx : ¬x ∈ s),
  h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x) =
    s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) (fun (x : α) ↦ h x (g x) (g' x)) x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
⊢ s.piecewise (β := δ) f f = f
have h : ∀ (x : α), s.piecewise (β := δ) f f x = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
x : α
⊢ s.piecewise (β := δ) f f x = f x
have pos : ∀ (hx : x ∈ s), s.piecewise (β := δ) f f x = f x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
x : α
pos : ∀ (hx : x ∈ s), s.piecewise (β := δ) f f x = f x
⊢ s.piecewise (β := δ) f f x = f x
have neg : ∀ (hx : ¬x ∈ s), s.piecewise (β := δ) f f x = f x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ range (s.piecewise (β := fun (a : α) ↦ β) f g) = f '' s ∪ g '' sᶜ
have h : ∀ (y : β), y ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g) ↔ y ∈ f '' s ∪ g '' sᶜ
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g) ↔ y ∈ f '' s ∪ g '' sᶜ
have h : y ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g) → y ∈ f '' s ∪ g '' sᶜ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
h : y ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g) → y ∈ f '' s ∪ g '' sᶜ
⊢ y ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g) ↔ y ∈ f '' s ∪ g '' sᶜ
have h₁ : y ∈ f '' s ∪ g '' sᶜ → y ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g)
Tactic: constructor