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
g : r ↪r s
toFun : α → β
inj' : Injective toFun
map_rel_iff' :
  ∀ {a b : α},
    s (({ toFun := toFun, inj' := inj' : α ↪ β } : (a : α) → β) a)
        (({ toFun := toFun, inj' := inj' : α ↪ β } : (a : α) → β) b) ↔
      r a b
h :
  Eq (α := (a : α) → β)
    ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) { toFun := toFun, inj' := inj' } @map_rel_iff'))
    ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun) g)
rcases :
  ∀ (toFun_1 : α → β) (inj'_1 : Injective toFun_1)
    (map_rel_iff'_1 :
      ∀ {a b : α},
        s (({ toFun := toFun_1, inj' := inj'_1 : α ↪ β } : (a : α) → β) a)
            (({ toFun := toFun_1, inj' := inj'_1 : α ↪ β } : (a : α) → β) b) ↔
          r a b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun)
          (mk (r := r) (s := s) { toFun := toFun, inj' := inj' } @map_rel_iff'))
        ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun)
          (mk (r := r) (s := s) { toFun := toFun_1, inj' := inj'_1 } @map_rel_iff'_1))),
    mk (r := r) (s := s) { toFun := toFun, inj' := inj' : α ↪ β } @map_rel_iff' =
      mk (r := r) (s := s) { toFun := toFun_1, inj' := inj'_1 } @map_rel_iff'_1
⊢ mk (r := r) (s := s) { toFun := toFun, inj' := inj' : α ↪ β } @map_rel_iff' = g

Tactic:
rcases g with ⟨⟨⟩⟩
-- 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
toFun : α → β
inj' : Injective toFun
map_rel_iff' :
  ∀ {a b : α},
    s (({ toFun := toFun, inj' := inj' : α ↪ β } : (a : α) → β) a)
        (({ toFun := toFun, inj' := inj' : α ↪ β } : (a : α) → β) b) ↔
      r a b
toFun_1 : α → β
inj'_1 : Injective toFun_1
map_rel_iff'_1 :
  ∀ {a b : α},
    s (({ toFun := toFun_1, inj' := inj'_1 : α ↪ β } : (a : α) → β) a)
        (({ toFun := toFun_1, inj' := inj'_1 : α ↪ β } : (a : α) → β) b) ↔
      r a b
h :
  Eq (α := (a : α) → β)
    ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) { toFun := toFun, inj' := inj' } @map_rel_iff'))
    ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) { toFun := toFun_1, inj' := inj'_1 } @map_rel_iff'_1))
⊢ mk (r := r) (s := s) { toFun := toFun, inj' := inj' : α ↪ β } @map_rel_iff' =
    mk (r := r) (s := s) { toFun := toFun_1, inj' := inj'_1 } @map_rel_iff'_1

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.toEmbedding (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.toRelHom (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 : α ↪ β
map_rel_iff' : ∀ {a b : α}, s ((f : (a : α) → β) a) ((f : (a : α) → β) b) ↔ r a b
g : α ↪ β
map_rel_iff'_1 : ∀ {a b : α}, s ((g : (a : α) → β) a) ((g : (a : α) → β) b) ↔ r a b
⊢ (mk (r := r) (s := s) f @map_rel_iff').toEmbedding (r := r) (s := s) =
      (mk (r := r) (s := s) g @map_rel_iff'_1).toEmbedding (r := r) (s := s) →
    mk (r := r) (s := s) f @map_rel_iff' = mk (r := r) (s := s) g @map_rel_iff'_1

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f g : r ↪r s
⊢ f.toEmbedding (r := r) (s := s) = g.toEmbedding (r := r) (s := s) ↔ f = g

Tactic:
toEmbedding_injective.eq_iff

Premises used: Function.Injective.eq_iff, RelEmbedding.toEmbedding_injective
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
⊢ Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
f.inj'

Premises used: Function.Embedding.inj', RelEmbedding.toEmbedding
-- 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: RelEmbedding.injective, Function.Injective.eq_iff
-- 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: RelEmbedding.map_rel_iff'
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α ↪ β
h : ∀ {a b : α}, s ((f : (a : α) → β) a) ((f : (a : α) → β) b) ↔ r a b
⊢ Eq (α := (a : α) → β) (⇑(mk (r := r) (s := s) f @h) : (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 _ _ 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
g : s ↪r t
⊢ ∀ {a b : α},
    t ((f.toEmbedding (r := r) (s := s).trans (g.toEmbedding (r := s) (s := t)) : (a : α) → γ) a)
        ((f.toEmbedding (r := r) (s := s).trans (g.toEmbedding (r := s) (s := t)) : (a : α) → γ) b) ↔
      r a b

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
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ↪r s
g : s ↪r t
a : α
⊢ Eq.{u_3 + 1} (α := γ) ((f.trans (r := r) (s := s) (t := t) g : (a : α) → γ) a : γ)
    ((g : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Eq (α := (a : α) → γ) (⇑(f.trans (r := r) (s := s) (t := t) g) : (a : α) → γ)
    (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (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 : α
⊢ Eq.{u_2 + 1} (α := β) ((f.swap (r := r) (s := s) : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : β → β → Prop
a : α
⊢ Eq.{u_2 + 1} (α := β) ((preimage f s : (a : α) → β) a : β) ((f : (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
h : ∀ (a b : α), r a b ↔ ((⇑f : (a : α) → β) ⁻¹'o s) a b
⊢ r = (⇑f : (a : α) → β) ⁻¹'o s

Tactic:
ext a b
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a b : α
⊢ r a b ↔ ((⇑f : (a : α) → β) ⁻¹'o s) a b

Tactic:
f.map_rel_iff.symm

Premises used: RelEmbedding.map_rel_iff, Iff.symm, Order.Preimage
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a b : α
⊢ r a b ↔ ((⇑f : (a : α) → β) ⁻¹'o s) a b

Tactic:
exact f.map_rel_iff.symm

Premises used: RelEmbedding.map_rel_iff, Iff.symm
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
inst : Std.Irrefl s
⊢ Std.Irrefl r

Tactic:
⟨fun a => mt f.map_rel_iff.2 (irrefl (f a))⟩

Premises used: Iff.mpr, irrefl, mt, RelEmbedding.map_rel_iff, Std.Irrefl.mk, DFunLike.coe
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
inst : Std.Refl s
⊢ Std.Refl r

Tactic:
⟨fun _ => f.map_rel_iff.1 <| refl _⟩

Premises used: Std.Refl.mk, RelEmbedding.map_rel_iff, Iff.mp, refl, DFunLike.coe
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
inst : Std.Symm s
⊢ Std.Symm r

Tactic:
⟨fun _ _ => imp_imp_imp f.map_rel_iff.2 f.map_rel_iff.1 symm⟩

Premises used: Iff.mpr, Std.Symm.mk, RelEmbedding.map_rel_iff, Iff.mp, imp_imp_imp, symm
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
inst : Std.Asymm s
⊢ Std.Asymm r

Tactic:
⟨fun _ _ h₁ h₂ => asymm (f.map_rel_iff.2 h₁) (f.map_rel_iff.2 h₂)⟩

Premises used: Iff.mpr, asymm, RelEmbedding.map_rel_iff, Std.Asymm.mk
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
generalize : ∀ (b : β) (h : (f : (a : α) → β) a = b), Acc s b → Acc r a
⊢ Acc s ((f : (a : α) → β) a) → Acc r a

Tactic:
generalize h : f a = b

Premises used: DFunLike.coe
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b x : β
H : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
a : α
h : (f : (a : α) → β) a = x
⊢ Acc r a

Tactic:
?_
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
b : β
h : (f : (a : α) → β) a = b
ac : Acc s b
intro :
  ∀ (x : β) (H : ∀ (y : β), s y x → Acc s y) (IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a)
    (a : α) (h : (f : (a : α) → β) a = x), Acc r a
⊢ Acc r a

Tactic:
induction ac generalizing a with | intro _ H IH => ?_
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b x : β
H : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
a : α
h : (f : (a : α) → β) a = x
⊢ ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y

Tactic:
subst h
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b x : β
H : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
a : α
h : (f : (a : α) → β) a = x
H₁ : ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y
⊢ ∀ (y : β), s y ((f : (a : α) → β) a) → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a

Tactic:
subst h
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b : β
a : α
H : ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y
IH : ∀ (y : β), s y ((f : (a : α) → β) a) → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
⊢ Acc r a

Tactic:
⟨_, fun a' h => IH (f a') (f.map_rel_iff.2 h) _ rfl⟩

Premises used: Iff.mpr, RelEmbedding.map_rel_iff, DFunLike.coe, rfl, Acc.intro
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b : β
a : α
H : ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y
IH : ∀ (y : β), s y ((f : (a : α) → β) a) → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
⊢ Acc r a

Tactic:
exact ⟨_, fun a' h => IH (f a') (f.map_rel_iff.2 h) _ rfl⟩
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
inst : IsWellFounded β s
⊢ IsWellFounded α r

Tactic:
⟨f.wellFounded IsWellFounded.wf⟩

Premises used: IsWellFounded.mk, RelEmbedding.wellFounded, IsWellFounded.wf
-- 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 : LT α
inst_1 : WellFoundedLT α
p : α → Prop
⊢ WellFoundedLT.{u_1} (Subtype p)

Tactic:
(Subtype.relEmbedding (· < ·) p).isWellFounded

Premises used: Subtype.relEmbedding, LT.lt, RelEmbedding.isWellFounded, Order.Preimage
-- 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 : LT α
inst_1 : WellFoundedGT α
p : α → Prop
⊢ WellFoundedGT.{u_1} (Subtype p)

Tactic:
(Subtype.relEmbedding (· > ·) p).isWellFounded

Premises used: Subtype.relEmbedding, GT.gt, RelEmbedding.isWellFounded, Order.Preimage
-- 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
x_1 : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
x y : Quotient x_1
h :
  ∀ (a b : α),
    r ((Embedding.quotientOut α : (a : Quotient x_1) → α) ⟦a⟧)
        ((Embedding.quotientOut α : (a : Quotient x_1) → α) ⟦b⟧) ↔
      Quotient.lift₂ r H ⟦a⟧ ⟦b⟧
⊢ r ((Embedding.quotientOut α : (a : Quotient x_1) → α) x) ((Embedding.quotientOut α : (a : Quotient x_1) → α) y) ↔
    Quotient.lift₂ r H x y

Tactic:
induction x, y using Quotient.inductionOn₂
-- 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
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a b : α
apply : (Embedding.quotientOut α : (a : Quotient x) → α) ⟦a⟧ ≈ a
apply₁ : (Embedding.quotientOut α : (a : Quotient x) → α) ⟦b⟧ ≈ b
⊢ r ((Embedding.quotientOut α : (a : Quotient x) → α) ⟦a⟧) ((Embedding.quotientOut α : (a : Quotient x) → α) ⟦b⟧) ↔
    Quotient.lift₂ r H ⟦a⟧ ⟦b⟧

Tactic:
apply iff_iff_eq.2 (H _ _ _ _ _ _)

Premises used: Iff.mpr, iff_iff_eq
-- 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
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a b : α
⊢ (Embedding.quotientOut α : (a : Quotient x) → α) ⟦a⟧ ≈ a

Tactic:
apply Quotient.mk_out

Premises used: Quotient.mk_out
-- 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
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a b : α
⊢ (Embedding.quotientOut α : (a : Quotient x) → α) ⟦b⟧ ≈ b

Tactic:
apply Quotient.mk_out

Premises used: Quotient.mk_out
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
mp : Acc (Quotient.lift₂ r H) ⟦a⟧ → Acc r a
mpr : Acc r a → Acc (Quotient.lift₂ r H) ⟦a⟧
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a

Tactic:
constructor
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ → Acc r a

Tactic:
RelHomClass.acc (Quotient.mkRelHom H) a

Premises used: RelHomClass.acc, Quotient.mkRelHom
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ → Acc r a

Tactic:
exact RelHomClass.acc (Quotient.mkRelHom H) a

Premises used: RelHomClass.acc, Quotient.mkRelHom
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x_1 : α
h : ∀ (y : α), r y x_1 → Acc r y
IH : ∀ (y : α), r y x_1 → Acc (Quotient.lift₂ r H) ⟦y⟧
⊢ Acc (Quotient.lift₂ r H) ⟦x_1⟧

Tactic:
?_
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
ac : Acc r a
mpr :
  ∀ (x_1 : α),
    (∀ (y : α), r y x_1 → Acc r y) →
      ∀ (IH : ∀ (y : α), r y x_1 → Acc (Quotient.lift₂ r H) ⟦y⟧), Acc (Quotient.lift₂ r H) ⟦x_1⟧
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
induction ac with | intro _ _ IH => ?_
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x_1 : α
h : ∀ (y : α), r y x_1 → Acc r y
IH : ∀ (y : α), r y x_1 → Acc (Quotient.lift₂ r H) ⟦y⟧
⊢ Acc (Quotient.lift₂ r H) ⟦x_1⟧

Tactic:
⟨_, fun q h => ?_⟩

Premises used: Acc.intro
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x_1 : α
h : ∀ (y : α), r y x_1 → Acc r y
IH : ∀ (y : α), r y x_1 → Acc (Quotient.lift₂ r H) ⟦y⟧
mpr : ∀ (q : Quotient x) (h : Quotient.lift₂ r H q ⟦x_1⟧), Acc (Quotient.lift₂ r H) q
⊢ Acc (Quotient.lift₂ r H) ⟦x_1⟧

Tactic:
refine ⟨_, fun q h => ?_⟩
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x_1 : α
h_1 : ∀ (y : α), r y x_1 → Acc r y
IH : ∀ (y : α), r y x_1 → Acc (Quotient.lift₂ r H) ⟦y⟧
q : Quotient x
h : Quotient.lift₂ r H q ⟦x_1⟧
mpr : ∀ (a' : α) (h : Quotient.lift₂ r H ⟦a'⟧ ⟦x_1⟧), Acc (Quotient.lift₂ r H) ⟦a'⟧
⊢ Acc (Quotient.lift₂ r H) q

Tactic:
obtain ⟨a', rfl⟩ := q.exists_rep

Premises used: Quotient.exists_rep, rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x_1 : α
h_1 : ∀ (y : α), r y x_1 → Acc r y
IH : ∀ (y : α), r y x_1 → Acc (Quotient.lift₂ r H) ⟦y⟧
a' : α
h : Quotient.lift₂ r H ⟦a'⟧ ⟦x_1⟧
⊢ Acc (Quotient.lift₂ r H) ⟦a'⟧

Tactic:
IH a' h
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x_1 : α
h_1 : ∀ (y : α), r y x_1 → Acc r y
IH : ∀ (y : α), r y x_1 → Acc (Quotient.lift₂ r H) ⟦y⟧
a' : α
h : Quotient.lift₂ r H ⟦a'⟧ ⟦x_1⟧
⊢ Acc (Quotient.lift₂ r H) ⟦a'⟧

Tactic:
exact IH a' h
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
s : Setoid α
r : α → α → Prop
H : ∀ (a₁ a₂ b₁ b₂ : α), (s : α → α → Prop) a₁ b₁ → (s : α → α → Prop) a₂ b₂ → r a₁ a₂ = r b₁ b₂
a : α
⊢ Acc (fun (x y : Quotient s) ↦ x.liftOn₂' y r H) (Quotient.mk'' a) ↔ Acc r a

Tactic:
acc_lift₂_iff (H := H)

Premises used: acc_lift₂_iff, Quotient.liftOn₂'
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
mp : WellFounded (Quotient.lift₂ r H) → WellFounded r
mpr : WellFounded r → WellFounded (Quotient.lift₂ r H)
⊢ WellFounded (Quotient.lift₂ r H) ↔ WellFounded r

Tactic:
constructor
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) → WellFounded r

Tactic:
RelHomClass.wellFounded (Quotient.mkRelHom H)

Premises used: RelHomClass.wellFounded, Quotient.mkRelHom
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) → WellFounded r

Tactic:
exact RelHomClass.wellFounded (Quotient.mkRelHom H)

Premises used: RelHomClass.wellFounded, Quotient.mkRelHom
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded r → WellFounded (Quotient.lift₂ r H)

Tactic:
fun wf => ⟨fun q => ?_⟩

Premises used: WellFounded.intro
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
mpr : ∀ (wf : WellFounded r) (q : Quotient x), Acc (Quotient.lift₂ r H) q
⊢ WellFounded r → WellFounded (Quotient.lift₂ r H)

Tactic:
refine fun wf => ⟨fun q => ?_⟩
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
q : Quotient x
mpr : ∀ (a : α), Acc (Quotient.lift₂ r H) ⟦a⟧
⊢ Acc (Quotient.lift₂ r H) q

Tactic:
obtain ⟨a, rfl⟩ := q.exists_rep

Premises used: Quotient.exists_rep, rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
acc_lift₂_iff.2 (wf.apply a)

Premises used: Iff.mpr, acc_lift₂_iff, WellFounded.apply
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
x : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
exact acc_lift₂_iff.2 (wf.apply a)

Premises used: Iff.mpr, acc_lift₂_iff, WellFounded.apply
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
s : Setoid α
r : α → α → Prop
H : ∀ (a₁ a₂ b₁ b₂ : α), (s : α → α → Prop) a₁ b₁ → (s : α → α → Prop) a₂ b₂ → r a₁ a₂ = r b₁ b₂
⊢ (WellFounded fun (x y : Quotient s) ↦ x.liftOn₂' y r H) ↔ WellFounded r

Tactic:
wellFounded_lift₂_iff (H := H)

Premises used: wellFounded_lift₂_iff, Quotient.liftOn₂'
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
inst : Std.Antisymm r
inst_1 : Std.Refl s
hf : ∀ (a b : α), s (f a) (f b) ↔ r a b
⊢ (⇑(ofMapRelIff (r := r) (s := s) f hf) : (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
inst : Std.Trichotomous r
inst_1 : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
⊢ Std.Irrefl s

Tactic:
haveI := @Std.Asymm.irrefl β s _
-- 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
refine_1 : ∀ (a b : α) (e : f a = f b), a = b
refine_2 :
  ∀ (a b : α)
    (h : s (({ toFun := f, inj' := ⋯ : α ↪ β } : (a : α) → β) a) (({ toFun := f, inj' := ⋯ : α ↪ β } : (a : α) → β) b)),
    r a b
⊢ r ↪r s

Tactic:
refine ⟨⟨f, fun a b e => ?_⟩, @fun a b => ⟨fun h => ?_, H _ _⟩⟩
-- 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
refine_1 : ¬r a b
refine_1₁ : ¬r b a
⊢ a = b

Tactic:
apply Std.Trichotomous.trichotomous (r := r) a b

Premises used: 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 : α
e : f a = f b
h : r a b
⊢ s (f a) (f a)

Tactic:
simpa [e] using H _ _ h
-- 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 a b

Tactic:
exact fun h => irrefl (r := s) (f a) (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 : α
e : f a = f b
h : r b a
⊢ s (f b) (f b)

Tactic:
simpa [e] using H _ _ h