awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f g : r →r s
h :
  Eq (α := (a : α) → β) ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) f)
    ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) g)
⊢ f = g
have mk : ∀ (toFun : α → β) (map_rel' : ∀ {a b : α}, r a b → s (toFun a) (toFun b))
  (h :
    Eq (α := (a : α) → β) ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) (mk (r := r) (s := s) toFun @map_rel'))
      ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) g)),
  mk (r := r) (s := s) toFun @map_rel' = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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 : α → β
map_rel' : ∀ {a b : α}, r a b → s (toFun a) (toFun b)
h :
  Eq (α := (a : α) → β) ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) (mk (r := r) (s := s) toFun @map_rel'))
    ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) g)
⊢ mk (r := r) (s := s) toFun @map_rel' = g
have mk : ∀ (toFun_1 : α → β) (map_rel'_1 : ∀ {a b : α}, r a b → s (toFun_1 a) (toFun_1 b))
  (h :
    Eq (α := (a : α) → β) ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) (mk (r := r) (s := s) toFun @map_rel'))
      ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) (mk (r := r) (s := s) toFun_1 @map_rel'_1))),
  mk (r := r) (s := s) toFun @map_rel' = mk (r := r) (s := s) toFun_1 @map_rel'_1
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
⊢ x = y
have inl : ∀ (h : r x y), x = y
Tactic: rcases trichotomous_of r x y with (h | h | h)
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
inl : ∀ (h : r x y), x = y
⊢ x = y
have inr : ∀ (h : x = y), x = y
Tactic: rcases trichotomous_of r x y with (h | h | h)
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
inl : ∀ (h : r x y), x = y
inr : ∀ (h : x = y), x = y
⊢ x = y
have inr₁ : ∀ (h : r y x), x = y
Tactic: rcases trichotomous_of r x y with (h | h | h)
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
⊢ x = y
have this : s (f x) (f y)
Tactic: have := hf h
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f x) (f y)
⊢ x = y
have this₁ : s (f y) (f y)
Tactic: rw [hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ x = y
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
⊢ x = y
have this : s (f y) (f x)
Tactic: have := hf h
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f x)
⊢ x = y
have this₁ : s (f y) (f y)
Tactic: rw [hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ x = y
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f g : r ↪r s
h :
  Eq (α := (a : α) → β) ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun) f)
    ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun) g)
⊢ f = g
have rcases : ∀ (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)),
  mk (r := r) (s := s) { toFun := toFun, inj' := inj' : α ↪ β } @map_rel_iff' = g
Tactic: rcases f with ⟨⟨⟩⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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)
⊢ mk (r := r) (s := s) { toFun := toFun, inj' := inj' : α ↪ β } @map_rel_iff' = g
have 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
Tactic: rcases g with ⟨⟨⟩⟩
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
⊢ r = (⇑f : (a : α) → β) ⁻¹'o s
have h : ∀ (a b : α), r a b ↔ ((⇑f : (a : α) → β) ⁻¹'o s) a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
⊢ Acc s ((f : (a : α) → β) a) → Acc r a
have generalize : ∀ (b : β) (h : (f : (a : α) → β) a = b), Acc s b → Acc r a
Tactic: generalize h : f a = b
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ Acc r a
have 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
Tactic: induction ac generalizing a with | intro _ H IH => ?_
Cleared hypotheses: a, h, ac
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (hypothesis)
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
have H₁ : ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y
Tactic: subst h
Cleared hypotheses: x, H, IH, h
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (hypothesis)
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
⊢ Acc r a
have IH₁ : ∀ (y : β), s y ((f : (a : α) → β) a) → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
Tactic: subst h
Cleared hypotheses: x, H, IH, h
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ r ((Embedding.quotientOut α : (a : Quotient x_1) → α) x) ((Embedding.quotientOut α : (a : Quotient x_1) → α) y) ↔
    Quotient.lift₂ r H x y
have h : ∀ (a b : α),
  r ((Embedding.quotientOut α : (a : Quotient x_1) → α) ⟦a⟧) ((Embedding.quotientOut α : (a : Quotient x_1) → α) ⟦b⟧) ↔
    Quotient.lift₂ r H ⟦a⟧ ⟦b⟧
Tactic: induction x, y using Quotient.inductionOn₂
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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 : α
⊢ r ((Embedding.quotientOut α : (a : Quotient x) → α) ⟦a⟧) ((Embedding.quotientOut α : (a : Quotient x) → α) ⟦b⟧) ↔
    Quotient.lift₂ r H ⟦a⟧ ⟦b⟧
have apply : (Embedding.quotientOut α : (a : Quotient x) → α) ⟦a⟧ ≈ a
Tactic: apply iff_iff_eq.2 (H _ _ _ _ _ _)
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ r ((Embedding.quotientOut α : (a : Quotient x) → α) ⟦a⟧) ((Embedding.quotientOut α : (a : Quotient x) → α) ⟦b⟧) ↔
    Quotient.lift₂ r H ⟦a⟧ ⟦b⟧
have apply₁ : (Embedding.quotientOut α : (a : Quotient x) → α) ⟦b⟧ ≈ b
Tactic: apply iff_iff_eq.2 (H _ _ _ _ _ _)
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
have mp : Acc (Quotient.lift₂ r H) ⟦a⟧ → Acc r a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a
have mpr : Acc r a → Acc (Quotient.lift₂ r H) ⟦a⟧
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧
have 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⟧
Tactic: induction ac with | intro _ _ IH => ?_
Cleared hypotheses: ac
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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⟧
have mpr : ∀ (q : Quotient x) (h : Quotient.lift₂ r H q ⟦x_1⟧), Acc (Quotient.lift₂ r H) q
Tactic: refine ⟨_, fun q h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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⟧
⊢ Acc (Quotient.lift₂ r H) q
have mpr : ∀ (a' : α) (h : Quotient.lift₂ r H ⟦a'⟧ ⟦x_1⟧), Acc (Quotient.lift₂ r H) ⟦a'⟧
Tactic: obtain ⟨a', rfl⟩ := q.exists_rep
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
have mp : WellFounded (Quotient.lift₂ r H) → WellFounded r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ WellFounded (Quotient.lift₂ r H) ↔ WellFounded r
have mpr : WellFounded r → WellFounded (Quotient.lift₂ r H)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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)
have mpr : ∀ (wf : WellFounded r) (q : Quotient x), Acc (Quotient.lift₂ r H) q
Tactic: refine fun wf => ⟨fun q => ?_⟩
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ Acc (Quotient.lift₂ r H) q
have mpr : ∀ (a : α), Acc (Quotient.lift₂ r H) ⟦a⟧
Tactic: obtain ⟨a, rfl⟩ := q.exists_rep
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (hypothesis)
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)
⊢ r ↪r s
have this : Std.Irrefl s
Tactic: haveI := @Std.Asymm.irrefl β s _
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ r ↪r s
have refine_1 : ∀ (a b : α) (e : f a = f b), a = b
Tactic: refine ⟨⟨f, fun a b e => ?_⟩, @fun a b => ⟨fun h => ?_, H _ _⟩⟩
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ r ↪r s
have refine_2 : ∀ (a b : α)
  (h : s (({ toFun := f, inj' := sorry : α ↪ β } : (a : α) → β) a) (({ toFun := f, inj' := sorry : α ↪ β } : (a : α) → β) b)),
  r a b
Tactic: refine ⟨⟨f, fun a b e => ?_⟩, @fun a b => ⟨fun h => ?_, H _ _⟩⟩
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ a = b
have refine_1 : ¬r a b
Tactic: apply Std.Trichotomous.trichotomous (r := r) a b
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ a = b
have refine_1₁ : ¬r b a
Tactic: apply Std.Trichotomous.trichotomous (r := r) a b
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
have refine_2 : ¬a = b
Tactic: refine Not.imp_symm (Std.Trichotomous.trichotomous a b · fun h' ↦ asymm (H _ _ h') h) ?_
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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 : β
⊢ r ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) a) ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) b) ↔ s a b
have 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
Tactic: erw [← f.map_rel_iff, f.1.apply_symm_apply, f.1.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ r ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) a) ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) b) ↔ s a b
have erw₁ : s a ((f : (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]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ r ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) a) ((f.toEquiv (r := r) (s := s).symm : (a : β) → α) b) ↔ s a b
have erw₂ : s a b ↔ s a b
Tactic: erw [← f.map_rel_iff, f.1.apply_symm_apply, f.1.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
x : α
y : β
f : r ≃r s
| (f : (a : α) → β) x = y
have rw : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) ((f.symm (r := r) (s := s) : (a : β) → α) y : α) : β)
Tactic: rw [← apply_symm_apply f y]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
x : α
y : β
f : r ≃r s
⊢ (f : (a : α) → β) x = y ↔ x = (f.symm (r := r) (s := s) : (a : β) → α) y
have 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
Tactic: conv_lhs => rw [← apply_symm_apply f y]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
x : α
y : β
f : r ≃r s
⊢ 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
have rw : x = (f.symm (r := r) (s := s) : (a : β) → α) y ↔ x = (f.symm (r := r) (s := s) : (a : β) → α) y
Tactic: rw [apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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 : α
⊢ s ((Equiv.cast h₁ : (a : α) → β) a) ((Equiv.cast h₁ : (a : α) → β) b) ↔ r a b
have subst : ∀ {s : α → α → Prop} (h₂ : r ≍ s), s ((Equiv.cast sorry : (a : α) → α) a) ((Equiv.cast sorry : (a : α) → α) b) ↔ r a b
Tactic: subst h₁
Cleared hypotheses: β, s, h₁, h₂
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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) ↔ r a b
have rw : s ((Equiv.cast sorry : (a : α) → α) a) ((Equiv.cast sorry : (a : α) → α) b) ↔ s a b
Tactic: rw [eq_of_heq h₂]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α β γ : Type u
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
h₁ : α = β
h₁' : β = γ
h₂ : r ≍ s
h₂' : s ≍ t
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 : γ)
have subst : ∀ {s : α → α → Prop} (h₁' : α = γ) (h₂ : r ≍ s) (h₂' : s ≍ t),
  Eq (α := γ)
    (((RelIso.cast (r := r) (s := s) sorry h₂).trans (r := r) (s := s) (t := t) (RelIso.cast (r := s) (s := t) h₁' h₂') :
          (a : α) → γ)
        x :
      γ)
    ((RelIso.cast (r := r) (s := t) sorry sorry : (a : α) → γ) x : γ)
Tactic: subst h₁
Cleared hypotheses: β, s, h₁, h₁', h₂, h₂'
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : α
y : β
⊢ r x ((e.symm (r := r) (s := s) : (a : β) → α) y) ↔ s ((e : (a : α) → β) x) y
have rw : s ((e : (a : α) → β) x) ((e : (a : α) → β) ((e.symm (r := r) (s := s) : (a : β) → α) y : α)) ↔ s ((e : (a : α) → β) x) y
Tactic: rw [← e.map_rel_iff, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ r x ((e.symm (r := r) (s := s) : (a : β) → α) y) ↔ s ((e : (a : α) → β) x) y
have rw₁ : s ((e : (a : α) → β) x) y ↔ s ((e : (a : α) → β) x) y
Tactic: rw [← e.map_rel_iff, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
y : α
⊢ r ((e.symm (r := r) (s := s) : (a : β) → α) x) y ↔ s x ((e : (a : α) → β) y)
have rw : s ((e : (a : α) → β) ((e.symm (r := r) (s := s) : (a : β) → α) x : α)) ((e : (a : α) → β) y) ↔ s x ((e : (a : α) → β) y)
Tactic: rw [← e.map_rel_iff, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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)
⊢ r ((e.symm (r := r) (s := s) : (a : β) → α) x) y ↔ s x ((e : (a : α) → β) y)
have rw₁ : s x ((e : (a : α) → β) y) ↔ s x ((e : (a : α) → β) y)
Tactic: rw [← e.map_rel_iff, e.apply_symm_apply]