awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
⊢ Disjoint (α := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i))
have rw : ∀ ⦃a : (i : ι) → α i⦄,
  Membership.mem (γ := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) a →
    a ∉ pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i)
Tactic: rw [disjoint_left]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
z : (i : ι) → α i
h₁ : Membership.mem (γ := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) z
h₂ : Membership.mem (γ := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i)) z
⊢ False
have refine : update (β := α) y i₀ m i₀ < z i₀
Tactic: refine (h₁ i₀ (mem_univ _)).2.not_gt ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update (β := α) f i '' Icc a b = Icc (update (β := α) f i a) (update (β := α) f i b)
have h : ∀ (x : (a : ι) → α a), x ∈ update (β := α) f i '' Icc a b ↔ x ∈ Icc (update (β := α) f i a) (update (β := α) f i b)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update (β := α) f i '' Icc a b ↔ x ∈ Icc (update (β := α) f i a) (update (β := α) f i b)
have h : x ∈ update (β := α) f i '' Icc a b ↔
  Membership.mem (γ := Set ((a : ι) → α a))
    (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x
Tactic: rw [← Set.pi_univ_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update (β := α) f i '' Icc a b ↔
    Membership.mem (γ := Set ((a : ι) → α a))
      (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x
have h : x ∈ update (β := α) f i '' Icc a b →
  Membership.mem (γ := Set ((a : ι) → α a))
    (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x
Tactic: refine ⟨?_, fun h => ⟨x i, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h :
  x ∈ update (β := α) f i '' Icc a b →
    Membership.mem (γ := Set ((a : ι) → α a))
      (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x
⊢ x ∈ update (β := α) f i '' Icc a b ↔
    Membership.mem (γ := Set ((a : ι) → α a))
      (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x
have h₁ : ∀
  (h :
    Membership.mem (γ := Set ((a : ι) → α a))
      (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x),
  x i ∈ Icc a b
Tactic: refine ⟨?_, fun h => ⟨x i, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h :
  x ∈ update (β := α) f i '' Icc a b →
    Membership.mem (γ := Set ((a : ι) → α a))
      (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x
h₁ :
  ∀
    (h :
      Membership.mem (γ := Set ((a : ι) → α a))
        (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x),
    x i ∈ Icc a b
⊢ x ∈ update (β := α) f i '' Icc a b ↔
    Membership.mem (γ := Set ((a : ι) → α a))
      (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x
have h₂ : ∀
  (h :
    Membership.mem (γ := Set ((a : ι) → α a))
      (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x),
  update (β := α) f i (x i) = x
Tactic: refine ⟨?_, fun h => ⟨x i, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h :
  Membership.mem (γ := Set ((a : ι) → α a))
    (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x
⊢ update (β := α) f i (x i) = x
have h₁ : ∀ (j : ι), update (β := α) f i (x i) j = x j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h :
  Membership.mem (γ := Set ((a : ι) → α a))
    (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x
j : ι
⊢ update (β := α) f i (x i) j = x j
have h₁ : update (β := α) f i (x i) i = x i
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h :
  Membership.mem (γ := Set ((a : ι) → α a))
    (pi (α := α) univ fun (i_1 : ι) ↦ Icc (update (β := α) f i a i_1) (update (β := α) f i b i_1)) x
j : ι
h₁ : update (β := α) f i (x i) i = x i
⊢ update (β := α) f i (x i) j = x j
have h₂ : ∀ (hij : i ≠ j), update (β := α) f i (x i) j = x j
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update (β := α) f i '' Ico a b = Ico (update (β := α) f i a) (update (β := α) f i b)
have rw : update (β := α) f i '' (Icc a b \ {b}) = Ico (update (β := α) f i a) (update (β := α) f i b)
Tactic: rw [← Icc_diff_right, ← Icc_diff_right, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Icc a b \ {b}) = Ico (update (β := α) f i a) (update (β := α) f i b)
⊢ update (β := α) f i '' Ico a b = Ico (update (β := α) f i a) (update (β := α) f i b)
have rw₁ : update (β := α) f i '' (Icc a b \ {b}) = Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b}
Tactic: rw [← Icc_diff_right, ← Icc_diff_right, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Icc a b \ {b}) = Ico (update (β := α) f i a) (update (β := α) f i b)
rw₁ :
  update (β := α) f i '' (Icc a b \ {b}) = Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b}
⊢ update (β := α) f i '' Ico a b = Ico (update (β := α) f i a) (update (β := α) f i b)
have rw₂ : update (β := α) f i '' Icc a b \ update (β := α) f i '' {b} =
  Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b}
Tactic: rw [← Icc_diff_right, ← Icc_diff_right, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Icc a b \ {b}) = Ico (update (β := α) f i a) (update (β := α) f i b)
rw₁ :
  update (β := α) f i '' (Icc a b \ {b}) = Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b}
rw₂ :
  update (β := α) f i '' Icc a b \ update (β := α) f i '' {b} =
    Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b}
⊢ update (β := α) f i '' Ico a b = Ico (update (β := α) f i a) (update (β := α) f i b)
have rw₃ : update (β := α) f i '' Icc a b \ {update (β := α) f i b} =
  Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b}
Tactic: rw [← Icc_diff_right, ← Icc_diff_right, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Icc a b \ {b}) = Ico (update (β := α) f i a) (update (β := α) f i b)
rw₁ :
  update (β := α) f i '' (Icc a b \ {b}) = Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b}
rw₂ :
  update (β := α) f i '' Icc a b \ update (β := α) f i '' {b} =
    Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b}
rw₃ :
  update (β := α) f i '' Icc a b \ {update (β := α) f i b} =
    Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b}
⊢ update (β := α) f i '' Ico a b = Ico (update (β := α) f i a) (update (β := α) f i b)
have rw₄ : Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b} =
  Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i b}
Tactic: rw [← Icc_diff_right, ← Icc_diff_right, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update (β := α) f i '' Ioc a b = Ioc (update (β := α) f i a) (update (β := α) f i b)
have rw : update (β := α) f i '' (Icc a b \ {a}) = Ioc (update (β := α) f i a) (update (β := α) f i b)
Tactic: rw [← Icc_diff_left, ← Icc_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Icc a b \ {a}) = Ioc (update (β := α) f i a) (update (β := α) f i b)
⊢ update (β := α) f i '' Ioc a b = Ioc (update (β := α) f i a) (update (β := α) f i b)
have rw₁ : update (β := α) f i '' (Icc a b \ {a}) = Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
Tactic: rw [← Icc_diff_left, ← Icc_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Icc a b \ {a}) = Ioc (update (β := α) f i a) (update (β := α) f i b)
rw₁ :
  update (β := α) f i '' (Icc a b \ {a}) = Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
⊢ update (β := α) f i '' Ioc a b = Ioc (update (β := α) f i a) (update (β := α) f i b)
have rw₂ : update (β := α) f i '' Icc a b \ update (β := α) f i '' {a} =
  Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
Tactic: rw [← Icc_diff_left, ← Icc_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Icc a b \ {a}) = Ioc (update (β := α) f i a) (update (β := α) f i b)
rw₁ :
  update (β := α) f i '' (Icc a b \ {a}) = Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
rw₂ :
  update (β := α) f i '' Icc a b \ update (β := α) f i '' {a} =
    Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
⊢ update (β := α) f i '' Ioc a b = Ioc (update (β := α) f i a) (update (β := α) f i b)
have rw₃ : update (β := α) f i '' Icc a b \ {update (β := α) f i a} =
  Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
Tactic: rw [← Icc_diff_left, ← Icc_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Icc a b \ {a}) = Ioc (update (β := α) f i a) (update (β := α) f i b)
rw₁ :
  update (β := α) f i '' (Icc a b \ {a}) = Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
rw₂ :
  update (β := α) f i '' Icc a b \ update (β := α) f i '' {a} =
    Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
rw₃ :
  update (β := α) f i '' Icc a b \ {update (β := α) f i a} =
    Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
⊢ update (β := α) f i '' Ioc a b = Ioc (update (β := α) f i a) (update (β := α) f i b)
have rw₄ : Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a} =
  Icc (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
Tactic: rw [← Icc_diff_left, ← Icc_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update (β := α) f i '' Ioo a b = Ioo (update (β := α) f i a) (update (β := α) f i b)
have rw : update (β := α) f i '' (Ico a b \ {a}) = Ioo (update (β := α) f i a) (update (β := α) f i b)
Tactic: rw [← Ico_diff_left, ← Ico_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Ico a b \ {a}) = Ioo (update (β := α) f i a) (update (β := α) f i b)
⊢ update (β := α) f i '' Ioo a b = Ioo (update (β := α) f i a) (update (β := α) f i b)
have rw₁ : update (β := α) f i '' (Ico a b \ {a}) = Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
Tactic: rw [← Ico_diff_left, ← Ico_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Ico a b \ {a}) = Ioo (update (β := α) f i a) (update (β := α) f i b)
rw₁ :
  update (β := α) f i '' (Ico a b \ {a}) = Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
⊢ update (β := α) f i '' Ioo a b = Ioo (update (β := α) f i a) (update (β := α) f i b)
have rw₂ : update (β := α) f i '' Ico a b \ update (β := α) f i '' {a} =
  Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
Tactic: rw [← Ico_diff_left, ← Ico_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Ico a b \ {a}) = Ioo (update (β := α) f i a) (update (β := α) f i b)
rw₁ :
  update (β := α) f i '' (Ico a b \ {a}) = Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
rw₂ :
  update (β := α) f i '' Ico a b \ update (β := α) f i '' {a} =
    Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
⊢ update (β := α) f i '' Ioo a b = Ioo (update (β := α) f i a) (update (β := α) f i b)
have rw₃ : update (β := α) f i '' Ico a b \ {update (β := α) f i a} =
  Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
Tactic: rw [← Ico_diff_left, ← Ico_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
rw : update (β := α) f i '' (Ico a b \ {a}) = Ioo (update (β := α) f i a) (update (β := α) f i b)
rw₁ :
  update (β := α) f i '' (Ico a b \ {a}) = Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
rw₂ :
  update (β := α) f i '' Ico a b \ update (β := α) f i '' {a} =
    Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
rw₃ :
  update (β := α) f i '' Ico a b \ {update (β := α) f i a} =
    Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
⊢ update (β := α) f i '' Ioo a b = Ioo (update (β := α) f i a) (update (β := α) f i b)
have rw₄ : Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a} =
  Ico (update (β := α) f i a) (update (β := α) f i b) \ {update (β := α) f i a}
Tactic: rw [← Ico_diff_left, ← Ico_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Lattice (α i)
inst_1 : DecidableEq ι
f : (i : ι) → α i
i : ι
a b : α i
⊢ Icc (update (β := α) f i (a ⊓ b)) (update (β := α) f i (a ⊔ b)) = uIcc (update (β := α) f i a) (update (β := α) f i b)
have simp_rw : Icc (update (β := α) f i (a ⊓ b)) (update (β := α) f i (a ⊔ b)) =
  Icc (update (β := α) f i a ⊓ update (β := α) f i b) (update (β := α) f i a ⊔ update (β := α) f i b)
Tactic: simp_rw [uIcc, update_sup, update_inf]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Lattice (α i)
inst_1 : DecidableEq ι
f : (i : ι) → α i
i : ι
a b : α i
simp_rw :
  Icc (update (β := α) f i (a ⊓ b)) (update (β := α) f i (a ⊔ b)) =
    Icc (update (β := α) f i a ⊓ update (β := α) f i b) (update (β := α) f i a ⊔ update (β := α) f i b)
⊢ Icc (update (β := α) f i (a ⊓ b)) (update (β := α) f i (a ⊔ b)) = uIcc (update (β := α) f i a) (update (β := α) f i b)
have simp_rw₁ : Icc (update (β := α) f i (a ⊓ b)) (update (β := α) f i a ⊔ update (β := α) f i b) =
  Icc (update (β := α) f i a ⊓ update (β := α) f i b) (update (β := α) f i a ⊔ update (β := α) f i b)
Tactic: simp_rw [uIcc, update_sup, update_inf]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
have simp_rw : Eq (α := Set ((i : ι) → α i))
  ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
    {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
  (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
Tactic: simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right,
    ← setOf_or, le_or_gt, setOf_true, univ_inter]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
simp_rw :
  Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
⊢ Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
have simp_rw₁ : Eq (α := Set ((i : ι) → α i))
  (({z : (i : ι) → α i | z i₀ ≤ m} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i)) ∪
    {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
  (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
Tactic: simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right,
    ← setOf_or, le_or_gt, setOf_true, univ_inter]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
simp_rw :
  Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₁ :
  Eq (α := Set ((i : ι) → α i))
    (({z : (i : ι) → α i | z i₀ ≤ m} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i)) ∪
      {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
⊢ Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
have simp_rw₂ : Eq (α := Set ((i : ι) → α i))
  (({z : (i : ι) → α i | z i₀ ≤ m} ∪ {z : (i : ι) → α i | m < z i₀}) ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
  (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
Tactic: simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right,
    ← setOf_or, le_or_gt, setOf_true, univ_inter]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
simp_rw :
  Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₁ :
  Eq (α := Set ((i : ι) → α i))
    (({z : (i : ι) → α i | z i₀ ≤ m} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i)) ∪
      {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₂ :
  Eq (α := Set ((i : ι) → α i))
    (({z : (i : ι) → α i | z i₀ ≤ m} ∪ {z : (i : ι) → α i | m < z i₀}) ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
⊢ Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
have simp_rw₃ : Eq (α := Set ((i : ι) → α i))
  ({a : (i : ι) → α i | a i₀ ≤ m ∨ m < a i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
  (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
Tactic: simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right,
    ← setOf_or, le_or_gt, setOf_true, univ_inter]