awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
ih : Join (ReflTransGen r) d c
⊢ Join (ReflTransGen r) e c
have tail : ∀ (b : α) (hdb : ReflTransGen r d b) (hcb : ReflTransGen r c b), Join (ReflTransGen r) e c
Tactic: rcases ih with ⟨b, hdb, hcb⟩
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
ih : ∃ (a : α), ReflTransGen r e a ∧ ReflGen r f a
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
have tail : ∀ (a : α) (hea : ReflTransGen r e a) (hfa : ReflGen r f a), ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
Tactic: rcases ih with ⟨a, hea, hfa⟩
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a_1 c
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
have tail : ∀ (c : α) (hbc : ReflGen r b c) (hac : ReflTransGen r a c), ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
Tactic: rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a_1 c
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : ReflGen r f a
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
have tail : ∀ (hea : ReflTransGen r e f), ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
Tactic: cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
Cleared hypotheses: a, hea, hfa
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a_1 c
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : ReflGen r f a
tail : ∀ (hea : ReflTransGen r e f), ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
have tail₁ : ∀ (hfa : r f a), ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
Tactic: cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
Cleared hypotheses: hfa
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
have refl : ∃ (a : α), ReflTransGen r e a ∧ ReflGen r d a
Tactic: induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
Cleared hypotheses: hdb
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
refl : ∃ (a : α), ReflTransGen r e a ∧ ReflGen r d a
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
have tail : ∀ {f b : α},
  ReflTransGen r d f →
    ∀ (hfb : r f b) (ih : ∃ (a : α), ReflTransGen r e a ∧ ReflGen r f a), ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
Tactic: induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
Cleared hypotheses: hdb
-- Lean 4 proof step from Mathlib.Logic.Relation (hypothesis)
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
⊢ Join (ReflTransGen r) e c
have this : ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
Tactic: have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
      clear hcb
      induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
this : ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
⊢ Join (ReflTransGen r) e c
have tail : ∀ (a : α) (hea : ReflTransGen r e a) (hba : ReflGen r b a), Join (ReflTransGen r) e c
Tactic: rcases this with ⟨a, hea, hba⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a_1 c
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : ReflGen r b a
⊢ Join (ReflTransGen r) e c
have tail : ∀ (hea : ReflTransGen r e b), Join (ReflTransGen r) e c
Tactic: cases hba with
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩
Cleared hypotheses: a, hea, hba
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a_1 c
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : ReflGen r b a
tail : ∀ (hea : ReflTransGen r e b), Join (ReflTransGen r) e c
⊢ Join (ReflTransGen r) e c
have tail₁ : ∀ (hba : r b a), Join (ReflTransGen r) e c
Tactic: cases hba with
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩
Cleared hypotheses: hba
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hab : ReflTransGen r a b
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) b c
have refl : Join (ReflTransGen r) a c
Tactic: induction hab with
  | refl => exact ⟨c, hac, refl⟩
  | @tail d e _ hde ih =>
    rcases ih with ⟨b, hdb, hcb⟩
    have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
      clear hcb
      induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
    rcases this with ⟨a, hea, hba⟩
    cases hba with
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hab : ReflTransGen r a b
hac : ReflTransGen r a c
refl : Join (ReflTransGen r) a c
⊢ Join (ReflTransGen r) b c
have tail : ∀ {d e : α}, ReflTransGen r a d → ∀ (hde : r d e) (ih : Join (ReflTransGen r) d c), Join (ReflTransGen r) e c
Tactic: induction hab with
  | refl => exact ⟨c, hac, refl⟩
  | @tail d e _ hde ih =>
    rcases ih with ⟨b, hdb, hcb⟩
    have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
      clear hcb
      induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
    rcases this with ⟨a, hea, hba⟩
    cases hba with
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h_1 : Equivalence r
h : EqvGen r a b
⊢ r a b
have rel : ∀ (x y : α), r x y → r x y
Tactic: induction h with
      | rel => assumption
      | refl => exact h.1 _
      | symm => apply h.symm; assumption
      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h_1 : Equivalence r
h : EqvGen r a b
rel : ∀ (x y : α), r x y → r x y
⊢ r a b
have refl : ∀ (x : α), r x x
Tactic: induction h with
      | rel => assumption
      | refl => exact h.1 _
      | symm => apply h.symm; assumption
      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h_1 : Equivalence r
h : EqvGen r a b
rel : ∀ (x y : α), r x y → r x y
refl : ∀ (x : α), r x x
⊢ r a b
have symm : ∀ (x y : α), EqvGen r x y → r x y → r y x
Tactic: induction h with
      | rel => assumption
      | refl => exact h.1 _
      | symm => apply h.symm; assumption
      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h_1 : Equivalence r
h : EqvGen r a b
rel : ∀ (x y : α), r x y → r x y
refl : ∀ (x : α), r x x
symm : ∀ (x y : α), EqvGen r x y → r x y → r y x
⊢ r a b
have trans : ∀ (x y z : α), EqvGen r x y → EqvGen r y z → ∀ (hab : r x y) (hbc : r y z), r x z
Tactic: induction h with
      | rel => assumption
      | refl => exact h.1 _
      | symm => apply h.symm; assumption
      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Small.Basic (goal)
Goal:
α : Type v
inst : Subsingleton α
⊢ Small.{w, v} α
have inl : IsEmpty α → Small.{w, v} α
Tactic: rcases isEmpty_or_nonempty α with ⟨⟩
-- Lean 4 proof step from Mathlib.Logic.Small.Basic (goal)
Goal:
α : Type v
inst : Subsingleton α
inl : IsEmpty α → Small.{w, v} α
⊢ Small.{w, v} α
have inr : Nonempty α → Small.{w, v} α
Tactic: rcases isEmpty_or_nonempty α with ⟨⟩
-- Lean 4 proof step from Mathlib.Logic.Small.Basic (goal)
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
⊢ Small.{u, w} β
have pos : ∀ (hβ : Nonempty β), Small.{u, w} β
Tactic: by_cases hβ : Nonempty β
-- Lean 4 proof step from Mathlib.Logic.Small.Basic (goal)
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
pos : ∀ (hβ : Nonempty β), Small.{u, w} β
⊢ Small.{u, w} β
have neg : ∀ (hβ : ¬Nonempty β), Small.{u, w} β
Tactic: by_cases hβ : Nonempty β
-- Lean 4 proof step from Mathlib.Logic.Small.Basic (goal)
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : Nonempty β
⊢ Small.{u, w} β
have pos : ∀ (b : β), ∃ (a : α), (Function.invFun g ∘ f) a = b
Tactic: refine small_of_surjective (f := Function.invFun g ∘ f) (fun b => ?_)
-- Lean 4 proof step from Mathlib.Logic.Small.Basic (goal)
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : Nonempty β
b : β
⊢ ∃ (a : α), (Function.invFun g ∘ f) a = b
have pos : ∀ (a : α) (ha : f a = g b), ∃ (a : α), (Function.invFun g ∘ f) a = b
Tactic: obtain ⟨a, ha⟩ := h b
-- Lean 4 proof step from Mathlib.Logic.Small.Basic (goal)
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ (Function.invFun g ∘ f) a = b
have rw : Function.invFun g (f a) = b
Tactic: rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]
-- Lean 4 proof step from Mathlib.Logic.Small.Basic (goal)
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
rw : Function.invFun g (f a) = b
⊢ (Function.invFun g ∘ f) a = b
have rw₁ : Function.invFun g (g b) = b
Tactic: rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]
-- Lean 4 proof step from Mathlib.Logic.Small.Basic (goal)
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
rw : Function.invFun g (f a) = b
rw₁ : Function.invFun g (g b) = b
⊢ (Function.invFun g ∘ f) a = b
have rw₂ : b = b
Tactic: rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]
-- Lean 4 proof step from Mathlib.Logic.Small.Basic (hypothesis)
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : ¬Nonempty β
⊢ Small.{u, w} β
have hβ₁ : IsEmpty β
Tactic: simp only [not_nonempty_iff] at hβ
Cleared hypotheses: hβ
-- Lean 4 proof step from Mathlib.Logic.Small.Defs (goal)
Goal:
α : Type u_1
inst : Small.{w, u_1} α
F : Shrink.{w, u_1} α → Sort v
f : (a : α) → F ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a)
a : α
⊢ Shrink.rec (F := F) f ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a) = f a
have simp : HEq (α :=
  F
    ((equivShrink α : (a : α) → Shrink.{w, u_1} α)
      ((Equiv.symm (equivShrink α) : (a : Shrink.{w, u_1} α) → α)
        ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a : Shrink.{w, u_1} α))))
  (f
    ((Equiv.symm (equivShrink α) : (a : Shrink.{w, u_1} α) → α)
      ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a : Shrink.{w, u_1} α)))
  (f a)
Tactic: simp only [Shrink.rec, eqRec_eq_cast, cast_eq_iff_heq]
-- Lean 4 proof step from Mathlib.Logic.Small.Defs (goal)
Goal:
α : Type u_1
inst : Small.{w, u_1} α
F : Shrink.{w, u_1} α → Sort v
f : (a : α) → F ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a)
a : α
⊢ HEq (α :=
    F
      ((equivShrink α : (a : α) → Shrink.{w, u_1} α)
        ((Equiv.symm (equivShrink α) : (a : Shrink.{w, u_1} α) → α)
          ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a : Shrink.{w, u_1} α))))
    (f
      ((Equiv.symm (equivShrink α) : (a : Shrink.{w, u_1} α) → α)
        ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a : Shrink.{w, u_1} α)))
    (f a)
have rw : f a ≍ f a
Tactic: rw [Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Logic.Small.Defs (hypothesis)
Goal:
S : Type u
e_1 : Type (max u v) ≃ S
a b : Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
e :
  Eq (α := (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
    (Sigma.mk (β := fun (α : S) ↦ (e_1.symm : (a : S) → Type (max u v)) α)
        ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α))) (cast ⋯ a) :
      (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
    (Sigma.mk (β := fun (α : S) ↦ (e_1.symm : (a : S) → Type (max u v)) α)
        ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α))) (cast ⋯ b) :
      (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
⊢ a = b
have h₁ : Eq.{u + 1} (α := S) ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)) : S)
  ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)) : S)
Tactic: injection e with h₁ h₂
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Logic.Small.Defs (hypothesis)
Goal:
S : Type u
e_1 : Type (max u v) ≃ S
a b : Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
e :
  Eq (α := (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
    (Sigma.mk (β := fun (α : S) ↦ (e_1.symm : (a : S) → Type (max u v)) α)
        ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α))) (cast ⋯ a) :
      (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
    (Sigma.mk (β := fun (α : S) ↦ (e_1.symm : (a : S) → Type (max u v)) α)
        ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α))) (cast ⋯ b) :
      (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
h₁ :
  Eq.{u + 1} (α := S) ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)) : S)
    ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)) : S)
⊢ a = b
have h₂ : cast sorry a = cast sorry b
Tactic: injection e with h₁ h₂
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Logic.Small.Set (goal)
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β → γ
s : Set α
t : Set β
inst : Small.{u, u1} (↑s : Type u1)
inst_1 : Small.{u, u2} (↑t : Type u2)
⊢ Small.{u, u3} (↑(Set.image2 f s t) : Type u3)
have rw : Small.{u, u3} (↑(Function.uncurry f '' s ×ˢ t) : Type u3)
Tactic: rw [← Set.image_uncurry_prod]
-- Lean 4 proof step from Mathlib.Logic.Small.Set (goal)
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst : Small.{u, u1} (↑s : Type u1)
inst_1 : Small.{u, u1} (↑t : Type u1)
⊢ Small.{u, u1} (↑(s ∪ t) : Type u1)
have rw : Small.{u, u1}
  (↑(Set.range (ι := { x : α // x ∈ s } ⊕ { x : α // x ∈ t })
        (Sum.elim (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t)))) :
    Type u1)
Tactic: rw [← Subtype.range_val (s := s), ← Subtype.range_val (s := t), ← Set.Sum.elim_range]
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
α : Sort u_1
p : α → Prop
h : ∃! a : α, p a
a : α
ha : (fun (a : α) ↦ p a) a
he : ∀ (y : α), (fun (a : α) ↦ p a) y → y = a
x : Subtype p
b : α
hb : p b
⊢ Eq.{max 1 u_1} (Subtype.mk (p := p) b hb) default.{max 1 u_1}
have e_val : b = a
Tactic: congr
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq : ∀ (a : α), a = default
⊢ Eq.{max 1 u_1} { default := x, uniq := h : Unique α } { default := y, uniq := uniq }
have e_toInhabited : x = y
Tactic: congr
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq : ∀ (a : α), a = default
⊢ x = y
have e_toInhabited : default = y
Tactic: rw [h x, h y]
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq : ∀ (a : α), a = default
e_toInhabited : default = y
⊢ x = y
have e_toInhabited₁ : Eq.{u_1} (α := α) default default
Tactic: rw [h x, h y]
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
α : Sort u
inst : Subsingleton α
inst_1 : Nonempty α
⊢ Nonempty.{max 1 u} (Unique α)
have inhabit : ∀ (inhabited_h : Inhabited α), Nonempty.{max 1 u} (Unique α)
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
α : Sort u
h : Nonempty.{max 1 u} (Unique α)
u : Unique α
⊢ Subsingleton α ∧ Nonempty α
have left : Subsingleton α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
α : Sort u
h : Nonempty.{max 1 u} (Unique α)
u : Unique α
left : Subsingleton α
⊢ Subsingleton α ∧ Nonempty α
have right : Nonempty α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
α : Sort u_1
inst : Unique α
β : α → Sort v
f : (a : α) → β a
i x : α
h : i ≍ x
⊢ HEq (f i) (β := β default) (Function.const α (f default) x)
have rw : HEq (α := β default) (f default) (β := β default) (Function.const α (f default) x)
Tactic: rw [Subsingleton.elim i default]
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
A : Sort u_2
B : Sort u_3
inst : Unique A
inst_1 : Unique B
f : A → B
⊢ Function.Bijective f
have rw : ∃ (g : B → A), Function.LeftInverse g f ∧ Function.RightInverse g f
Tactic: rw [Function.bijective_iff_has_inverse]
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
A : Sort u_2
B : Sort u_3
inst : Unique A
inst_1 : Unique B
f : A → B
⊢ ∃ (g : B → A), Function.LeftInverse g f ∧ Function.RightInverse g f
have refine_1 : Function.LeftInverse default f
Tactic: refine ⟨default, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
A : Sort u_2
B : Sort u_3
inst : Unique A
inst_1 : Unique B
f : A → B
refine_1 : Function.LeftInverse default f
⊢ ∃ (g : B → A), Function.LeftInverse g f ∧ Function.RightInverse g f
have refine_2 : Function.RightInverse default f
Tactic: refine ⟨default, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Unique (goal)
Goal:
α : Sort u_1
y : α
x_1 : { x : α // y = x }
x : α
hx : y = x
⊢ Eq.{max 1 u_1} (Subtype.mk (p := fun (x : α) ↦ y = x) x hx) (Subtype.mk (p := fun (x : α) ↦ y = x) y ⋯)
have subst : Eq.{max 1 u_1} (Subtype.mk (p := fun (x : α) ↦ y = x) y sorry) (Subtype.mk (p := fun (x : α) ↦ y = x) y sorry)
Tactic: subst hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Logic.UnivLE (goal)
Goal:
⊢ ¬UnivLE.{u + 1, u}
have simp : ∃ (x : Type (u + 1)), ∀ (x_1 : Type u), ¬Nonempty.{u + 2} (x ≃ x_1)
Tactic: simp only [univLE_iff, small_iff, not_forall, not_exists]
-- Lean 4 proof step from Mathlib.MeasureTheory.Category.MeasCat (goal)
Goal:
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ ∫⁻ (x : ℝ≥0∞), x ∂μ.join =
    ∫⁻ (x : ℝ≥0∞), x ∂Measure.map (fun (m : MeasureTheory.Measure ℝ≥0∞) ↦ ∫⁻ (x : ℝ≥0∞), x ∂m) μ
have hf : Measurable (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x
Tactic: rw [Measure.lintegral_join, lintegral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Category.MeasCat (goal)
Goal:
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
hf : Measurable (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x
⊢ ∫⁻ (x : ℝ≥0∞), x ∂μ.join =
    ∫⁻ (x : ℝ≥0∞), x ∂Measure.map (fun (m : MeasureTheory.Measure ℝ≥0∞) ↦ ∫⁻ (x : ℝ≥0∞), x ∂m) μ
have hg : Measurable (β := ℝ≥0∞) fun (m : MeasureTheory.Measure ℝ≥0∞) ↦ ∫⁻ (x : ℝ≥0∞), x ∂m
Tactic: rw [Measure.lintegral_join, lintegral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Category.MeasCat (goal)
Goal:
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
hf : Measurable (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x
hg : Measurable (β := ℝ≥0∞) fun (m : MeasureTheory.Measure ℝ≥0∞) ↦ ∫⁻ (x : ℝ≥0∞), x ∂m
⊢ ∫⁻ (x : ℝ≥0∞), x ∂μ.join =
    ∫⁻ (x : ℝ≥0∞), x ∂Measure.map (fun (m : MeasureTheory.Measure ℝ≥0∞) ↦ ∫⁻ (x : ℝ≥0∞), x ∂m) μ
have rw : AEMeasurable (β := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ x) μ.join
Tactic: rw [Measure.lintegral_join, lintegral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (hypothesis)
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
⊢ MeasurableSet u
have hu₁ : TopologicalSpace.IsOpen u
Tactic: rw [hs] at hu
Cleared hypotheses: hu