awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hac : a ≤ c
hbc : b ≤ c
⊢ f a = f b

Tactic:
le_antisymm ((hf ha hc hac).trans <| hf' hb hc hbc) ((hf hb hc hbc).trans <| hf' ha hc hac)

Premises used: le_antisymm, LE.le.trans
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hac : a ≤ c
hbc : b ≤ c
⊢ f a = f b

Tactic:
exact le_antisymm ((hf ha hc hac).trans <| hf' hb hc hbc) ((hf hb hc hbc).trans <| hf' ha hc hac)

Premises used: le_antisymm, LE.le.trans
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
κ : Sort u_4
r r' s : α → α → Prop
inst : SemilatticeSup α
⊢ IsDirectedOrder α

Tactic:
⟨fun a b => ⟨a ⊔ b, le_sup_left, le_sup_right⟩⟩

Premises used: le_sup_left, le_sup_right, IsDirected.mk, Max.max, And.intro, Exists.intro
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
κ : Sort u_4
r r' s : α → α → Prop
inst : LE α
inst_1 : OrderTop α
⊢ IsDirectedOrder α

Tactic:
⟨fun _ _ => ⟨⊤, le_top _, le_top _⟩⟩

Premises used: OrderTop.le_top, IsDirected.mk, And.intro, Exists.intro, Top.top
-- Module: Mathlib.Order.Directed
Goal:
ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : Set ((i : ι) → α i)
hd : DirectedOn (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) d
i : ι
⊢ DirectedOn (r i) ((fun (a : (i : ι) → α i) ↦ a i) '' d)

Tactic:
DirectedOn.mono_comp (fun _ _ h => h) (mono hd fun ⦃_ _⦄ h ↦ h i)

Premises used: DirectedOn.mono_comp, DirectedOn.mono
-- Module: Mathlib.Order.Directed
Goal:
ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.pi (α := α) Set.univ d
b : (i : ι) → α i
hb : b ∈ Set.pi (α := α) Set.univ d
choose :
  ∀ (f : (i : ι) → α i) (hfd : ∀ (i : ι), f i ∈ d i) (haf : ∀ (i : ι), r i (a i) (f i))
    (hbf : ∀ (i : ι), r i (b i) (f i)),
    ∃ z ∈ Set.pi (α := α) Set.univ d,
      (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧
        (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) b z
⊢ ∃ z ∈ Set.pi (α := α) Set.univ d,
    (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧
      (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) b z

Tactic:
choose f hfd haf hbf using fun i => hd i (a i) (ha i trivial) (b i) (hb i trivial)

Premises used: trivial
-- Module: Mathlib.Order.Directed
Goal:
ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.pi (α := α) Set.univ d
b : (i : ι) → α i
hb : b ∈ Set.pi (α := α) Set.univ d
f : (i : ι) → α i
hfd : ∀ (i : ι), f i ∈ d i
haf : ∀ (i : ι), r i (a i) (f i)
hbf : ∀ (i : ι), r i (b i) (f i)
⊢ ∃ z ∈ Set.pi (α := α) Set.univ d,
    (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧
      (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) b z

Tactic:
⟨f, fun i _ => hfd i, haf, hbf⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Directed
Goal:
ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.pi (α := α) Set.univ d
b : (i : ι) → α i
hb : b ∈ Set.pi (α := α) Set.univ d
f : (i : ι) → α i
hfd : ∀ (i : ι), f i ∈ d i
haf : ∀ (i : ι), r i (a i) (f i)
hbf : ∀ (i : ι), r i (b i) (f i)
⊢ ∃ z ∈ Set.pi (α := α) Set.univ d,
    (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧
      (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) b z

Tactic:
exact ⟨f, fun i _ => hfd i, haf, hbf⟩
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r₂ : β → β → Prop
d : Set (α × β)
hd : DirectedOn (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) d
⊢ DirectedOn (fun (x1 x2 : α) ↦ r x1 x2) (Prod.fst '' d)

Tactic:
DirectedOn.mono_comp (fun ⦃_ _⦄ h ↦ h) (mono hd fun ⦃_ _⦄ h ↦ h.1)

Premises used: DirectedOn.mono_comp, DirectedOn.mono, And.left
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r₂ : β → β → Prop
d : Set (α × β)
hd : DirectedOn (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) d
⊢ DirectedOn (fun (x1 x2 : β) ↦ r₂ x1 x2) (Prod.snd '' d)

Tactic:
DirectedOn.mono_comp (fun ⦃_ _⦄ h ↦ h) (mono hd fun ⦃_ _⦄ h ↦ h.2)

Premises used: DirectedOn.mono_comp, DirectedOn.mono, And.right
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r₂ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun (x1 x2 : α) ↦ r x1 x2) d₁
h₂ : DirectedOn (fun (x1 x2 : β) ↦ r₂ x1 x2) d₂
x : α × β
hpd : x ∈ d₁ ×ˢ d₂
x_1 : α × β
hqd : x_1 ∈ d₁ ×ˢ d₂
obtain :
  ∀ (r₁ : α) (hdr₁ : r₁ ∈ d₁) (hpr₁ : r x.1 r₁) (hqr₁ : r x_1.1 r₁),
    ∃ z ∈ d₁ ×ˢ d₂,
      (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x z ∧ (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x_1 z
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x z ∧ (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x_1 z

Tactic:
obtain ⟨r₁, hdr₁, hpr₁, hqr₁⟩ := h₁ _ hpd.1 _ hqd.1

Premises used: And.left
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r₂ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun (x1 x2 : α) ↦ r x1 x2) d₁
h₂ : DirectedOn (fun (x1 x2 : β) ↦ r₂ x1 x2) d₂
x : α × β
hpd : x ∈ d₁ ×ˢ d₂
x_1 : α × β
hqd : x_1 ∈ d₁ ×ˢ d₂
r₁ : α
hdr₁ : r₁ ∈ d₁
hpr₁ : r x.1 r₁
hqr₁ : r x_1.1 r₁
obtain :
  ∀ (r₂_1 : β) (hdr₂ : r₂_1 ∈ d₂) (hpr₂ : r₂ x.2 r₂_1) (hqr₂ : r₂ x_1.2 r₂_1),
    ∃ z ∈ d₁ ×ˢ d₂,
      (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x z ∧ (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x_1 z
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x z ∧ (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x_1 z

Tactic:
obtain ⟨r₂, hdr₂, hpr₂, hqr₂⟩ := h₂ _ hpd.2 _ hqd.2

Premises used: And.right
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r₂_1 : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun (x1 x2 : α) ↦ r x1 x2) d₁
h₂ : DirectedOn (fun (x1 x2 : β) ↦ r₂_1 x1 x2) d₂
x : α × β
hpd : x ∈ d₁ ×ˢ d₂
x_1 : α × β
hqd : x_1 ∈ d₁ ×ˢ d₂
r₁ : α
hdr₁ : r₁ ∈ d₁
hpr₁ : r x.1 r₁
hqr₁ : r x_1.1 r₁
r₂ : β
hdr₂ : r₂ ∈ d₂
hpr₂ : r₂_1 x.2 r₂
hqr₂ : r₂_1 x_1.2 r₂
⊢ ∃ z ∈ d₁ ×ˢ d₂,
    (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂_1 p.2 q.2) x z ∧ (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂_1 p.2 q.2) x_1 z

Tactic:
⟨⟨r₁, r₂⟩, ⟨hdr₁, hdr₂⟩, ⟨hpr₁, hpr₂⟩, ⟨hqr₁, hqr₂⟩⟩

Premises used: Prod.mk, And.intro, Exists.intro
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r₂_1 : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun (x1 x2 : α) ↦ r x1 x2) d₁
h₂ : DirectedOn (fun (x1 x2 : β) ↦ r₂_1 x1 x2) d₂
x : α × β
hpd : x ∈ d₁ ×ˢ d₂
x_1 : α × β
hqd : x_1 ∈ d₁ ×ˢ d₂
r₁ : α
hdr₁ : r₁ ∈ d₁
hpr₁ : r x.1 r₁
hqr₁ : r x_1.1 r₁
r₂ : β
hdr₂ : r₂ ∈ d₂
hpr₂ : r₂_1 x.2 r₂
hqr₂ : r₂_1 x_1.2 r₂
⊢ ∃ z ∈ d₁ ×ˢ d₂,
    (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂_1 p.2 q.2) x z ∧ (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂_1 p.2 q.2) x_1 z

Tactic:
exact ⟨⟨r₁, r₂⟩, ⟨hdr₁, hdr₂⟩, ⟨hpr₁, hpr₂⟩, ⟨hqr₁, hqr₂⟩⟩
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
i : ι
x : F i
⊢ (f i i ⋯ : (a : F i) → F i) x = x

Tactic:
DirectedSystem.map_self (f := (f · · ·)) x

Premises used: DirectedSystem.map_self
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
i j k : ι
hij : i ≤ j
hjk : j ≤ k
x : F i
⊢ Eq (α := F k) ((f j k hjk : (a : F j) → F k) ((f i j hij : (a : F i) → F j) x : F j) : F k)
    ((f i k ⋯ : (a : F i) → F k) x : F k)

Tactic:
DirectedSystem.map_map (f := (f · · ·)) hij hjk x

Premises used: DirectedSystem.map_map
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
x : (i : ι) × F i
i : ι
h : x.fst (β := fun (i : ι) ↦ F i) ≤ i
⊢ (setoid f : (i : ι) × F i → (i : ι) × F i → Prop) x
    (Sigma.mk (β := fun (i : ι) ↦ F i) i
      ((f (x.fst (β := fun (i : ι) ↦ F i)) i h : (a : F x.fst) → F i) (x.snd (β := fun (i : ι) ↦ F i))))

Tactic:
⟨i, h, le_rfl, (map_map' _ _ _ _).symm⟩

Premises used: le_rfl, DirectedSystem.map_map', Exists.intro, Eq.symm
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
x : (i : ι) × F i
i : ι
h : x.fst (β := fun (i : ι) ↦ F i) ≤ i
⊢ Eq (α := Quotient (α := (i : ι) × F i) (setoid (F := F) (T := T) f)) ⟦x⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i
        ((f (x.fst (β := fun (i : ι) ↦ F i)) i h : (a : F x.fst) → F i) (x.snd (β := fun (i : ι) ↦ F i)))⟧

Tactic:
Quotient.sound (r_of_le _ x i h)

Premises used: DirectLimit.r_of_le, Quotient.sound
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
i j : ι
x : F i
h : i ≤ j
⊢ Eq (α := Quotient (α := (i : ι) × F i) (setoid (F := F) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ F i) j ((f i j h : (a : F i) → F j) x)⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧

Tactic:
eq_of_le ⟨_, x⟩ j h |>.symm

Premises used: DirectLimit.eq_of_le, Sigma.mk, Eq.symm
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
C : DirectLimit F (T := T) f → Prop
ih : ∀ (i : ι) (x : F i), C ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧
x : DirectLimit F (T := T) f
⊢ C x

Tactic:
Quotient.ind (fun _ ↦ ih _ _) x

Premises used: Sigma.fst, Quotient.ind, Sigma.snd
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
z : DirectLimit F (T := T) f
mk :
  ∀ (a : (i : ι) × F i),
    ∃ (i : ι) (x : F i),
      Eq (α := DirectLimit F (T := T) f) (Quot.mk (⇑(setoid f) : (i : ι) × F i → (i : ι) × F i → Prop) a)
        ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧
⊢ ∃ (i : ι) (x : F i), z = ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧

Tactic:
rcases z
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
z : DirectLimit F (T := T) f
a : (i : ι) × F i
⊢ ∃ (i : ι) (x : F i),
    Eq (α := DirectLimit F (T := T) f) (Quot.mk (⇑(setoid f) : (i : ι) × F i → (i : ι) × F i → Prop) a)
      ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧

Tactic:
⟨_, _, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
z : DirectLimit F (T := T) f
a : (i : ι) × F i
⊢ ∃ (i : ι) (x : F i),
    Eq (α := DirectLimit F (T := T) f) (Quot.mk (⇑(setoid f) : (i : ι) × F i → (i : ι) × F i → Prop) a)
      ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧

Tactic:
exact ⟨_, _, rfl⟩
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
z w : DirectLimit F (T := T) f
⊢ ∃ (i : ι) (x : F i) (y : F i),
    z = ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧ ∧ w = ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧

Tactic:
z.inductionOn₂ w fun x y ↦
    have ⟨i, hxi, hyi⟩ := exists_ge_ge x.1 y.1
    ⟨i, _, _, eq_of_le x i hxi, eq_of_le y i hyi⟩

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
w u v : DirectLimit F (T := T) f
⊢ ∃ (i : ι) (x : F i) (y : F i) (z : F i),
    w = ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧ ∧
      u = ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧ ∧ v = ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i z⟧

Tactic:
w.inductionOn₃ u v fun x y z ↦
    have ⟨i, hxi, hyi, hzi⟩ := directed_of₃ (· ≤ ·) x.1 y.1 z.1
    ⟨i, _, _, _, eq_of_le x i hxi, eq_of_le y i hyi, eq_of_le z i hzi⟩

Premises used: Quotient.inductionOn₃
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
C : DirectLimit F (T := T) f → DirectLimit F (T := T) f → Prop
ih : ∀ (i : ι) (x y : F i), C ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧
x y : DirectLimit F (T := T) f
obtain :
  ∀ (w : ι) (w_1 w_2 : F w), C ⟦Sigma.mk (β := fun (i : ι) ↦ F i) w w_1⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) w w_2⟧
⊢ C x y

Tactic:
obtain ⟨_, _, _, rfl, rfl⟩ := exists_eq_mk₂ f x y

Premises used: DirectLimit.exists_eq_mk₂, rfl
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
C : DirectLimit F (T := T) f → DirectLimit F (T := T) f → Prop
ih : ∀ (i : ι) (x y : F i), C ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧
w : ι
w_1 w_2 : F w
⊢ C ⟦Sigma.mk (β := fun (i : ι) ↦ F i) w w_1⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) w w_2⟧

Tactic:
apply ih
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
C : DirectLimit F (T := T) f → DirectLimit F (T := T) f → DirectLimit F (T := T) f → Prop
ih :
  ∀ (i : ι) (x y z : F i),
    C ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i z⟧
x y z : DirectLimit F (T := T) f
obtain :
  ∀ (w : ι) (w_1 w_2 w_3 : F w),
    C ⟦Sigma.mk (β := fun (i : ι) ↦ F i) w w_1⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) w w_2⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ F i) w w_3⟧
⊢ C x y z

Tactic:
obtain ⟨_, _, _, _, rfl, rfl, rfl⟩ := exists_eq_mk₃ f x y z

Premises used: rfl, DirectLimit.exists_eq_mk₃
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
C : DirectLimit F (T := T) f → DirectLimit F (T := T) f → DirectLimit F (T := T) f → Prop
ih :
  ∀ (i : ι) (x y z : F i),
    C ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i z⟧
w : ι
w_1 w_2 w_3 : F w
⊢ C ⟦Sigma.mk (β := fun (i : ι) ↦ F i) w w_1⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) w w_2⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ F i) w w_3⟧

Tactic:
apply ih
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
h :
  ∀ (i j : ι) (hij : i ≤ j),
    Function.Injective.{u_4 + 1, u_4 + 1} (α := F i) (β := F j) (⇑(f i j hij) : (a : F i) → F j)
i : ι
⊢ Function.Injective (β := Quotient (α := (i : ι) × F i) (setoid (F := F) (T := T) f)) fun (x : F i) ↦
    ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧

Tactic:
fun _ _ eq ↦ have ⟨_, _, _, eq⟩ := Quotient.eq.mp eq; h _ _ _ eq

Premises used: _private.0.DirectLimit.mk_injective.match_1, Iff.mp, Function.Injective, Eq, Quotient.eq
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
ih : (i : ι) → F i
compat : ∀ (i j : ι) (h : i ≤ j), (f i j h : (a : F i) → F j) (ih i) = ih j
i : ι
⊢ Eq (α := DirectLimit F (T := T) f) (map₀ (F := F) (T := T) f ih) ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i (ih i)⟧

Tactic:
have ⟨j, hcj, hij⟩ := exists_ge_ge (Classical.arbitrary ι) i
  Quotient.sound ⟨j, hcj, hij, (compat ..).trans (compat ..).symm⟩

Premises used: DirectLimit.setoid, Sigma.fst, Quotient.mk, DirectLimit.map₀, exists_ge_ge, _private.0.DirectLimit.map₀_def.match_1, Exists.intro, Classical.arbitrary, Sigma.mk, Quotient.sound, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_6, u_2 + 1, u_2 + 1} (T₁ h) (F₁ i) (F₁ j)
inst_2 : DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₁ x1 x2 x3) : (a : F₁ x1) → F₁ x2)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_7, u_3 + 1, u_3 + 1} (T₂ h) (F₂ i) (F₂ j)
inst_4 : DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₂ x1 x2 x3) : (a : F₂ x1) → F₂ x2)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_6 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_7 : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h : (a : F i) → F j) x)
z : DirectLimit F (T := T) f
x y : (i : ι) × F i
h : x ≈ y
k : ι
hxk : x.fst (β := fun (i : ι) ↦ F i) ≤ k
hyk : y.fst (β := fun (i : ι) ↦ F i) ≤ k
eq :
  Eq (α := F k)
    ((f (x.fst (β := fun (i : ι) ↦ F i)) k hxk : (a : F x.fst) → F k) (x.snd (β := fun (i : ι) ↦ F i)) : F k)
    ((f (y.fst (β := fun (i : ι) ↦ F i)) k hyk : (a : F y.fst) → F k) (y.snd (β := fun (i : ι) ↦ F i)) : F k)
simp_rw simp_rw₁ :
  @Eq.rec _ _ (fun (x_1 : Quotient (α := (i : ι) × F i) (setoid (F := F) (T := T) f)) (x : ⟦x⟧ = x_1) ↦ C)
      (ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i))) ⟦y⟧ ⋯ =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
simp_rw₂ :
  ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i)) =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
simp_rw₃ :
  ih k ((f (x.fst (β := fun (i : ι) ↦ F i)) k hxk : (a : F x.fst) → F k) (x.snd (β := fun (i : ι) ↦ F i))) =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
simp_rw₄ :
  ih k ((f (x.fst (β := fun (i : ι) ↦ F i)) k hxk : (a : F x.fst) → F k) (x.snd (β := fun (i : ι) ↦ F i))) =
    ih k ((f (y.fst (β := fun (i : ι) ↦ F i)) k hyk : (a : F y.fst) → F k) (y.snd (β := fun (i : ι) ↦ F i)))
⊢ Eq.ndrec (a := ⟦x⟧) (motive := fun (x : DirectLimit F (T := T) f) ↦ C)
      (ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i))) (b := ⟦y⟧) ⋯ =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))

Tactic:
simp_rw [eq_rec_constant, compat _ _ hxk, compat _ _ hyk, eq]

Premises used: eq_rec_constant
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h : (a : F i) → F j) x)
x : (i : ι) × F i
⊢ DirectLimit.lift (F := F) (T := T) f ih compat ⟦x⟧ =
    ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i))

Tactic:
rfl

Premises used: DirectLimit.lift, rfl
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h : (a : F i) → F j) x)
h : ∀ (i : ι), Function.Injective (ih i)
i : ι
x y : F i
eq : ih i x = ih i y
rw rw₁ :
  Eq (α := DirectLimit F (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧
⊢ Eq (α := DirectLimit F (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧

Tactic:
rw [h i eq]