awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
⊢ ¬c₁ :: cs₁ < []
have cons : [] < c₁ :: cs₁
Tactic: apply not_lt_of_gt
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator } { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator } =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂
have cons : (if { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.hasNext = true then
      if { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.hasNext = true then
        if
            { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.curr =
              { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.curr then
          ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.next
            { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.next
        else
          decide
            ({ s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.curr <
              { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.curr)
      else true
    else false) =
    true ↔
  c₁ :: cs₁ < c₂ :: cs₂
Tactic: unfold ltb
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ (if { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.hasNext = true then
        if { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.hasNext = true then
          if
              { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.curr =
                { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.curr then
            ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.next
              { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.next
          else
            decide
              ({ s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.curr <
                { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.curr)
        else true
      else false) =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂
have cons : (if c₁ = c₂ then
    ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
        { s := ofList (c₂ :: cs₂), i := 0 + c₂ : Legacy.Iterator } =
      true
  else c₁ < c₂) ↔
  c₁ :: cs₁ < c₂ :: cs₂
Tactic: simp only [Legacy.Iterator.hasNext, Pos.Raw.byteIdx_zero, rawEndPos_ofList, utf8Len_cons,
        add_pos_iff, Char.utf8Size_pos, or_true, decide_true, ↓reduceIte, Legacy.Iterator.curr,
        Pos.Raw.get, String.toList_ofList, Pos.Raw.utf8GetAux, Legacy.Iterator.next, Pos.Raw.next,
        Bool.ite_eq_true_distrib, decide_eq_true_eq]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ (if c₁ = c₂ then
      ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
          { s := ofList (c₂ :: cs₂), i := 0 + c₂ : Legacy.Iterator } =
        true
    else c₁ < c₂) ↔
    c₁ :: cs₁ < c₂ :: cs₂
have pos : ∀ (h : c₁ = c₂),
  ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
        { s := ofList (c₂ :: cs₂), i := 0 + c₂ : Legacy.Iterator } =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
pos :
  ∀ (h : c₁ = c₂),
    ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
          { s := ofList (c₂ :: cs₂), i := 0 + c₂ : Legacy.Iterator } =
        true ↔
      c₁ :: cs₁ < c₂ :: cs₂
⊢ (if c₁ = c₂ then
      ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
          { s := ofList (c₂ :: cs₂), i := 0 + c₂ : Legacy.Iterator } =
        true
    else c₁ < c₂) ↔
    c₁ :: cs₁ < c₂ :: cs₂
have neg : ∀ (h : ¬c₁ = c₂), c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : c₁ = c₂
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
        { s := ofList (c₂ :: cs₂), i := 0 + c₂ : Legacy.Iterator } =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂
have pos : ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
      { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
    true ↔
  c₁ :: cs₁ < c₁ :: cs₂
Tactic: subst c₂
Cleared hypotheses: c₂, h
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
cs₂ : List Char
this :
  ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
      { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
    ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 }
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
        { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
      true ↔
    c₁ :: cs₁ < c₁ :: cs₂
have rw : ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList cs₂, i := 0 : Legacy.Iterator } = true ↔
  c₁ :: cs₁ < c₁ :: cs₂
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
cs₂ : List Char
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
        { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
      true ↔
    c₁ :: cs₁ < c₁ :: cs₂
have pos : ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
    { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
  ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 }
Tactic: suffices ltb ⟨ofList (c₁ :: cs₁), (0 : Pos.Raw) + c₁⟩
            ⟨ofList (c₁ :: cs₂), (0 : Pos.Raw) + c₁⟩ =
              ltb ⟨ofList cs₁, 0⟩ ⟨ofList cs₂, 0⟩ by
          rw [this]; exact (ih cs₂).trans List.lex_cons_iff.symm
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂
have neg : ∀ (e : c₁ :: cs₁ < c₂ :: cs₂), c₁ < c₂
Tactic: refine ⟨List.Lex.rel, fun e ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
e : c₁ :: cs₁ < c₂ :: cs₂
⊢ c₁ < c₂
have neg : c₁ < c₂ → c₁ < c₂
Tactic: cases e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
e : c₁ :: cs₁ < c₂ :: cs₂
neg : c₁ < c₂ → c₁ < c₂
⊢ c₁ < c₂
have neg₁ : ∀ (h : ¬c₁ = c₁), List.Lex (fun (x1 x2 : Char) ↦ x1 < x2) cs₁ cs₂ → c₁ < c₁
Tactic: cases e
Cleared hypotheses: c₂, h, e
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
s : String
h : s ≠ ""
⊢ s.toList = Legacy.front s :: (Legacy.drop s 1).toList
have obtain : ∀ (l : List Char) (h : ofList l ≠ ""), (ofList l).toList = Legacy.front (ofList l) :: (Legacy.drop (ofList l) 1).toList
Tactic: obtain ⟨l, rfl⟩ := s.exists_eq_ofList
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
a b c : String
⊢ a ≤ b → b ≤ c → a ≤ c
have simp : a.toList ≤ b.toList → b.toList ≤ c.toList → a.toList ≤ c.toList
Tactic: simp only [le_iff_toList_le]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
a b : String
⊢ a ≤ b → b ≤ a → a = b
have simp : a.toList ≤ b.toList → b.toList ≤ a.toList → a.toList = b.toList
Tactic: simp only [le_iff_toList_le, ← toList_inj]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
a b : String
⊢ a ≤ b ∨ b ≤ a
have simp : a.toList ≤ b.toList ∨ b.toList ≤ a.toList
Tactic: simp only [le_iff_toList_le]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
a b : String
⊢ compare a b = compareOfLessAndEq a b
have simp : (if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
  if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
Tactic: simp +instances only [compare, compareOfLessAndEq, instLT, List.instLT, lt_iff_toList_lt]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
a b : String
⊢ (if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have pos : a.toList.lt b.toList → Ordering.lt = Ordering.lt
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
a b : String
pos : a.toList.lt b.toList → Ordering.lt = Ordering.lt
⊢ (if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have pos₁ : ¬a.toList.lt b.toList → a = b → Ordering.eq = Ordering.eq
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
a b : String
pos : a.toList.lt b.toList → Ordering.lt = Ordering.lt
pos₁ : ¬a.toList.lt b.toList → a = b → Ordering.eq = Ordering.eq
⊢ (if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have neg : ¬a.toList.lt b.toList → ¬a = b → Ordering.gt = Ordering.gt
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (∃ (fab : (ab : α ⊕ β) → γ ab), p fab) ↔
    ∃ (fa : (val : α) → γ (inl val)),
      ∃ (fb : (val : β) → γ (inr val)), p fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) fa fb t
have rw : (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)),
      ¬p fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) fa fb t) ↔
  ∃ (fa : (val : α) → γ (inl val)),
    ∃ (fb : (val : β) → γ (inr val)), p fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) fa fb t
Tactic: rw [← not_forall_not, forall_sum]
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x y : α ⊕ β
h : x = y
⊢ rec (motive := P) f g x = cast ⋯ (rec (motive := P) f g y)
have refl : rec (motive := P) f g x = cast sorry (rec (motive := P) f g x)
Tactic: cases h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
x : α ⊕ β
a : α
⊢ x = inl a ↔ ∃ (h : x.isLeft = true), x.getLeft h = a
have inl : ∀ (val : α),
  Eq (α := α ⊕ β) (inl val) (inl a) ↔ ∃ (h : isLeft.{u, v} (β := β) (inl val) = true), getLeft (inl val) h = a
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
x : α ⊕ β
a : α
inl :
  ∀ (val : α),
    Eq (α := α ⊕ β) (Sum.inl val) (Sum.inl a) ↔
      ∃ (h : isLeft.{u, v} (β := β) (Sum.inl val) = true), getLeft (Sum.inl val) h = a
⊢ x = Sum.inl a ↔ ∃ (h : x.isLeft = true), x.getLeft h = a
have inr : ∀ (val : β), inr val = Sum.inl a ↔ ∃ (h : isLeft.{u, v} (α := α) (inr val) = true), getLeft (inr val) h = a
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
x : α ⊕ β
b : β
⊢ x = inr b ↔ ∃ (h : x.isRight = true), x.getRight h = b
have inl : ∀ (val : α), inl val = inr b ↔ ∃ (h : isRight.{u, v} (β := β) (inl val) = true), getRight (inl val) h = b
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
x : α ⊕ β
b : β
inl :
  ∀ (val : α), Sum.inl val = inr b ↔ ∃ (h : isRight.{u, v} (β := β) (Sum.inl val) = true), getRight (Sum.inl val) h = b
⊢ x = inr b ↔ ∃ (h : x.isRight = true), x.getRight h = b
have inr : ∀ (val : β),
  Eq (α := α ⊕ β) (inr val) (inr b) ↔ ∃ (h : isRight.{u, v} (α := α) (inr val) = true), getRight (inr val) h = b
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq β
inst_1 : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
⊢ update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x (inr j) = update (β := fun (a : β) ↦ γ) (f ∘ inr) i x j
have rw : update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x (inr j) = (update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x ∘ inr) j
Tactic: rw [← update_inr_comp_inr, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq β
inst_1 : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
rw : update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x (inr j) = (update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x ∘ inr) j
⊢ update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x (inr j) = update (β := fun (a : β) ↦ γ) (f ∘ inr) i x j
have rw₁ : update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x (inr j) = update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x (inr j)
Tactic: rw [← update_inr_comp_inr, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
⊢ x.isLeft = true ↔ y.isLeft = true
have inl : ∀ {a : α} {c : γ}, r a c → (isLeft.{u, v} (β := β) (inl a) = true ↔ isLeft.{u_1, u_2} (β := δ) (inl c) = true)
Tactic: cases h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
inl :
  ∀ {a : α} {c : γ}, r a c → (isLeft.{u, v} (β := β) (Sum.inl a) = true ↔ isLeft.{u_1, u_2} (β := δ) (Sum.inl c) = true)
⊢ x.isLeft = true ↔ y.isLeft = true
have inr : ∀ {b : β} {d : δ}, s b d → (isLeft.{u, v} (α := α) (inr b) = true ↔ isLeft.{u_1, u_2} (α := γ) (inr d) = true)
Tactic: cases h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
⊢ x.isRight = true ↔ y.isRight = true
have inl : ∀ {a : α} {c : γ}, r a c → (isRight.{u, v} (β := β) (inl a) = true ↔ isRight.{u_1, u_2} (β := δ) (inl c) = true)
Tactic: cases h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
inl :
  ∀ {a : α} {c : γ},
    r a c → (isRight.{u, v} (β := β) (Sum.inl a) = true ↔ isRight.{u_1, u_2} (β := δ) (Sum.inl c) = true)
⊢ x.isRight = true ↔ y.isRight = true
have inr : ∀ {b : β} {d : δ}, s b d → (isRight.{u, v} (α := α) (inr b) = true ↔ isRight.{u_1, u_2} (α := γ) (inr d) = true)
Tactic: cases h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
c : γ
h : LiftRel r s x (inl c)
⊢ x.isLeft = true
have inl : ∀ {a : α}, r a c → isLeft.{u, v} (β := β) (inl a) = true
Tactic: cases h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
a : α
h : LiftRel r s (inl a) y
⊢ y.isLeft = true
have inl : ∀ {c : γ}, r a c → isLeft.{u_1, u_2} (β := δ) (inl c) = true
Tactic: cases h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
d : δ
h : LiftRel r s x (inr d)
⊢ x.isRight = true
have inr : ∀ {b : β}, s b d → isRight.{u, v} (α := α) (inr b) = true
Tactic: cases h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
b : β
h : LiftRel r s (inr b) y
⊢ y.isRight = true
have inr : ∀ {d : δ}, s b d → isRight.{u_1, u_2} (α := γ) (inr d) = true
Tactic: cases h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
⊢ ∃ (a : α), f a = c
have inl : ∀ (a : α) (h : Sum.map f g (inl a) = inl c), ∃ (a : α), f a = c
Tactic: obtain ⟨a | b, h⟩ := h (inl c)
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
inl : ∀ (a : α) (h : Sum.map f g (Sum.inl a) = Sum.inl c), ∃ (a : α), f a = c
⊢ ∃ (a : α), f a = c
have inr : ∀ (b : β) (h : Sum.map f g (inr b) = Sum.inl c), ∃ (a : α), f a = c
Tactic: obtain ⟨a | b, h⟩ := h (inl c)
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
d : δ
⊢ ∃ (a : β), g a = d
have inl : ∀ (a : α) (h : Sum.map f g (inl a) = inr d), ∃ (a : β), g a = d
Tactic: obtain ⟨a | b, h⟩ := h (inr d)
-- Lean 4 proof step from Mathlib.Data.Sum.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
d : δ
inl : ∀ (a : α) (h : Sum.map f g (Sum.inl a) = inr d), ∃ (a : β), g a = d
⊢ ∃ (a : β), g a = d
have inr : ∀ (b : β) (h : Sum.map f g (inr b) = inr d), ∃ (a : β), g a = d
Tactic: obtain ⟨a | b, h⟩ := h (inr d)
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ c ∈ sumLift₂ f g a b ↔
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
have mp : c ∈ sumLift₂ f g a b →
  (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
mp :
  c ∈ sumLift₂ f g a b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
⊢ c ∈ sumLift₂ f g a b ↔
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
have mpr : ((∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂) →
  c ∈ sumLift₂ f g a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ c ∈ sumLift₂ f g a b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
have mp : ∀ (a : α₁),
  c ∈ sumLift₂ f g (inl a) b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
Tactic: rcases a with a | a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
mp :
  ∀ (a : α₁),
    c ∈ sumLift₂ f g (inl a) b →
      (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
⊢ c ∈ sumLift₂ f g a b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
have mp₁ : ∀ (a : α₂),
  c ∈ sumLift₂ f g (inr a) b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), inr a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
Tactic: rcases a with a | a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₁
⊢ c ∈ sumLift₂ f g (inl a) b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
have mp : ∀ (b : β₁),
  c ∈ sumLift₂ f g (inl a) (inl b) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
        Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
Tactic: rcases b with b | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₁
mp :
  ∀ (b : β₁),
    c ∈ sumLift₂ f g (inl a) (inl b) →
      (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
⊢ c ∈ sumLift₂ f g (inl a) b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
have mp₁ : ∀ (b : β₂),
  c ∈ sumLift₂ f g (inl a) (inr b) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
Tactic: rcases b with b | b
Cleared hypotheses: b