awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
have left : ∀ (k : ι) (hi : i < k) (hj : k < j),
  ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
Tactic: obtain ⟨k, hi, hj⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
have left : ∀ (c : α k), ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
Tactic: obtain ⟨c⟩ : Nonempty (α k) := inferInstance
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
have right : ∀ (c : α i) (ha : a < c) (hb : c < b),
  ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
Tactic: obtain ⟨c, ha, hb⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
have left : ∀ (c : α i) (ha : a < c),
  ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
Tactic: obtain ⟨c, ha⟩ := exists_gt a
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
have right : ∀ (c : α i) (ha : a < c) (hb : c < b),
  ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
Tactic: obtain ⟨c, ha, hb⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
have left : ∀ (c : α j) (hb : c < b),
  ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
Tactic: obtain ⟨c, hb⟩ := exists_lt b
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
have right : ∀ (c : α i) (ha : a < c) (hb : c < b),
  ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
Tactic: obtain ⟨c, ha, hb⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMaxOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
⊢ ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
have obtain : ∀ (j : ι) (h : i < j), ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
Tactic: obtain ⟨j, h⟩ := exists_gt i
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMaxOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : i < j
⊢ ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
have obtain : ∀ (b : α j), ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
Tactic: obtain ⟨b⟩ : Nonempty (α j) := inferInstance
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMinOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
⊢ ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
have obtain : ∀ (j : ι) (h : j < i), ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain ⟨j, h⟩ := exists_lt i
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMinOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : j < i
⊢ ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
have obtain : ∀ (b : α j), ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain ⟨b⟩ : Nonempty (α j) := inferInstance
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a : α i
⊢ ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
have obtain : ∀ (b : α i) (h : a < b), ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
Tactic: obtain ⟨b, h⟩ := exists_gt a
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a : α i
⊢ ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
have obtain : ∀ (b : α i) (h : b < a), ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain ⟨b, h⟩ := exists_lt a
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom
have pos : ∀ (h : o.Dom), o.toOption.isSome = true ↔ o.Dom
Tactic: by_cases h : o.Dom
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
pos : ∀ (h : o.Dom), o.toOption.isSome = true ↔ o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom
have neg : ∀ (h : ¬o.Dom), o.toOption.isSome = true ↔ o.Dom
Tactic: by_cases h : o.Dom
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
⊢ o.toOption = none ↔ ¬o.Dom
have pos : ∀ (h : o.Dom), o.toOption = none ↔ ¬o.Dom
Tactic: by_cases h : o.Dom
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
pos : ∀ (h : o.Dom), o.toOption = none ↔ ¬o.Dom
⊢ o.toOption = none ↔ ¬o.Dom
have neg : ∀ (h : ¬o.Dom), o.toOption = none ↔ ¬o.Dom
Tactic: by_cases h : o.Dom
-- Lean 4 proof step from Mathlib.Data.Part (hypothesis)
Goal:
α : Type u_1
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o : Part α }.Dom ↔ { Dom := pd, get := p : Part α }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o : Part α }.Dom) (h₂ : { Dom := pd, get := p : Part α }.Dom),
    { Dom := od, get := o : Part α }.get h₁ = { Dom := pd, get := p }.get h₂
⊢ { Dom := od, get := o : Part α } = { Dom := pd, get := p }
have t : od = pd
Tactic: have t : od = pd := propext H1
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o : Part α }.Dom ↔ { Dom := pd, get := p : Part α }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o : Part α }.Dom) (h₂ : { Dom := pd, get := p : Part α }.Dom),
    { Dom := od, get := o : Part α }.get h₁ = { Dom := pd, get := p }.get h₂
t : od = pd
⊢ { Dom := od, get := o : Part α } = { Dom := pd, get := p }
have refl : ∀ (p : od → α) (H1 : { Dom := od, get := o : Part α }.Dom ↔ { Dom := od, get := p : Part α }.Dom)
  (H2 :
    ∀ (h₁ : { Dom := od, get := o : Part α }.Dom) (h₂ : { Dom := od, get := p : Part α }.Dom),
      { Dom := od, get := o : Part α }.get h₁ = { Dom := od, get := p }.get h₂),
  { Dom := od, get := o : Part α } = { Dom := od, get := p }
Tactic: cases t
Cleared hypotheses: pd, p, H1, H2, t
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
od : Prop
o p : od → α
H1 : { Dom := od, get := o : Part α }.Dom ↔ { Dom := od, get := p : Part α }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o : Part α }.Dom) (h₂ : { Dom := od, get := p : Part α }.Dom),
    { Dom := od, get := o : Part α }.get h₁ = { Dom := od, get := p }.get h₂
⊢ { Dom := od, get := o : Part α } = { Dom := od, get := p }
have refl : { Dom := od, get := p : Part α } = { Dom := od, get := p }
Tactic: rw [show o = p from funext fun p => H2 p p]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
⊢ o ≠ none ↔ ∃ (x : α), o = some x
have mp : o ≠ none → ∃ (x : α), o = some x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
mp : o ≠ none → ∃ (x : α), o = some x
⊢ o ≠ none ↔ ∃ (x : α), o = some x
have mpr : (∃ (x : α), o = some x) → o ≠ none
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
⊢ o ≠ none → ∃ (x : α), o = some x
have mp : o.Dom → ∃ (x : α), o = some x
Tactic: rw [Ne, eq_none_iff', not_not]
-- Lean 4 proof step from Mathlib.Data.Part (hypothesis)
Goal:
α : Type u_1
a b : Part α
ha : a.Dom
hb : a.get ha ∈ b
⊢ a = b
have hb' : b.Dom
Tactic: have hb' : b.Dom := Part.dom_iff_mem.mpr ⟨a.get ha, hb⟩
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
a b : Part α
ha : a.Dom
hb : a.get ha ∈ b
hb' : b.Dom
⊢ a = b
have rwa : ∀ (hb : a.get ha = b.get hb'), a = b
Tactic: rwa [← eq_get_iff_mem hb', eq_iff_of_dom ha hb'] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
a b : Part α
ha : a.Dom
hb : a.get ha ∈ b
hb' : b.Dom
rwa : ∀ (hb : a.get ha = b.get hb'), a = b
⊢ a = b
have rwa₁ : ∀ (hb : a = b), a = b
Tactic: rwa [← eq_get_iff_mem hb', eq_iff_of_dom ha hb'] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
⊢ Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o
have pos : ∀ (h : o.Dom), Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o
Tactic: by_cases h : o.Dom
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
pos : ∀ (h : o.Dom), Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o
⊢ Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o
have neg : ∀ (h : ¬o.Dom), Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o
Tactic: by_cases h : o.Dom
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o
have neg : ¬a ∈ o
Tactic: simp only [h, ↓reduceDIte, Option.mem_def, reduceCtorEq, false_iff]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
⊢ o.toOption = Option.some a ↔ a ∈ o
have rw : a ∈ o.toOption ↔ a ∈ o
Tactic: rw [← Option.mem_def, mem_toOption]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
rw : a ∈ o.toOption ↔ a ∈ o
⊢ o.toOption = Option.some a ↔ a ∈ o
have rw₁ : a ∈ o ↔ a ∈ o
Tactic: rw [← Option.mem_def, mem_toOption]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_4
β : Type u_5
a : Part α
inst : Decidable a.Dom
b : β
f : α → β
⊢ a.toOption.elim b f = if h : a.Dom then f (a.get h) else b
have pos : ∀ (h : a.Dom), a.toOption.elim b f = f (a.get h)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_4
β : Type u_5
a : Part α
inst : Decidable a.Dom
b : β
f : α → β
pos : ∀ (h : a.Dom), a.toOption.elim b f = f (a.get h)
⊢ a.toOption.elim b f = if h : a.Dom then f (a.get h) else b
have neg : ∀ (h : ¬a.Dom), a.toOption.elim b f = b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_4
β : Type u_5
a : Part α
inst : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ a.toOption.elim b f = f (a.get h)
have pos : (Option.some (a.get h)).elim b f = f (a.get h)
Tactic: rw [h.toOption]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_4
β : Type u_5
a : Part α
inst : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ a.toOption.elim b f = b
have neg : Option.elim Option.none b f = b
Tactic: rw [Part.toOption_eq_none_iff.2 h]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_4
o : Option α
h₁ : (↑o : Part α).Dom
h₂ : { Dom := o.isSome = true, get := o.get : Part α }.Dom
⊢ (↑o : Part α).get h₁ = { Dom := o.isSome = true, get := o.get }.get h₂
have none : ∀ (h₁ : Dom.{u_4} (α := α) (↑Option.none : Part α))
  (h₂ : Dom.{u_4} (α := α) { Dom := Option.isSome.{u_4} (α := α) Option.none = true, get := Option.get Option.none }),
  get (↑Option.none : Part α) h₁ =
    get { Dom := Option.isSome.{u_4} (α := α) Option.none = true, get := Option.get Option.none } h₂
Tactic: cases o
Cleared hypotheses: o, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_4
o : Option α
h₁ : (↑o : Part α).Dom
h₂ : { Dom := o.isSome = true, get := o.get : Part α }.Dom
none :
  ∀ (h₁ : Dom.{u_4} (α := α) (↑Option.none : Part α))
    (h₂ : Dom.{u_4} (α := α) { Dom := Option.isSome.{u_4} (α := α) Option.none = true, get := Option.get Option.none }),
    get (↑Option.none : Part α) h₁ =
      get { Dom := Option.isSome.{u_4} (α := α) Option.none = true, get := Option.get Option.none } h₂
⊢ (↑o : Part α).get h₁ = { Dom := o.isSome = true, get := o.get }.get h₂
have some : ∀ (val : α) (h₁ : (↑(Option.some val) : Part α).Dom)
  (h₂ : { Dom := (Option.some val).isSome = true, get := (Option.some val).get : Part α }.Dom),
  (↑(Option.some val) : Part α).get h₁ = { Dom := (Option.some val).isSome = true, get := (Option.some val).get }.get h₂
Tactic: cases o
Cleared hypotheses: o, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Option α
⊢ (↑o : Part α).toOption = o
have none : Eq.{u_1 + 1} (α := Option α) (toOption (↑Option.none : Part α)) Option.none
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
o : Option α
none : Eq.{u_1 + 1} (α := Option α) (toOption (↑Option.none : Part α)) Option.none
⊢ (↑o : Part α).toOption = o
have some : ∀ (val : α), (↑(Option.some val) : Part α).toOption = Option.some val
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
⊢ x ≤ y ∨ y ≤ x
have inl : ∀ (h : x = none), x ≤ y ∨ y ≤ x
Tactic: rcases Part.eq_none_or_eq_some x with (h | ⟨b, h₀⟩)
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
inl : ∀ (h : x = none), x ≤ y ∨ y ≤ x
⊢ x ≤ y ∨ y ≤ x
have inr : ∀ (b : α) (h₀ : x = some b), x ≤ y ∨ y ≤ x
Tactic: rcases Part.eq_none_or_eq_some x with (h | ⟨b, h₀⟩)
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ x ≤ y ∨ y ≤ x
have inl : none ≤ y ∨ y ≤ none
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y ∨ y ≤ none
have inl : none ≤ y
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ x ≤ y ∨ y ≤ x
have inr : y ≤ x
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
have inr : ∀ (h₀ : b ∈ x) (b' : α) (h₁ : b' ∈ y), b' ∈ x
Tactic: rw [Part.eq_some_iff] at h₀
Cleared hypotheses: h₀, b', h₁
-- Lean 4 proof step from Mathlib.Data.Part (hypothesis)
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
have hx₁ : b ∈ z
Tactic: have hx := hx _ h₀
-- Lean 4 proof step from Mathlib.Data.Part (hypothesis)
Goal:
α : Type u_1
x y z : Part α
hx_1 : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ x
have hy₁ : b' ∈ z
Tactic: have hy := hy _ h₁
-- Lean 4 proof step from Mathlib.Data.Part (hypothesis)
Goal:
α : Type u_1
x y z : Part α
hx_1 : x ≤ z
hy_1 : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
hy : b' ∈ z
⊢ b' ∈ x
have hx₁ : b = b'
Tactic: have hx := Part.mem_unique hx hy
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
x y z : Part α
hx_1 : x ≤ z
hy_1 : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx_2 : b ∈ z
hy : b' ∈ z
hx : b = b'
⊢ b' ∈ x
have inr : ∀ (h₁ : b ∈ y) (hy : b ∈ z), b ∈ x
Tactic: subst hx
Cleared hypotheses: b', h₁, hy, hx
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
p : Prop
f : p → Part α
h : p
⊢ assert p f = f h
have H : ∀ (a : α), a ∈ assert p f ↔ a ∈ f h
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ assert p f = none
have H : ∀ (a : α), a ∈ assert p f ↔ Membership.mem (γ := Part α) none a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
⊢ o.bind f = f (o.get h)
have H : ∀ (b : β), b ∈ o.bind f ↔ b ∈ f (o.get h)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ b ∈ o.bind f ↔ b ∈ f (o.get h)
have H : (∃ (a : α), a ∈ o ∧ b ∈ f a) ↔ b ∈ f (o.get h)
Tactic: simp only [Part.mem_bind_iff]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ (a : α), a ∈ o ∧ b ∈ f a) ↔ b ∈ f (o.get h)
have H : (∃ (a : α), a ∈ o ∧ b ∈ f a) → b ∈ f (o.get h)
Tactic: refine ⟨?_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
o : Part α
a : α
h : a ∈ o
f : α → Part β
⊢ o.bind f = f a
have rw : (some a).bind f = f a
Tactic: rw [eq_some_iff.2 h, bind_some]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
o : Part α
a : α
h : a ∈ o
f : α → Part β
rw : (some a).bind f = f a
⊢ o.bind f = f a
have rw₁ : f a = f a
Tactic: rw [eq_some_iff.2 h, bind_some]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst : Decidable o.Dom
inst_1 : (a : α) → Decidable (f a).Dom
inst_2 : Decidable (o.bind f).Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption
have pos : ∀ (h : o.Dom), (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption
Tactic: by_cases h : o.Dom
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst : Decidable o.Dom
inst_1 : (a : α) → Decidable (f a).Dom
inst_2 : Decidable (o.bind f).Dom
pos : ∀ (h : o.Dom), (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption
have neg : ∀ (h : ¬o.Dom), (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption
Tactic: by_cases h : o.Dom
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst : Decidable o.Dom
inst_1 : (a : α) → Decidable (f a).Dom
inst_2 : Decidable (o.bind f).Dom
h : o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption
have pos : (f (o.get h)).toOption = (Option.some (o.get h)).elim Option.none fun (a : α) ↦ (f a).toOption
Tactic: simp_rw [h.toOption, h.bind]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst : Decidable o.Dom
inst_1 : (a : α) → Decidable (f a).Dom
inst_2 : Decidable (o.bind f).Dom
h : ¬o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption
have neg : (o.bind f).toOption = Option.elim Option.none Option.none fun (a : α) ↦ (f a).toOption
Tactic: rw [Part.toOption_eq_none_iff.2 h]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ a ∈ (f.bind g).bind k ↔ Membership.mem (γ := Part γ) (f.bind fun (x : α) ↦ (g x).bind k) a
have simp : (∃ (a_1 : β), (∃ (a : α), a ∈ f ∧ a_1 ∈ g a) ∧ a ∈ k a_1) ↔ ∃ (a_1 : α), a_1 ∈ f ∧ ∃ (a_2 : β), a_2 ∈ g a_1 ∧ a ∈ k a_2
Tactic: simp only [mem_bind_iff]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (map f x).bind g = x.bind fun (y : α) ↦ g (f y)
have rw : Eq.{u_4 + 1} (α := Part γ) (x.bind fun (x : α) ↦ (some (f x)).bind g) (x.bind fun (y : α) ↦ g (f y))
Tactic: rw [← bind_some_eq_map, bind_assoc]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ map g (x.bind f) = x.bind fun (y : α) ↦ map g (f y)
have rw : Eq.{u_4 + 1} (α := Part γ) (x.bind fun (x : α) ↦ (f x).bind fun (y : β) ↦ some (g y)) (x.bind fun (y : α) ↦ map g (f y))
Tactic: rw [← bind_some_eq_map, bind_assoc]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
α_1 : Type u_4
f : Part α_1
⊢ id <$> f = f
have mk : ∀ (Dom : Prop) (get : Dom → α_1), id <$> { Dom := Dom, get := get : Part α_1 } = { Dom := Dom, get := get }
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map f o = o
have rw : map id o = o
Tactic: rw [show f = id from funext H]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
x : Part α
⊢ x.bind some = x
have rw : map (fun (y : α) ↦ y) x = x
Tactic: rw [bind_some_eq_map]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y
have mp : x >>= f ≤ y → ∀ (a : α), a ∈ x → f a ≤ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
mp : x >>= f ≤ y → ∀ (a : α), a ∈ x → f a ≤ y
⊢ x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y
have mpr : (∀ (a : α), a ∈ x → f a ≤ y) → x >>= f ≤ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Part (hypothesis)
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
⊢ b ∈ f a → b ∈ y
have h₁ : b ∈ x >>= f → b ∈ y
Tactic: have h := h b
-- Lean 4 proof step from Mathlib.Data.Part (hypothesis)
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h_1 : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : b ∈ x >>= f → b ∈ y
⊢ b ∈ f a → b ∈ y
have h₁ : ∀ (x_1 : α), x_1 ∈ x → b ∈ f x_1 → b ∈ y
Tactic: simp only [and_imp, bind_eq_bind, mem_bind_iff, exists_imp] at h
Cleared hypotheses: h