awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ ((f : (a : α₁) → β₁) a) ((f : (a : α₁) → β₁) b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ ((g : (a : α₂) → β₂) a) ((g : (a : α₂) → β₂) b) ↔ r₂ a b
val : α₁
inl :
  ∀ (val_1 : α₁),
    Sum.Lex s₁ s₂
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inl val))
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inl val_1)) ↔
      Sum.Lex r₁ r₂ (Sum.inl val) (Sum.inl val_1)
inl₁ :
  ∀ (val_1 : α₂),
    Sum.Lex s₁ s₂
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inl val))
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inr val_1)) ↔
      Sum.Lex r₁ r₂ (Sum.inl val) (Sum.inr val_1)
⊢ Sum.Lex s₁ s₂
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inl val))
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        b) ↔
    Sum.Lex r₁ r₂ (Sum.inl val) b

Tactic:
cases b
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ ((f : (a : α₁) → β₁) a) ((f : (a : α₁) → β₁) b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ ((g : (a : α₂) → β₂) a) ((g : (a : α₂) → β₂) b) ↔ r₂ a b
val : α₂
inr :
  ∀ (val_1 : α₁),
    Sum.Lex s₁ s₂
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inr val))
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inl val_1)) ↔
      Sum.Lex r₁ r₂ (Sum.inr val) (Sum.inl val_1)
inr₁ :
  ∀ (val_1 : α₂),
    Sum.Lex s₁ s₂
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inr val))
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inr val_1)) ↔
      Sum.Lex r₁ r₂ (Sum.inr val) (Sum.inr val_1)
⊢ Sum.Lex s₁ s₂
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inr val))
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        b) ↔
    Sum.Lex r₁ r₂ (Sum.inr val) b

Tactic:
cases b
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ ((f : (a : α₁) → β₁) a) ((f : (a : α₁) → β₁) b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ ((g : (a : α₂) → β₂) a) ((g : (a : α₂) → β₂) b) ↔ r₂ a b
val val_1 : α₁
⊢ Sum.Lex s₁ s₂
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inl val))
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inl val_1)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val) (Sum.inl val_1)

Tactic:
simp [hf, hg]
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ ((f : (a : α₁) → β₁) a) ((f : (a : α₁) → β₁) b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ ((g : (a : α₂) → β₂) a) ((g : (a : α₂) → β₂) b) ↔ r₂ a b
val : α₁
val_1 : α₂
⊢ Sum.Lex s₁ s₂
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inl val))
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inr val_1)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val) (Sum.inr val_1)

Tactic:
simp [hf, hg]
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ ((f : (a : α₁) → β₁) a) ((f : (a : α₁) → β₁) b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ ((g : (a : α₂) → β₂) a) ((g : (a : α₂) → β₂) b) ↔ r₂ a b
val : α₂
val_1 : α₁
⊢ Sum.Lex s₁ s₂
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inr val))
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inl val_1)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val) (Sum.inl val_1)

Tactic:
simp [hf, hg]
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ ((f : (a : α₁) → β₁) a) ((f : (a : α₁) → β₁) b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ ((g : (a : α₂) → β₂) a) ((g : (a : α₂) → β₂) b) ↔ r₂ a b
val val_1 : α₂
⊢ Sum.Lex s₁ s₂
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inr val))
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inr val_1)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val) (Sum.inr val_1)

Tactic:
simp [hf, hg]
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r s₁
e₂ : r₂ ≃r s₂
⊢ ∀ {a b : α₁ × α₂},
    Prod.Lex s₁ s₂
        ((e₁.toEquiv (r := r₁) (s := s₁).prodCongr (e₂.toEquiv (r := r₂) (s := s₂)) : (a : α₁ × α₂) → β₁ × β₂) a)
        ((e₁.toEquiv (r := r₁) (s := s₁).prodCongr (e₂.toEquiv (r := r₂) (s := s₂)) : (a : α₁ × α₂) → β₁ × β₂) b) ↔
      Prod.Lex r₁ r₂ a b

Tactic:
simp [Prod.lex_def, e₁.map_rel_iff, e₂.map_rel_iff,
    e₁.injective.eq_iff]

Premises used: Prod.lex_def, Function.Injective.eq_iff, RelIso.injective, RelIso.map_rel_iff
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsEmpty β
⊢ ∀ {a b : α ⊕ β},
    r ((Equiv.sumEmpty α β : (a : α ⊕ β) → α) a) ((Equiv.sumEmpty α β : (a : α ⊕ β) → α) b) ↔ Sum.Lex r s a b

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsEmpty α
⊢ ∀ {a b : α ⊕ β},
    s ((Equiv.emptySum α β : (a : α ⊕ β) → β) a) ((Equiv.emptySum α β : (a : α ⊕ β) → β) b) ↔ Sum.Lex r s a b

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : SemilatticeInf α
inst_1 : LinearOrder β
inst_2 : FunLike F β α
inst_3 : RelHomClass.{u_3, u_2, u_1} F (α := β) (β := α) (fun (x1 x2 : β) ↦ x1 < x2) fun (x1 x2 : α) ↦ x1 < x2
a : F
m n : β
⊢ Eq.{u_1 + 1} (α := α) ((a : (a : β) → α) (min m n) : α) ((a : (a : β) → α) m ⊓ (a : (a : β) → α) n : α)

Tactic:
(StrictMono.monotone fun _ _ => map_rel a).map_inf m n

Premises used: StrictMono.monotone, RelHomClass.map_rel, Monotone.map_inf
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder β
inst_2 : FunLike F β α
inst_3 : RelHomClass.{u_3, u_2, u_1} F (α := β) (β := α) (fun (x1 x2 : β) ↦ x1 > x2) fun (x1 x2 : α) ↦ x1 > x2
a : F
m n : β
⊢ Eq.{u_1 + 1} (α := α) ((a : (a : β) → α) (max m n) : α) ((a : (a : β) → α) m ⊔ (a : (a : β) → α) n : α)

Tactic:
map_inf (α := αᵒᵈ) (β := βᵒᵈ) _ _ _

Premises used: RelHomClass.map_inf, OrderDual
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_3
inst : FunLike F α β
inst_1 : RelHomClass F r s
ι : Sort u_4
a : ι → α
f : F
ha : Directed r a
⊢ Directed s ((⇑f : (a : α) → β) ∘ a)

Tactic:
ha.mono_comp _ fun _ _ h ↦ map_rel f h

Premises used: Directed.mono_comp, RelHomClass.map_rel
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_3
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
t : Set α
hs : DirectedOn r t
⊢ DirectedOn s ((⇑f : (a : α) → β) '' t)

Tactic:
hs.mono_comp fun _ _ h ↦ map_rel f h

Premises used: DirectedOn.mono_comp, RelHomClass.map_rel
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β)) Set.univ

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
r : α → α → Prop
p : α → Prop
a b : Subtype p
⊢ Subrel r p a b ↔ r (↑a : α) (↑b : α)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Subrel, Order.Preimage
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
r : α → α → Prop
p : α → Prop
a : Subtype p
⊢ (Subrel.relEmbedding r p : (a : Subtype p) → α) a = (↑a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
⊢ (⇑(Subrel.inclusionEmbedding r (s := s) (t := t) h) : (a : { x : α // x ∈ s }) → { x : α // x ∈ t }) =
    Set.inclusion (s := s) (t := t) h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : Std.Refl r
p : α → Prop
⊢ Std.Refl (Subrel r p)

Tactic:
⟨fun x => Std.Refl.refl (r := r) x⟩

Premises used: Std.Refl.refl, Std.Refl.mk, Subtype.val
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : Std.Symm r
p : α → Prop
⊢ Std.Symm (Subrel r p)

Tactic:
⟨fun x y => Std.Symm.symm (r := r) x y⟩

Premises used: Std.Symm.mk, Std.Symm.symm, Subtype.val
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : Std.Asymm r
p : α → Prop
⊢ Std.Asymm (Subrel r p)

Tactic:
⟨fun x y => Std.Asymm.asymm (r := r) x y⟩

Premises used: Std.Asymm.mk, Std.Asymm.asymm, Subtype.val
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsTrans α r
p : α → Prop
⊢ IsTrans (Subtype p) (Subrel r p)

Tactic:
⟨fun x y z => IsTrans.trans (r := r) x y z⟩

Premises used: IsTrans.mk, IsTrans.trans, Subtype.val
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
⊢ Std.Irrefl (Subrel r p)

Tactic:
⟨fun x => Std.Irrefl.irrefl (r := r) x⟩

Premises used: Std.Irrefl.irrefl, Std.Irrefl.mk, Subtype.val
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : Std.Trichotomous r
p : α → Prop
x y : Subtype p
rw : ¬Subrel r p x y → ¬Subrel r p y x → (↑x : α) = (↑y : α)
⊢ ¬Subrel r p x y → ¬Subrel r p y x → x = y

Tactic:
rw [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : Std.Trichotomous r
p : α → Prop
x y : Subtype p
⊢ ¬Subrel r p x y → ¬Subrel r p y x → (↑x : α) = (↑y : α)

Tactic:
@Std.Trichotomous.trichotomous α r _ x y

Premises used: Subrel, Subtype.val, Std.Trichotomous.trichotomous, Order.Preimage
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : Std.Trichotomous r
p : α → Prop
x y : Subtype p
⊢ ¬Subrel r p x y → ¬Subrel r p y x → (↑x : α) = (↑y : α)

Tactic:
exact @Std.Trichotomous.trichotomous α r _ x y

Premises used: Subtype.val, Std.Trichotomous.trichotomous
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellFounded α r
p : α → Prop
⊢ IsWellFounded (Subtype p) (Subrel r p)

Tactic:
(Subrel.relEmbedding r p).isWellFounded

Premises used: Subrel.relEmbedding, RelEmbedding.isWellFounded
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p : α → Prop
h : ∀ (x : α), p x
⊢ ∀ {a b : Subtype p},
    r ((Equiv.subtypeUnivEquiv (p := p) h : (a : Subtype p) → α) a)
        ((Equiv.subtypeUnivEquiv (p := p) h : (a : Subtype p) → α) b) ↔
      Subrel r p a b

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p : Set β
f : r ↪r s
H : ∀ (a : α), Membership.mem (α := β) p ((f : (a : α) → β) a : β)
a : α
⊢ Eq.{u_2 + 1} (α := { x : β // x ∈ p })
    ((codRestrict (r := r) (s := s) p f H : (a : α) → { x : β // x ∈ p }) a : { x : β // x ∈ p })
    (Subtype.mk (p := fun (x : β) ↦ x ∈ p) ((f : (a : α) → β) a) ⋯ : { x : β // x ∈ p })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' t) ((⇑(e.symm (r := r) (s := s)) : (a : β) → α) ⁻¹' t)

Tactic:
e.toEquiv.image_eq_preimage_symm t

Premises used: Equiv.image_eq_preimage_symm, RelIso.toEquiv
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
rw :
  Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' t)
    ((⇑(e.symm (r := r) (s := s).symm (r := s) (s := r)) : (a : α) → β) ⁻¹' t)
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' t) ((⇑(e.symm (r := r) (s := s)) : (a : β) → α) '' t)

Tactic:
rw [e.symm.image_eq_preimage_symm]

Premises used: RelIso.symm, RelIso.image_eq_preimage_symm
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' t)
    ((⇑(e.symm (r := r) (s := s).symm (r := s) (s := r)) : (a : α) → β) ⁻¹' t)

Tactic:
rfl
-- Module: Mathlib.Order.RelIso.Set
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
b : α
a : { a : α // r a b }
h : Acc (Subrel r fun (x : α) ↦ r x b) a
⊢ Acc r (↑a : α)

Tactic:
h.recOn fun a _ IH ↦ ⟨_, fun _ hb ↦ IH ⟨_, _root_.trans hb a.2⟩ hb⟩

Premises used: Acc.recOn
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Nonempty α
⊢ Nonempty.{u_1 + 1} (RelSeries r)

Tactic:
Nonempty.map (singleton r) inferInstance

Premises used: inferInstance, Nonempty.map, RelSeries.singleton
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x y : RelSeries r
length_eq : x.length (r := r) = y.length (r := r)
rw rw₁ : y.length (r := r) + 1 = y.length (r := r) + 1
⊢ x.length (r := r) + 1 = y.length (r := r) + 1

Tactic:
rw [length_eq]
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x y : RelSeries r
length_eq : x.length (r := r) = y.length (r := r)
toFun_eq : x.toFun (r := r) = y.toFun (r := r) ∘ Fin.cast ⋯
rcases :
  ∀ (nx : ℕ) (fx : Fin (nx + 1) → α) (step : ∀ (i : Fin nx), (fx i.castSucc, fx i.succ) ∈ r)
    (length_eq : (mk (r := r) nx fx step).length (r := r) = y.length (r := r))
    (toFun_eq : (mk (r := r) nx fx step).toFun (r := r) = y.toFun (r := r) ∘ Fin.cast ⋯), mk (r := r) nx fx step = y
⊢ x = y

Tactic:
rcases x with ⟨nx, fx⟩
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
y : RelSeries r
nx : ℕ
fx : Fin (nx + 1) → α
step : ∀ (i : Fin nx), (fx i.castSucc, fx i.succ) ∈ r
length_eq : nx = y.length (r := r)
toFun_eq : (mk (r := r) nx fx step).toFun (r := r) = y.toFun (r := r) ∘ Fin.cast ⋯
subst :
  ∀ (fx : Fin (y.length (r := r) + 1) → α) (step : ∀ (i : Fin (y.length (r := r))), (fx i.castSucc, fx i.succ) ∈ r)
    (toFun_eq : (mk (r := r) (y.length (r := r)) fx step).toFun (r := r) = y.toFun (r := r) ∘ Fin.cast ⋯),
    mk (r := r) (y.length (r := r)) fx step = y
⊢ mk (r := r) nx fx step = y

Tactic:
subst length_eq
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
y : RelSeries r
fx : Fin (y.length (r := r) + 1) → α
step : ∀ (i : Fin (y.length (r := r))), (fx i.castSucc, fx i.succ) ∈ r
toFun_eq : (mk (r := r) (y.length (r := r)) fx step).toFun (r := r) = y.toFun (r := r) ∘ Fin.cast ⋯
⊢ mk (r := r) (y.length (r := r)) fx step = y

Tactic:
simp_all
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
inst : r.IsTrans
x : RelSeries r
i j : Fin (x.length (r := r) + 1)
h : i < j
⊢ (x.toFun (r := r) i, x.toFun (r := r) j) ∈ r

Tactic:
(Fin.liftFun_iff_succ (· ~[r] ·)).mpr x.step h

Premises used: Iff.mpr, Fin.liftFun_iff_succ, Membership.mem, Prod.mk, RelSeries.step
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
s : SetRel α α
h : r ≤ s
⊢ (x.ofLE (r := r) (s := s) h).toFun (r := s) = x.toFun (r := r)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ x.toList (r := r).length = x.length (r := r) + 1

Tactic:
List.length_ofFn

Premises used: List.length_ofFn, RelSeries.toList
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : α
⊢ (singleton r x).toList (r := r) = [x]

Tactic:
simp [toList, singleton]

Premises used: RelSeries.toList, RelSeries.singleton
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
simp_rw :
  ∀ (i : ℕ) (_hi : i < x.length (r := r)),
    (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) i ⋯,
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (i + 1) ⋯) ∈
      r
⊢ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) (x.toList (r := r))

Tactic:
simp_rw [List.isChain_iff_getElem, length_toList, add_lt_add_iff_right]

Premises used: List.isChain_iff_getElem, add_lt_add_iff_right, RelSeries.length_toList
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length (r := r)
⊢ i < x.length (r := r)

Tactic:
simpa [toList] using h

Premises used: RelSeries.toList
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length (r := r)
h₁ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) i ⋯ =
    x.toFun (r := r) ⟨i, h⟩.castSucc
h₂ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (i + 1) ⋯ =
    x.toFun (r := r) ⟨i, h⟩.succ
⊢ (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) i ⋯,
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (i + 1) ⋯) ∈
    r

Tactic:
convert! x.step ⟨i, by simpa [toList] using h⟩

Premises used: Fin.mk, RelSeries.step
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length (r := r)
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) i ⋯ =
    x.toFun (r := r) ⟨i, h⟩.castSucc

Tactic:
apply List.get_ofFn

Premises used: List.get_ofFn
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length (r := r)
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x.toList (r := r)) (i + 1) ⋯ =
    x.toFun (r := r) ⟨i, h⟩.succ

Tactic:
apply List.get_ofFn

Premises used: List.get_ofFn
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ x.toList (r := r) ≠ []

Tactic:
fun m =>
  List.eq_nil_iff_forall_not_mem.mp m (x 0) <| List.mem_ofFn.mpr ⟨_, rfl⟩

Premises used: Iff.mpr, List.mem_ofFn, Exists.intro, Iff.mp, RelSeries.toFun, OfNat.ofNat, Not, rfl, List.eq_nil_iff_forall_not_mem
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
⊢ length (r := r)
      ((fun (x : (↑{x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} : Type u_1)) ↦
          fromListIsChain (r := r) (↑x : List α) ⋯ ⋯)
        ((fun (x : RelSeries r) ↦
            (Subtype.mk (p := fun (x : List α) ↦
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x)
                (x.toList (r := r)) ⋯ :
              { x : List α //
                Membership.mem (γ := Set (List α))
                  {x : List α | x ≠ [] ∧ List.IsChain (fun (x1 x2 : α) ↦ (x1, x2) ∈ r) x} x }))
          x)) =
    x.length (r := r)

Tactic:
simp [toList]

Premises used: RelSeries.toList