awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
x y : (i : ι) → α i
inst_1 : Nonempty ι
⊢ (pi (α := α) univ fun (i : ι) ↦ Ioo (x i) (y i)) ⊆ Ioo x y

Tactic:
fun _ hx ↦
  ⟨(pi_univ_Ioi_subset _) fun i hi ↦ (hx i hi).1, (pi_univ_Iio_subset _) fun i hi ↦ (hx i hi).2⟩

Premises used: Set.Mem, setOf, Set.Subset, And.right, And.left, Set.pi_univ_Ioi_subset, And.intro, Set.Ioo, Set.pi_univ_Iio_subset
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
x y : (i : ι) → α i
inst_1 : Nonempty ι
⊢ (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i)) ⊆ Ioc x y

Tactic:
fun _ hx ↦
  ⟨(pi_univ_Ioi_subset _) fun i hi ↦ (hx i hi).1, fun i ↦ (hx i trivial).2⟩

Premises used: Set.Ioc, trivial, Set.Mem, setOf, Set.Subset, And.right, And.left, Set.pi_univ_Ioi_subset, And.intro
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
rw : Ioi m ∩ Iic (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
rw₁ : Ioi m ∩ Iic (y i₀) = Ioi m ∩ (Ioi (x i₀) ∩ Iic (y i₀))
rw₂ : Ioi m ∩ Iic (y i₀) = Ioi m ∩ Ioi (x i₀) ∩ Iic (y i₀)
rw₃ rw₄ : Ioi m ∩ Iic (y i₀) = Ioi m ∩ Iic (y i₀)
⊢ Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
      inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]

Premises used: Set.Ioi_inter_Iic, Set.Ioi_subset_Ioi, Set.inter_assoc, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)

Tactic:
have : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀) := by
    rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
      inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
simp_rw :
  Eq (α := Set ((i : ι) → α i))
    ({x_1 : (i : ι) → α i | x_1 i₀ ∈ Ioi m ∩ Ioc (x i₀) (y i₀)} ∩ pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))
    ({z : (i : ι) → α i | m < z i₀} ∩ {x_1 : (i : ι) → α i | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩
      pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))
⊢ Eq (α := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i))
    ({z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))

Tactic:
simp_rw [univ_pi_update i₀ _ _ fun i z ↦ Ioc z (y i), ← pi_inter_compl ({i₀} : Set ι),
    singleton_pi', ← inter_assoc, this]

Premises used: Set.Ioc, Set.singleton_pi', Set.univ_pi_update, Set.pi_inter_compl, Singleton.singleton, Set.inter_assoc
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ Eq (α := Set ((i : ι) → α i))
    ({x_1 : (i : ι) → α i | x_1 i₀ ∈ Ioi m ∩ Ioc (x i₀) (y i₀)} ∩ pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))
    ({z : (i : ι) → α i | m < z i₀} ∩ {x_1 : (i : ι) → α i | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩
      pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
rw : Ioi (x i₀) ∩ Iic m = Iic m ∩ Ioc (x i₀) (y i₀)
rw₁ : Ioi (x i₀) ∩ Iic m = Iic m ∩ (Ioi (x i₀) ∩ Iic (y i₀))
rw₂ : Ioi (x i₀) ∩ Iic m = Ioi (x i₀) ∩ (Iic m ∩ Iic (y i₀))
rw₃ rw₄ : Ioi (x i₀) ∩ Iic m = Ioi (x i₀) ∩ Iic m
⊢ Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]

Premises used: Iff.mpr, Set.Ioi_inter_Iic, Set.Iic_subset_Iic, Set.inter_left_comm, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)

Tactic:
have : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀) := by
    rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
simp_rw :
  Eq (α := Set ((i : ι) → α i))
    ({x_1 : (i : ι) → α i | x_1 i₀ ∈ Iic m ∩ Ioc (x i₀) (y i₀)} ∩ pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))
    ({z : (i : ι) → α i | z i₀ ≤ m} ∩ {x_1 : (i : ι) → α i | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩
      pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))
⊢ Eq (α := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i))
    ({z : (i : ι) → α i | z i₀ ≤ m} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))

Tactic:
simp_rw [univ_pi_update i₀ y m fun i z ↦ Ioc (x i) z, ← pi_inter_compl ({i₀} : Set ι),
    singleton_pi', ← inter_assoc, this]

Premises used: Set.Ioc, Set.singleton_pi', Set.univ_pi_update, Set.pi_inter_compl, Singleton.singleton, Set.inter_assoc
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ Eq (α := Set ((i : ι) → α i))
    ({x_1 : (i : ι) → α i | x_1 i₀ ∈ Iic m ∩ Ioc (x i₀) (y i₀)} ∩ pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))
    ({z : (i : ι) → α i | z i₀ ≤ m} ∩ {x_1 : (i : ι) → α i | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩
      pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
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)
⊢ 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))

Tactic:
rw [disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Order.Interval.Set.Pi
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

Tactic:
(h₁ i₀ (mem_univ _)).2.not_gt ?_

Premises used: And.right, LE.le.not_gt, Set.mem_univ
-- Module: Mathlib.Order.Interval.Set.Pi
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
refine : update (β := α) y i₀ m i₀ < z i₀
⊢ False

Tactic:
refine (h₁ i₀ (mem_univ _)).2.not_gt ?_

Premises used: And.right, LE.le.not_gt, Set.mem_univ
-- Module: Mathlib.Order.Interval.Set.Pi
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
⊢ update (β := α) y i₀ m i₀ < z i₀

Tactic:
simpa only [Function.update_self] using (h₂ i₀ (mem_univ _)).1

Premises used: And.left, Set.mem_univ, Function.update_self
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
h : ∀ (x : (a : ι) → α a), x ∈ update (β := α) f i '' Icc a b ↔ x ∈ Icc (update (β := α) f i a) (update (β := α) f i b)
⊢ update (β := α) f i '' Icc a b = Icc (update (β := α) f i a) (update (β := α) f i b)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.Pi
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 ↔ x ∈ Icc (update (β := α) f i a) (update (β := α) f i b)

Tactic:
rw [← Set.pi_univ_Icc]

Premises used: Set.pi_univ_Icc
-- Module: Mathlib.Order.Interval.Set.Pi
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

Tactic:
⟨?_, fun h => ⟨x i, ?_, ?_⟩⟩

Premises used: And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Order.Interval.Set.Pi
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
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
⊢ 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, ?_, ?_⟩⟩
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b c : α i
hc : c ∈ 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))
    (update (β := α) f i c)

Tactic:
simpa [update_le_update_iff]

Premises used: update_le_update_iff
-- Module: Mathlib.Order.Interval.Set.Pi
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
⊢ x i ∈ Icc a b

Tactic:
simpa only [Function.update_self] using h i (mem_univ i)

Premises used: Set.mem_univ, Function.update_self
-- Module: Mathlib.Order.Interval.Set.Pi
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
h₁ : ∀ (j : ι), update (β := α) f i (x i) j = x j
⊢ update (β := α) f i (x i) = x

Tactic:
ext j
-- Module: Mathlib.Order.Interval.Set.Pi
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
h₂ : ∀ (hij : i ≠ j), update (β := α) f i (x i) j = x j
⊢ update (β := α) f i (x i) j = x j

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Order.Interval.Set.Pi
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) i = x i

Tactic:
Function.update_self ..

Premises used: Function.update_self
-- Module: Mathlib.Order.Interval.Set.Pi
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) i = x i

Tactic:
exact Function.update_self ..

Premises used: Function.update_self
-- Module: Mathlib.Order.Interval.Set.Pi
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 : ι
hij : i ≠ j
⊢ update (β := α) f i (x i) j = x j

Tactic:
simpa only [Function.update_of_ne hij.symm, le_antisymm_iff] using h j (mem_univ j)

Premises used: Ne.symm, le_antisymm_iff, Set.mem_univ, Function.update_of_ne
-- Module: Mathlib.Order.Interval.Set.Pi
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}
rw₄ 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}
⊢ update (β := α) f i '' Ico a 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]

Premises used: Set.image_singleton, Set.image_update_Icc, Set.image_diff, Set.Icc_diff_right, Function.update_injective
-- Module: Mathlib.Order.Interval.Set.Pi
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}
rw₄ 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}
⊢ update (β := α) f i '' Ioc a b = 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]

Premises used: Set.image_singleton, Set.image_update_Icc, Set.image_diff, Set.Icc_diff_left, Function.update_injective
-- Module: Mathlib.Order.Interval.Set.Pi
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}
rw₄ 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}
⊢ update (β := α) f i '' Ioo a b = 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]

Premises used: Set.image_singleton, Set.image_diff, Function.update_injective, Set.image_update_Ico, Set.Ico_diff_left
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update (β := α) f i '' Icc a (f i) = Icc (update (β := α) f i a) f

Tactic:
simpa using image_update_Icc f i a (f i)

Premises used: Set.image_update_Icc
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update (β := α) f i '' Ico a (f i) = Ico (update (β := α) f i a) f

Tactic:
simpa using image_update_Ico f i a (f i)

Premises used: Set.image_update_Ico
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update (β := α) f i '' Ioc a (f i) = Ioc (update (β := α) f i a) f

Tactic:
simpa using image_update_Ioc f i a (f i)

Premises used: Set.image_update_Ioc
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update (β := α) f i '' Ioo a (f i) = Ioo (update (β := α) f i a) f

Tactic:
simpa using image_update_Ioo f i a (f i)

Premises used: Set.image_update_Ioo
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update (β := α) f i '' Icc (f i) b = Icc f (update (β := α) f i b)

Tactic:
simpa using image_update_Icc f i (f i) b

Premises used: Set.image_update_Icc
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update (β := α) f i '' Ico (f i) b = Ico f (update (β := α) f i b)

Tactic:
simpa using image_update_Ico f i (f i) b

Premises used: Set.image_update_Ico
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update (β := α) f i '' Ioc (f i) b = Ioc f (update (β := α) f i b)

Tactic:
simpa using image_update_Ioc f i (f i) b

Premises used: Set.image_update_Ioc
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update (β := α) f i '' Ioo (f i) b = Ioo f (update (β := α) f i b)

Tactic:
simpa using image_update_Ioo f i (f i) b

Premises used: Set.image_update_Ioo
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
a b : α i
⊢ Pi.mulSingle (M := α) i '' Icc a b = Icc (Pi.mulSingle (M := α) i a) (Pi.mulSingle (M := α) i b)

Tactic:
image_update_Icc _ _ _ _

Premises used: Set.image_update_Icc, Pi.mulSingle
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
a b : α i
⊢ Pi.mulSingle (M := α) i '' Ico a b = Ico (Pi.mulSingle (M := α) i a) (Pi.mulSingle (M := α) i b)

Tactic:
image_update_Ico _ _ _ _

Premises used: Set.image_update_Ico, Pi.mulSingle
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
a b : α i
⊢ Pi.mulSingle (M := α) i '' Ioc a b = Ioc (Pi.mulSingle (M := α) i a) (Pi.mulSingle (M := α) i b)

Tactic:
image_update_Ioc _ _ _ _

Premises used: Set.image_update_Ioc, Pi.mulSingle
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
a b : α i
⊢ Pi.mulSingle (M := α) i '' Ioo a b = Ioo (Pi.mulSingle (M := α) i a) (Pi.mulSingle (M := α) i b)

Tactic:
image_update_Ioo _ _ _ _

Premises used: Set.image_update_Ioo, Pi.mulSingle
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
a : α i
⊢ Pi.mulSingle (M := α) i '' Icc a 1 = Icc (Pi.mulSingle (M := α) i a) 1

Tactic:
image_update_Icc_left _ _ _

Premises used: Set.image_update_Icc_left, Pi.mulSingle
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
a : α i
⊢ Pi.mulSingle (M := α) i '' Ico a 1 = Ico (Pi.mulSingle (M := α) i a) 1

Tactic:
image_update_Ico_left _ _ _

Premises used: Set.image_update_Ico_left, Pi.mulSingle
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
a : α i
⊢ Pi.mulSingle (M := α) i '' Ioc a 1 = Ioc (Pi.mulSingle (M := α) i a) 1

Tactic:
image_update_Ioc_left _ _ _

Premises used: Set.image_update_Ioc_left, Pi.mulSingle
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
a : α i
⊢ Pi.mulSingle (M := α) i '' Ioo a 1 = Ioo (Pi.mulSingle (M := α) i a) 1

Tactic:
image_update_Ioo_left _ _ _

Premises used: Set.image_update_Ioo_left, Pi.mulSingle
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
b : α i
⊢ Pi.mulSingle (M := α) i '' Icc 1 b = Icc 1 (Pi.mulSingle (M := α) i b)

Tactic:
image_update_Icc_right _ _ _

Premises used: Pi.mulSingle, Set.image_update_Icc_right
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
b : α i
⊢ Pi.mulSingle (M := α) i '' Ico 1 b = Ico 1 (Pi.mulSingle (M := α) i b)

Tactic:
image_update_Ico_right _ _ _

Premises used: Set.image_update_Ico_right, Pi.mulSingle
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : (i : ι) → One (α i)
i : ι
b : α i
⊢ Pi.mulSingle (M := α) i '' Ioc 1 b = Ioc 1 (Pi.mulSingle (M := α) i b)

Tactic:
image_update_Ioc_right _ _ _

Premises used: Set.image_update_Ioc_right, Pi.mulSingle