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
inst : Std.Trichotomous r
inst_1 : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
⊢ ¬r b a

Tactic:
exact fun h => irrefl (r := s) (f b) (by simpa [e] using H _ _ h)

Premises used: irrefl
-- 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
inst : Std.Trichotomous r
inst_1 : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
h : s (({ toFun := f, inj' := ⋯ : α ↪ β } : (a : α) → β) a) (({ toFun := f, inj' := ⋯ : α ↪ β } : (a : α) → β) b)
⊢ r a b

Tactic:
Not.imp_symm (Std.Trichotomous.trichotomous a b · fun h' ↦ asymm (H _ _ h') h) ?_

Premises used: asymm, Not.imp_symm, Std.Trichotomous.trichotomous
-- 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
inst : Std.Trichotomous r
inst_1 : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
h : s (({ toFun := f, inj' := ⋯ : α ↪ β } : (a : α) → β) a) (({ toFun := f, inj' := ⋯ : α ↪ β } : (a : α) → β) b)
refine_2 : ¬a = b
⊢ r a b

Tactic:
refine Not.imp_symm (Std.Trichotomous.trichotomous a b · fun h' ↦ asymm (H _ _ h') h) ?_

Premises used: asymm, Not.imp_symm, Std.Trichotomous.trichotomous
-- 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
inst : Std.Trichotomous r
inst_1 : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
h : s (({ toFun := f, inj' := ⋯ : α ↪ β } : (a : α) → β) a) (({ toFun := f, inj' := ⋯ : α ↪ β } : (a : α) → β) b)
⊢ ¬a = b

Tactic:
(irrefl _ <| · ▸ h)

Premises used: irrefl, Not
-- 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
inst : Std.Trichotomous r
inst_1 : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
h : s (({ toFun := f, inj' := ⋯ : α ↪ β } : (a : α) → β) a) (({ toFun := f, inj' := ⋯ : α ↪ β } : (a : α) → β) b)
⊢ ¬a = b

Tactic:
exact (irrefl _ <| · ▸ h)

Premises used: irrefl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
⊢ (⇑(ofMonotone (r := r) (s := s) f H) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- 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
f : r ↪r s
g : t ↪r u
a c : α
⊢ Sum.LiftRel s u
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inl a))
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inl c)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelEmbedding.map_rel_iff
-- 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
f : r ↪r s
g : t ↪r u
a : α
d : γ
⊢ Sum.LiftRel s u
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inl a))
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inr d)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelEmbedding.map_rel_iff
-- 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
f : r ↪r s
g : t ↪r u
b : γ
c : α
⊢ Sum.LiftRel s u
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inr b))
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inl c)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelEmbedding.map_rel_iff
-- 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
f : r ↪r s
g : t ↪r u
b d : γ
⊢ Sum.LiftRel s u
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inr b))
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inr d)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelEmbedding.map_rel_iff
-- 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
f : r ↪r s
g : t ↪r u
a c : α
⊢ Sum.Lex s u
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inl a))
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inl c)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelEmbedding.map_rel_iff
-- 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
f : r ↪r s
g : t ↪r u
a : α
d : γ
⊢ Sum.Lex s u
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inl a))
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inr d)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelEmbedding.map_rel_iff
-- 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
f : r ↪r s
g : t ↪r u
b : γ
c : α
⊢ Sum.Lex s u
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inr b))
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inl c)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelEmbedding.map_rel_iff
-- 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
f : r ↪r s
g : t ↪r u
b d : γ
⊢ Sum.Lex s u
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inr b))
      (({ toFun := Sum.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α ⊕ γ ↪ β ⊕ δ } : (a : α ⊕ γ) → β ⊕ δ)
        (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inr d)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelEmbedding.map_rel_iff
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
s : β → β → Prop
a : α
h : ¬r a a
⊢ ∀ {a_1 b : β},
    Prod.Lex r s (({ toFun := Prod.mk a, inj' := ⋯ } : (a : β) → α × β) a_1)
        (({ toFun := Prod.mk a, inj' := ⋯ } : (a : β) → α × β) b) ↔
      s a_1 b

Tactic:
simp [Prod.lex_def, h]

Premises used: Prod.lex_def
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
b : β
h : ¬s b b
⊢ ∀ {a b_1 : α},
    Prod.Lex r s (({ toFun := fun (a : α) ↦ (a, b), inj' := ⋯ } : (a : α) → α × β) a)
        (({ toFun := fun (a : α) ↦ (a, b), inj' := ⋯ } : (a : α) → α × β) b_1) ↔
      r a b_1

Tactic:
simp [Prod.lex_def, h]

Premises used: Prod.lex_def
-- 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
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α × γ},
    Prod.Lex s u
        (({ toFun := Prod.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α × γ ↪ β × δ } : (a : α × γ) → β × δ)
          a)
        (({ toFun := Prod.map (⇑f : (a : α) → β) (⇑g : (a : γ) → δ), inj' := ⋯ : α × γ ↪ β × δ } : (a : α × γ) → β × δ)
          b) ↔
      Prod.Lex r t a b

Tactic:
simp [Prod.lex_def, f.map_rel_iff, g.map_rel_iff, f.inj]

Premises used: Prod.lex_def, RelEmbedding.map_rel_iff, RelEmbedding.inj
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e₁ : α ≃ β
o₁ : ∀ {a b : α}, s ((e₁ : (a : α) → β) a) ((e₁ : (a : α) → β) b) ↔ r a b
e₂ : α ≃ β
map_rel_iff' : ∀ {a b : α}, s ((e₂ : (a : α) → β) a) ((e₂ : (a : α) → β) b) ↔ r a b
h :
  (mk (r := r) (s := s) e₁ @o₁).toEquiv (r := r) (s := s) =
    (mk (r := r) (s := s) e₂ @map_rel_iff').toEquiv (r := r) (s := s)
⊢ mk (r := r) (s := s) e₁ @o₁ = mk (r := r) (s := s) e₂ @map_rel_iff'

Tactic:
congr
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ Eq (α := (a : α) → β) (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ Eq (α := (a : α) → β) (⇑f.toEquiv (r := r) (s := s).toEmbedding : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
a b : α
⊢ s ((f : (a : α) → β) a) ((f : (a : α) → β) b) ↔ r a b

Tactic:
f.map_rel_iff'

Premises used: RelIso.map_rel_iff'
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α ≃ β
o : ∀ ⦃a b : α⦄, s ((f : (a : α) → β) a) ((f : (a : α) → β) b) ↔ r a b
⊢ Eq (α := (a : α) → β) (⇑(mk (r := r) (s := s) f o) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ Eq (α := (a : α) → β) (⇑(f.toEquiv (r := r) (s := s)) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
⊢ Injective (β := (a : α) → β) fun (f : r ≃r s) ↦ (⇑f : (a : α) → β)

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f g : r ≃r s
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- 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
f : r ≃r s
a b : β
erw :
  s ((f : (a : α) → β) ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) a : α))
      ((f : (a : α) → β) ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) b : α)) ↔
    s a b
erw₁ : s a ((f : (a : α) → β) ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) b : α)) ↔ s a b
erw₂ erw₃ : s a b ↔ s a b
⊢ r ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) a) ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) b) ↔ s a b

Tactic:
erw [← f.map_rel_iff, f.1.apply_symm_apply, f.1.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, RelIso.map_rel_iff, RelIso.toEquiv
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
r : α → α → Prop
⊢ default = RelIso.refl r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
⊢ (e : (a : α) → β) ((e.symm (r := r) (s := s) : (a : β) → α) x : α) = x

Tactic:
e.right_inv x

Premises used: Equiv.right_inv, RelIso.toEquiv
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : α
⊢ (e.symm (r := r) (s := s) : (a : β) → α) ((e : (a : α) → β) x : β) = x

Tactic:
e.left_inv x

Premises used: RelIso.toEquiv, Equiv.left_inv
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ Eq.{u_1 + 1} (α := α → α)
    (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑(e.symm (r := r) (s := s)) : (a : β) → α) (⇑e : (a : α) → β)) id

Tactic:
funext e.symm_apply_apply

Premises used: RelIso.symm_apply_apply, funext
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ Eq.{u_2 + 1} (α := β → β)
    (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑(e.symm (r := r) (s := s)) : (a : β) → α)) id

Tactic:
funext e.apply_symm_apply

Premises used: funext, RelIso.apply_symm_apply
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≃r s
g : s ≃r t
a : γ
⊢ Eq.{u_1 + 1} (α := α) (((f.trans (r := r) (s := s) (t := t) g).symm (r := r) (s := t) : (a : γ) → α) a : α)
    ((f.symm (r := r) (s := s) : (a : β) → α) ((g.symm (r := s) (s := t) : (a : γ) → β) a : β) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
b : α
⊢ Eq.{u_2 + 1} (α := β) ((f.symm (r := r) (s := s).symm (r := s) (s := r) : (a : α) → β) b : β)
    ((f : (a : α) → β) b : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
x y : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x = y

Tactic:
EquivLike.apply_eq_iff_eq f

Premises used: EquivLike.apply_eq_iff_eq
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
x : α
y : β
f : r ≃r s
rw :
  Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β)
    ((f : (a : α) → β) ((f.symm (r := r) (s := s) : (a : β) → α) y : α) : β)
| (f : (a : α) → β) x = y

Tactic:
rw [← apply_symm_apply f y]

Premises used: RelIso.apply_symm_apply
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
x : α
y : β
f : r ≃r s
conv_lhs :
  Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β)
      ((f : (a : α) → β) ((f.symm (r := r) (s := s) : (a : β) → α) y : α) : β) ↔
    x = (f.symm (r := r) (s := s) : (a : β) → α) y
⊢ (f : (a : α) → β) x = y ↔ x = (f.symm (r := r) (s := s) : (a : β) → α) y

Tactic:
conv_lhs => rw [← apply_symm_apply f y]

Premises used: RelIso.apply_symm_apply
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
x : α
y : β
f : r ≃r s
rw rw₁ : x = (f.symm (r := r) (s := s) : (a : β) → α) y ↔ x = (f.symm (r := r) (s := s) : (a : β) → α) y
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β)
      ((f : (a : α) → β) ((f.symm (r := r) (s := s) : (a : β) → α) y : α) : β) ↔
    x = (f.symm (r := r) (s := s) : (a : β) → α) y

Tactic:
rw [apply_eq_iff_eq]

Premises used: RelIso.apply_eq_iff_eq
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
y : α
⊢ (e.symm (r := r) (s := s) : (a : β) → α) x = y ↔ x = (e : (a : α) → β) y

Tactic:
e.toEquiv.symm_apply_eq

Premises used: Equiv.symm_apply_eq, RelIso.toEquiv
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
y : α
⊢ y = (e.symm (r := r) (s := s) : (a : β) → α) x ↔ (e : (a : α) → β) y = x

Tactic:
e.toEquiv.eq_symm_apply

Premises used: RelIso.toEquiv, Equiv.eq_symm_apply
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ e.symm (r := r) (s := s).symm (r := s) (s := r) = e

Tactic:
rfl

Premises used: RelIso.symm, Equiv.symm, rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
⊢ Bijective (α := r ≃r s) (RelIso.symm (r := r) (s := s))

Tactic:
bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, RelIso.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
r : α → α → Prop
⊢ (RelIso.refl r).symm (r := r) (s := r) = RelIso.refl r

Tactic:
rfl

Premises used: RelIso.refl, RelIso.symm, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ e.trans (r := r) (s := s) (t := s) (RelIso.refl s) = e

Tactic:
rfl

Premises used: Equiv.trans, RelIso.trans, rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ (RelIso.refl r).trans (r := r) (s := r) (t := s) e = e

Tactic:
rfl

Premises used: Equiv.trans, RelIso.trans, rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ ∀ (x : β),
    Eq (α := β) ((e.symm (r := r) (s := s).trans (r := s) (s := r) (t := s) e : (a : β) → β) x : β)
      ((RelIso.refl s : (a : β) → β) x : β)

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ ∀ (x : α),
    Eq (α := α) ((e.trans (r := r) (s := s) (t := r) (e.symm (r := r) (s := s)) : (a : α) → α) x : α)
      ((RelIso.refl r : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
δ : Type u_5
u : δ → δ → Prop
ab : r ≃r s
bc : s ≃r t
cd : t ≃r u
⊢ (ab.trans (r := r) (s := s) (t := t) bc).trans (r := r) (s := t) (t := u) cd =
    ab.trans (r := r) (s := s) (t := u) (bc.trans (r := s) (s := t) (t := u) cd)

Tactic:
rfl

Premises used: Equiv.trans, RelIso.trans, rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
h₁ : α = β
h₂ : r ≍ s
a b : α
subst : ∀ {s : α → α → Prop} (h₂ : r ≍ s), s ((Equiv.cast ⋯ : (a : α) → α) a) ((Equiv.cast ⋯ : (a : α) → α) b) ↔ r a b
⊢ s ((Equiv.cast h₁ : (a : α) → β) a) ((Equiv.cast h₁ : (a : α) → β) b) ↔ r a b

Tactic:
subst h₁
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α_1 → α_1 → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α : Type u
r : α → α → Prop
a b : α
s : α → α → Prop
h₂ : r ≍ s
rw : s ((Equiv.cast ⋯ : (a : α) → α) a) ((Equiv.cast ⋯ : (a : α) → α) b) ↔ s a b
⊢ s ((Equiv.cast ⋯ : (a : α) → α) a) ((Equiv.cast ⋯ : (a : α) → α) b) ↔ r a b

Tactic:
rw [eq_of_heq h₂]

Premises used: eq_of_heq
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α_1 → α_1 → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α : Type u
r : α → α → Prop
a b : α
s : α → α → Prop
h₂ : r ≍ s
⊢ s ((Equiv.cast ⋯ : (a : α) → α) a) ((Equiv.cast ⋯ : (a : α) → α) b) ↔ s a b

Tactic:
rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α β : Type u
r : α → α → Prop
s : β → β → Prop
h₁ : α = β
h₂ : r ≍ s
⊢ (RelIso.cast (r := r) (s := s) h₁ h₂).symm (r := r) (s := s) = RelIso.cast (r := s) (s := r) ⋯ ⋯

Tactic:
rfl

Premises used: RelIso.cast, Equiv.cast, cast, RelIso.symm, Equiv.symm, rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u
r : α → α → Prop
h₁ : α = α
h₂ : r ≍ r
⊢ RelIso.cast (r := r) (s := r) h₁ h₂ = RelIso.refl r

Tactic:
rfl

Premises used: RelIso.refl, Equiv.refl, rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α β γ : Type u
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
h₁ : α = β
h₁' : β = γ
h₂ : r ≍ s
h₂' : s ≍ t
x : α
subst :
  ∀ {s : α → α → Prop} (h₁' : α = γ) (h₂ : r ≍ s) (h₂' : s ≍ t),
    Eq (α := γ)
      (((RelIso.cast (r := r) (s := s) ⋯ h₂).trans (r := r) (s := s) (t := t) (RelIso.cast (r := s) (s := t) h₁' h₂') :
            (a : α) → γ)
          x :
        γ)
      ((RelIso.cast (r := r) (s := t) ⋯ ⋯ : (a : α) → γ) x : γ)
⊢ Eq (α := γ)
    (((RelIso.cast (r := r) (s := s) h₁ h₂).trans (r := r) (s := s) (t := t) (RelIso.cast (r := s) (s := t) h₁' h₂') :
          (a : α) → γ)
        x :
      γ)
    ((RelIso.cast (r := r) (s := t) ⋯ ⋯ : (a : α) → γ) x : γ)

Tactic:
subst h₁
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : r ≍ s
h₂' : s ≍ t
⊢ Eq (α := γ)
    (((RelIso.cast (r := r) (s := s) ⋯ h₂).trans (r := r) (s := s) (t := t) (RelIso.cast (r := s) (s := t) h₁' h₂') :
          (a : α) → γ)
        x :
      γ)
    ((RelIso.cast (r := r) (s := t) ⋯ ⋯ : (a : α) → γ) x : γ)

Tactic:
rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α ≃ β
o : ∀ {a b : α}, s ((f : (a : α) → β) a) ((f : (a : α) → β) b) ↔ r a b
⊢ Eq (α := (a : β) → α) (⇑((mk (r := r) (s := s) f @o).symm (r := r) (s := s)) : (a : β) → α) (⇑f.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : α
y : β
rw :
  s ((e : (a : α) → β) x) ((e : (a : α) → β) ((e.symm (r := r) (s := s) : (a : β) → α) y : α)) ↔
    s ((e : (a : α) → β) x) y
rw₁ rw₂ : s ((e : (a : α) → β) x) y ↔ s ((e : (a : α) → β) x) y
⊢ r x ((e.symm (r := r) (s := s) : (a : β) → α) y) ↔ s ((e : (a : α) → β) x) y

Tactic:
rw [← e.map_rel_iff, e.apply_symm_apply]

Premises used: RelIso.apply_symm_apply, RelIso.map_rel_iff
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
y : α
rw :
  s ((e : (a : α) → β) ((e.symm (r := r) (s := s) : (a : β) → α) x : α)) ((e : (a : α) → β) y) ↔
    s x ((e : (a : α) → β) y)
rw₁ rw₂ : s x ((e : (a : α) → β) y) ↔ s x ((e : (a : α) → β) y)
⊢ r ((e.symm (r := r) (s := s) : (a : β) → α) x) y ↔ s x ((e : (a : α) → β) y)

Tactic:
rw [← e.map_rel_iff, e.apply_symm_apply]

Premises used: RelIso.apply_symm_apply, RelIso.map_rel_iff
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ Bijective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toEquiv.bijective

Premises used: Equiv.bijective, RelIso.toEquiv
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toEquiv.injective

Premises used: Equiv.injective, RelIso.toEquiv
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toEquiv.surjective

Premises used: Equiv.surjective, RelIso.toEquiv
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
a b : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ↔ a = b

Tactic:
f.injective.eq_iff

Premises used: Function.Injective.eq_iff, RelIso.injective
-- 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
e : r ≃r s
f : α → β
g : β → α
hf : f = (⇑e : (a : α) → β)
hg : g = (⇑(e.symm (r := r) (s := s)) : (a : β) → α)
x : α
⊢ g (f x) = x

Tactic:
simp [hf, hg]