awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 '' Ioo 1 b = Ioo 1 (Pi.mulSingle (M := α) i b)

Tactic:
image_update_Ioo_right _ _ _

Premises used: Pi.mulSingle, Set.image_update_Ioo_right
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Lattice (α i)
a b : (i : ι) → α i
⊢ (pi (α := α) univ fun (i : ι) ↦ uIcc (a i) (b i)) = uIcc a b

Tactic:
pi_univ_Icc _ _

Premises used: Set.uIcc, Set.pi_univ_Icc
-- Module: Mathlib.Order.Interval.Set.Pi
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)
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)
⊢ Icc (update (β := α) f i (a ⊓ b)) (update (β := α) f i (a ⊔ b)) = uIcc (update (β := α) f i a) (update (β := α) f i b)

Tactic:
simp_rw [uIcc, update_sup, update_inf]

Premises used: Function.update_inf, Set.uIcc, Function.update_sup
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Lattice (α i)
inst_1 : DecidableEq ι
f : (i : ι) → α i
i : ι
a : α i
⊢ update (β := α) f i '' uIcc a (f i) = uIcc (update (β := α) f i a) f

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

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

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

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

Tactic:
image_update_uIcc _ _ _ _

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

Tactic:
image_update_uIcc_left _ _ _

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

Tactic:
image_update_uIcc_right _ _ _

Premises used: Set.image_update_uIcc_right, Pi.mulSingle
-- Module: Mathlib.Order.Interval.Set.Pi
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))
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))
simp_rw₄ :
  Eq (α := Set ((i : ι) → α i)) ({a : (i : ι) → α i | True} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₅ :
  Eq (α := Set ((i : ι) → α i)) (univ ∩ 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))

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]

Premises used: Set.pi_univ_Ioc_update_right, Set.univ_inter, le_or_gt, And.right, And.left, Set.setOf_true, Set.pi_univ_Ioc_update_left, Set.union_inter_distrib_right, Set.setOf_or
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
ha' : a ∉ pi (α := α) univ fun (i : ι) ↦ Ioo (x' i) (y' i)
hxa : x ≤ a
hay : a ≤ y
⊢ ∃ (x : ι), ¬(x' x < a x ∧ a x < y' x)

Tactic:
simp only [mem_pi, mem_univ, mem_Ioo, true_implies, not_forall] at ha'

Premises used: Set.mem_Ioo, Set.mem_pi, true_implies, Set.mem_univ, Classical.not_forall
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ (x : ι), ¬(x' x < a x ∧ a x < y' x)
simp : ∃ (x : ι), (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True
⊢ Membership.mem (γ := Set ((i : ι) → α i))
    ((⋃ (i : ι), Icc x (update (β := α) y i (x' i))) ∪ ⋃ (i : ι), Icc (update (β := α) x i (y' i)) y) a

Tactic:
simp only [le_update_iff, update_le_iff, mem_union, mem_iUnion, mem_Icc,
    hxa, hay _, hxa _, hay, ← exists_or]

Premises used: Set.mem_union, exists_or, Set.mem_iUnion, le_update_iff, update_le_iff, Set.mem_Icc
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ (x : ι), ¬(x' x < a x ∧ a x < y' x)
rcases :
  ∀ (w : ι) (hw : ¬(x' w < a w ∧ a w < y' w)),
    ∃ (x : ι), (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True
⊢ ∃ (x : ι), (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True

Tactic:
rcases ha' with ⟨w, hw⟩
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
apply : (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
⊢ ∃ (x : ι), (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True

Tactic:
apply Exists.intro w

Premises used: Exists.intro
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
inl : x' w < a w → (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
inr : a w ≤ x' w → (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
⊢ (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True

Tactic:
cases lt_or_ge (x' w) (a w)

Premises used: lt_or_ge
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
h : x' w < a w
⊢ (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True

Tactic:
simp_all
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
h : a w ≤ x' w
⊢ (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True

Tactic:
simp_all
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y z a : (i : ι) → α i
hay : a ∉ pi (α := α) univ fun (i : ι) ↦ Ioc (y i) (z i)
hax : x ≤ a
haz : a ≤ z
⊢ Membership.mem (γ := Set ((i : ι) → α i)) (⋃ (i : ι), Icc x (update (β := α) z i (y i))) a

Tactic:
simpa [not_and_or, hax, le_update_iff, haz _] using hay

Premises used: le_update_iff, not_and_or
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a x : α
⊢ (↑(projIci a x) : α) = max a x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b x : α
⊢ (↑(projIic b x) : α) = min b x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
x : α
⊢ (↑(projIcc a b h x) : α) = max a (min b x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a x : α
hx : x ≤ a
⊢ Eq (α := (↑(Ici a) : Type u_1)) (projIci a x) (Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) a ⋯)

Tactic:
Subtype.ext <| max_eq_left hx

Premises used: max_eq_left, Subtype.ext
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b x : α
hx : b ≤ x
⊢ Eq (α := (↑(Iic b) : Type u_1)) (projIic b x) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b ⋯)

Tactic:
Subtype.ext <| min_eq_left hx

Premises used: min_eq_left, Subtype.ext
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ≤ a
⊢ projIcc a b h x = Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯

Tactic:
simp [projIcc, hx, hx.trans h]

Premises used: Set.projIcc, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : b ≤ x
⊢ projIcc a b h x = Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯

Tactic:
simp [projIcc, hx, h]

Premises used: Set.projIcc
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Eq (α := (↑(Ici a) : Type u_1)) (projIci a a) (Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) a ⋯)

Tactic:
projIci_of_le le_rfl

Premises used: le_rfl, Set.projIci_of_le
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b : α
⊢ Eq (α := (↑(Iic b) : Type u_1)) (projIic b b) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b ⋯)

Tactic:
projIic_of_le le_rfl

Premises used: le_rfl, Set.projIic_of_le
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ projIcc a b h a = Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯

Tactic:
projIcc_of_le_left h le_rfl

Premises used: le_rfl, Set.projIcc_of_le_left
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ projIcc a b h b = Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯

Tactic:
projIcc_of_right_le h le_rfl

Premises used: le_rfl, Set.projIcc_of_right_le
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a x : α
⊢ Eq (α := (↑(Ici a) : Type u_1)) (projIci a x) (Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) a ⋯) ↔ x ≤ a

Tactic:
simp [projIci, Subtype.ext_iff]

Premises used: Set.projIci, Subtype.ext_iff
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b x : α
⊢ Eq (α := (↑(Iic b) : Type u_1)) (projIic b x) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b ⋯) ↔ b ≤ x

Tactic:
simp [projIic, Subtype.ext_iff]

Premises used: Subtype.ext_iff, Set.projIic
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b x : α
h : a < b
⊢ projIcc a b ⋯ x = Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯ ↔ x ≤ a

Tactic:
simp [projIcc, Subtype.ext_iff, h.not_ge]

Premises used: Set.projIcc, Subtype.ext_iff, LT.lt.not_ge
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b x : α
h : a < b
⊢ projIcc a b ⋯ x = Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯ ↔ b ≤ x

Tactic:
simp [projIcc, Subtype.ext_iff, max_min_distrib_left, h.le, h.not_ge]

Premises used: Set.projIcc, max_min_distrib_left, LT.lt.le, Subtype.ext_iff, LT.lt.not_ge
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a x : α
hx : x ∈ Ici a
⊢ projIci a x = Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) x hx

Tactic:
simpa [projIci]

Premises used: Set.projIci
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b x : α
hx : x ∈ Iic b
⊢ projIic b x = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) x hx

Tactic:
simpa [projIic]

Premises used: Set.projIic
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ projIcc a b h x = Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) x hx

Tactic:
simp [projIcc, hx.1, hx.2]

Premises used: Set.projIcc, And.right, And.left
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a : α
x : (↑(Ici a) : Type u_1)
mk :
  ∀ (val : α) (property : val ∈ Ici a),
    projIci a (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) val property) : α) =
      Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) val property
⊢ projIci a (↑x : α) = x

Tactic:
cases x
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a val : α
property : val ∈ Ici a
⊢ projIci a (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) val property) : α) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) val property

Tactic:
apply projIci_of_mem

Premises used: Set.projIci_of_mem
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b : α
x : (↑(Iic b) : Type u_1)
mk :
  ∀ (val : α) (property : val ∈ Iic b),
    projIic b (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) val property) : α) =
      Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) val property
⊢ projIic b (↑x : α) = x

Tactic:
cases x
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b val : α
property : val ∈ Iic b
⊢ projIic b (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) val property) : α) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) val property

Tactic:
apply projIic_of_mem

Premises used: Set.projIic_of_mem
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
x : (↑(Icc a b) : Type u_1)
mk :
  ∀ (val : α) (property : val ∈ Icc a b),
    projIcc a b h (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) val property) : α) =
      Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) val property
⊢ projIcc a b h (↑x : α) = x

Tactic:
cases x
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
val : α
property : val ∈ Icc a b
⊢ projIcc a b h (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) val property) : α) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) val property

Tactic:
apply projIcc_of_mem

Premises used: Set.projIcc_of_mem
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ SurjOn (β := (↑(Ici a) : Type u_1)) (projIci a) (Ici a) univ

Tactic:
fun x _ => ⟨x, x.2, projIci_coe x⟩

Premises used: Set.Mem, setOf, Set.SurjOn, Set.Subset, And.intro, Exists.intro, Set.image, Set.projIci_coe, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b : α
⊢ SurjOn (β := (↑(Iic b) : Type u_1)) (projIic b) (Iic b) univ

Tactic:
fun x _ => ⟨x, x.2, projIic_coe x⟩

Premises used: Set.Mem, setOf, Set.SurjOn, Set.projIic_coe, Set.Subset, And.intro, Exists.intro, Set.image, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ SurjOn (projIcc a b h) (Icc a b) univ

Tactic:
fun x _ =>
  ⟨x, x.2, projIcc_val h x⟩

Premises used: Set.Mem, setOf, Set.SurjOn, Set.Subset, And.intro, Set.projIcc_val, Exists.intro, Set.image, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Surjective (β := (↑(Ici a) : Type u_1)) (projIci a)

Tactic:
fun x => ⟨x, projIci_coe x⟩

Premises used: Exists.intro, Set.projIci_coe, Subtype.val, Function.Surjective
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b : α
⊢ Surjective (β := (↑(Iic b) : Type u_1)) (projIic b)

Tactic:
fun x => ⟨x, projIic_coe x⟩

Premises used: Set.projIic_coe, Exists.intro, Subtype.val, Function.Surjective
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Surjective (projIcc a b h)

Tactic:
fun x => ⟨x, projIcc_val h x⟩

Premises used: Set.projIcc_val, Exists.intro, Subtype.val, Function.Surjective
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Eq (α := Set (↑(Ici a) : Type u_1)) (range (projIci a)) univ

Tactic:
projIci_surjective.range_eq

Premises used: Set.projIci_surjective, Function.Surjective.range_eq
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Eq (α := Set (↑(Iic a) : Type u_1)) (range (projIic a)) univ

Tactic:
projIic_surjective.range_eq

Premises used: Set.projIic_surjective, Function.Surjective.range_eq
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ range (projIcc a b h) = univ

Tactic:
(projIcc_surjective h).range_eq

Premises used: Function.Surjective.range_eq, Set.projIcc_surjective
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Monotone (β := (↑(Ici a) : Type u_1)) (projIci a)

Tactic:
fun _ _ => max_le_max le_rfl

Premises used: le_rfl, Monotone, max_le_max
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Monotone (β := (↑(Iic a) : Type u_1)) (projIic a)

Tactic:
fun _ _ => min_le_min le_rfl

Premises used: le_rfl, Monotone, min_le_min
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Monotone (projIcc a b h)

Tactic:
fun _ _ hxy =>
  max_le_max le_rfl <| min_le_min le_rfl hxy

Premises used: le_rfl, Monotone, max_le_max, min_le_min
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a x : α
hx : x ∈ Ici a
y : α
hy : y ∈ Ici a
hxy : x < y
⊢ LT.lt (α := (↑(Ici a) : Type u_1)) (projIci a x) (projIci a y)

Tactic:
simpa only [projIci_of_mem, hx, hy]

Premises used: Set.projIci_of_mem
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b x : α
hx : x ∈ Iic b
y : α
hy : y ∈ Iic b
hxy : x < y
⊢ LT.lt (α := (↑(Iic b) : Type u_1)) (projIic b x) (projIic b y)

Tactic:
simpa only [projIic_of_mem, hx, hy]

Premises used: Set.projIic_of_mem
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
y : α
hy : y ∈ Icc a b
hxy : x < y
⊢ projIcc a b h x < projIcc a b h y

Tactic:
simpa only [projIcc_of_mem, hx, hy]

Premises used: Set.projIcc_of_mem
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a : α
f : (↑(Ici a) : Type u_1) → β
x : α
⊢ IciExtend f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) (max a x) ⋯)

Tactic:
rfl

Premises used: Set.IciExtend, Set.projIci, rfl
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
b : α
f : (↑(Iic b) : Type u_1) → β
x : α
⊢ IicExtend f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (min b x) ⋯)

Tactic:
rfl

Premises used: Set.projIic, Set.IicExtend, rfl
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : (↑(Icc a b) : Type u_1) → β
x : α
⊢ IccExtend h f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (max a (min b x)) ⋯)

Tactic:
rfl

Premises used: Set.projIcc, Set.IccExtend, rfl
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a : α
f : (↑(Ici a) : Type u_1) → β
⊢ range (IciExtend f) = range f

Tactic:
simp only [IciExtend, range_comp f, range_projIci, image_univ]

Premises used: Set.range_comp, Set.image_univ, Set.IciExtend, Set.range_projIci
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
b : α
f : (↑(Iic b) : Type u_1) → β
⊢ range (IicExtend f) = range f

Tactic:
simp only [IicExtend, range_comp f, range_projIic, image_univ]

Premises used: Set.range_comp, Set.image_univ, Set.range_projIic, Set.IicExtend
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : (↑(Icc a b) : Type u_1) → β
⊢ range (IccExtend h f) = range f

Tactic:
simp only [IccExtend, range_comp f, range_projIcc, image_univ]

Premises used: Set.range_comp, Set.image_univ, Set.IccExtend, Set.range_projIcc
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a x : α
f : (↑(Ici a) : Type u_1) → β
hx : x ≤ a
⊢ IciExtend f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) a ⋯)

Tactic:
congr_arg f <| projIci_of_le hx

Premises used: Set.IciExtend, congr_arg, Set.projIci_of_le
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
b x : α
f : (↑(Iic b) : Type u_1) → β
hx : b ≤ x
⊢ IicExtend f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b ⋯)

Tactic:
congr_arg f <| projIic_of_le hx

Premises used: congr_arg, Set.IicExtend, Set.projIic_of_le
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
x : α
f : (↑(Icc a b) : Type u_1) → β
hx : x ≤ a
⊢ IccExtend h f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯)

Tactic:
congr_arg f <| projIcc_of_le_left h hx

Premises used: congr_arg, Set.IccExtend, Set.projIcc_of_le_left
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
x : α
f : (↑(Icc a b) : Type u_1) → β
hx : b ≤ x
⊢ IccExtend h f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯)

Tactic:
congr_arg f <| projIcc_of_right_le h hx

Premises used: Set.projIcc_of_right_le, congr_arg, Set.IccExtend
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a : α
f : (↑(Ici a) : Type u_1) → β
⊢ IciExtend f a = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) a ⋯)

Tactic:
IciExtend_of_le f le_rfl

Premises used: le_rfl, Set.IciExtend_of_le
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
b : α
f : (↑(Iic b) : Type u_1) → β
⊢ IicExtend f b = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b ⋯)

Tactic:
IicExtend_of_le f le_rfl

Premises used: le_rfl, Set.IicExtend_of_le
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : (↑(Icc a b) : Type u_1) → β
⊢ IccExtend h f a = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯)

Tactic:
IccExtend_of_le_left h f le_rfl

Premises used: le_rfl, Set.IccExtend_of_le_left
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : (↑(Icc a b) : Type u_1) → β
⊢ IccExtend h f b = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯)

Tactic:
IccExtend_of_right_le h f le_rfl

Premises used: le_rfl, Set.IccExtend_of_right_le