awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : ZNum.zero.div 0 = 0
⊢ n.div 0 = 0
have pos : ∀ (a : PosNum), (pos a).div 0 = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : ZNum.zero.div 0 = 0
pos : ∀ (a : PosNum), (ZNum.pos a).div 0 = 0
⊢ n.div 0 = 0
have neg : ∀ (a : PosNum), (neg a).div 0 = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
⊢ (↑(n.div' d) : ℤ) = HDiv.hDiv (α := ℤ) (↑(pos n) : ℤ) (↑(pos d) : ℤ)
have rw : (↑(↑(n.div' d) : ℕ) : ℤ) = HDiv.hDiv (α := ℤ) (↑(pos n) : ℤ) (↑(pos d) : ℤ)
Tactic: rw [← Num.to_nat_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
⊢ -(↑(n.div' d) : ℤ) = HDiv.hDiv (α := ℤ) (↑(pos n) : ℤ) (↑(neg d) : ℤ)
have rw : -(↑(↑(n.div' d) : ℕ) : ℤ) = HDiv.hDiv (α := ℤ) (↑(pos n) : ℤ) (↑(neg d) : ℤ)
Tactic: rw [← Num.to_nat_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
⊢ -(↑(n.pred' / Num.pos d).succ' : ℤ) = HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)
have rw : -(↑(HDiv.hDiv (α := ℕ) (↑n.pred' : ℕ) (↑(Num.pos d) : ℕ) + 1) : ℤ) =
  -HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1 / HAdd.hAdd (α := ℤ) (↑(↑d.pred' : ℕ) : ℤ) 1
Tactic: rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
        Num.div_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
⊢ -[HDiv.hDiv (α := ℕ) (↑n.pred' : ℕ) (↑d : ℕ)+1] = -[(↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1+1]
have rw : -[(↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1+1] = -[(↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1+1]
Tactic: rw [d.to_nat_eq_succ_pred]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
⊢ (↑(n.pred' / Num.pos d).succ' : ℤ) = HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (-(↑d : ℤ))
have rw : (↑(HDiv.hDiv (α := ℕ) (↑n.pred' : ℕ) (↑(Num.pos d) : ℕ) + 1) : ℤ) =
  -HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1 / -HAdd.hAdd (α := ℤ) (↑(↑d.pred' : ℕ) : ℤ) 1
Tactic: rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
        Num.div_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
⊢ Eq (α := ℤ) (↑(HDiv.hDiv (α := ℕ) (↑n.pred' : ℕ) (↑d : ℕ)).succ : ℤ)
    (↑((↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1).succ : ℤ)
have rw : Eq (α := ℤ) (↑((↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1).succ : ℤ)
  (↑((↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1).succ : ℤ)
Tactic: rw [d.to_nat_eq_succ_pred]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : PosNum
d : ZNum
⊢ (↑(Num.pos n % d.abs) : ℤ) = HMod.hMod (α := ℤ) (↑(pos n) : ℤ) (↑d : ℤ)
have rw : (↑((↑(Num.pos n) : ℕ) % natAbs (↑d : ℤ)) : ℤ) = HMod.hMod (α := ℤ) (↑(↑n : ℕ) : ℤ) (↑d : ℤ)
Tactic: rw [← Num.to_nat_to_int, cast_pos, Num.mod_to_nat, ← PosNum.to_nat_to_int, abs_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : PosNum
d : ZNum
⊢ HSub.hSub (α := ℤ) (↑d.abs : ℤ) (↑(n.pred' % d.abs).succ : ℤ) = HMod.hMod (α := ℤ) (↑(neg n) : ℤ) (↑d : ℤ)
have rw : subNatNat (natAbs (↑d : ℤ)) ((↑n.pred' : ℕ) % natAbs (↑d : ℤ) + 1) =
  -HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1 % (↑d : ℤ)
Tactic: rw [← Num.to_nat_to_int, cast_neg, ← Num.to_nat_to_int, Num.succ_to_nat, Num.mod_to_nat,
          abs_to_nat, ← Int.subNatNat_eq_coe, n.to_int_eq_succ_pred]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : ZNum
⊢ Nat.gcd (↑a.abs : ℕ) (↑b.abs : ℕ) = Int.gcd (↑a : ℤ) (↑b : ℤ)
have simp : (natAbs (↑a : ℤ)).gcd (natAbs (↑b : ℤ)) = Int.gcd (↑a : ℤ) (↑b : ℤ)
Tactic: simp only [abs_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m n : ZNum
⊢ m ∣ n ↔ n % m = 0
have rw : HMod.hMod (α := ℤ) (↑n : ℤ) (↑m : ℤ) = 0 ↔ HMod.hMod (α := ℤ) (↑n : ℤ) (↑m : ℤ) = (↑0 : ℤ)
Tactic: rw [← dvd_to_int, Int.dvd_iff_emod_eq_zero, ← to_int_inj, mod_to_int]
-- Lean 4 proof step from Mathlib.Data.Opposite (goal)
Goal:
α : Sort u
X : Type v
inst : Small.{u, v} X
⊢ Small.{u, v} Xᵒᵖ
have obtain : ∀ (S : Type u) (e : X ≃ S), Small.{u, v} Xᵒᵖ
Tactic: obtain ⟨S, ⟨e⟩⟩ := Small.equiv_small (α := X)
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
⊢ Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))
have rw : Option.map (g₁ ∘ f₁) (some a) = Option.map g₂ (Option.map f₂ (some a))
Tactic: rw [map_map, h, ← map_map]
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
rw : Option.map (g₁ ∘ f₁) (some a) = Option.map g₂ (Option.map f₂ (some a))
⊢ Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))
have rw₁ : Option.map (g₂ ∘ f₂) (some a) = Option.map g₂ (Option.map f₂ (some a))
Tactic: rw [map_map, h, ← map_map]
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
rw : Option.map (g₁ ∘ f₁) (some a) = Option.map g₂ (Option.map f₂ (some a))
rw₁ : Option.map (g₂ ∘ f₂) (some a) = Option.map g₂ (Option.map f₂ (some a))
⊢ Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))
have rw₂ : Option.map g₂ (Option.map f₂ (some a)) = Option.map g₂ (Option.map f₂ (some a))
Tactic: rw [map_map, h, ← map_map]
-- Lean 4 proof step from Mathlib.Data.Option.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha : a ∈ x
⊢ f a ⋯ ∈ pmap (p := p) f x h
have ha₁ : x = some a
Tactic: rw [mem_def] at ha ⊢
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha_1 : a ∈ x
ha : x = some a
⊢ pmap (p := p) f x h = some (f a ⋯)
have subst : ∀ (h : ∀ (a_1 : α), a_1 ∈ some a → p a_1) (ha : a ∈ some a), pmap (p := p) f (some a) h = some (f a sorry)
Tactic: subst ha
Cleared hypotheses: x, h, ha_1, ha
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
inst : Inhabited α
o : Option α
⊢ o.getD default = o.iget
have none : Eq.{u_1 + 1} (α := α) (getD none default) (iget none)
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
inst : Inhabited α
o : Option α
none : Eq.{u_1 + 1} (α := α) (getD Option.none default) (iget Option.none)
⊢ o.getD default = o.iget
have some : ∀ (val : α), (some val).getD default = (some val).iget
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
o : Option α
⊢ o.casesOn' (f none) (f ∘ fun (a : α) ↦ some a) = f o
have none : casesOn' (α := α) none (f none) (f ∘ fun (a : α) ↦ some a) = f none
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
o : Option α
none : casesOn' (α := α) Option.none (f Option.none) (f ∘ fun (a : α) ↦ some a) = f Option.none
⊢ o.casesOn' (f Option.none) (f ∘ fun (a : α) ↦ some a) = f o
have some : ∀ (val : α), (some val).casesOn' (f Option.none) (f ∘ fun (a : α) ↦ some a) = f (some val)
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
b : β
f : α → β
a : Option α
⊢ a.casesOn' b f = a.elim b f
have none : casesOn' none b f = Option.elim none b f
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
b : β
f : α → β
a : Option α
none : casesOn' Option.none b f = Option.elim Option.none b f
⊢ a.casesOn' b f = a.elim b f
have some : ∀ (val : α), (some val).casesOn' b f = (some val).elim b f
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
i : Option α
⊢ i.elim (f none) (f ∘ some) = f i
have none : Option.elim none (f none) (f ∘ some) = f none
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
i : Option α
none : Option.elim Option.none (f Option.none) (f ∘ some) = f Option.none
⊢ i.elim (f Option.none) (f ∘ some) = f i
have some : ∀ (val : α), (some val).elim (f Option.none) (f ∘ some) = f (some val)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
i : Option γ
⊢ (i.elim (h x) fun (j : γ) ↦ h (f j)) = h (i.elim x f)
have none : (Option.elim none (h x) fun (j : γ) ↦ h (f j)) = h (Option.elim none x f)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
i : Option γ
none : (Option.elim Option.none (h x) fun (j : γ) ↦ h (f j)) = h (Option.elim Option.none x f)
⊢ (i.elim (h x) fun (j : γ) ↦ h (f j)) = h (i.elim x f)
have some : ∀ (val : γ), ((some val).elim (h x) fun (j : γ) ↦ h (f j)) = h ((some val).elim x f)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
i : Option γ
⊢ (i.elim (h x y) fun (j : γ) ↦ h (f j) (g j)) = h (i.elim x f) (i.elim y g)
have none : (Option.elim none (h x y) fun (j : γ) ↦ h (f j) (g j)) = h (Option.elim none x f) (Option.elim none y g)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
i : Option γ
none :
  (Option.elim Option.none (h x y) fun (j : γ) ↦ h (f j) (g j)) =
    h (Option.elim Option.none x f) (Option.elim Option.none y g)
⊢ (i.elim (h x y) fun (j : γ) ↦ h (f j) (g j)) = h (i.elim x f) (i.elim y g)
have some : ∀ (val : γ), ((some val).elim (h x y) fun (j : γ) ↦ h (f j) (g j)) = h ((some val).elim x f) ((some val).elim y g)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : γ → α → β
x : α → β
i : Option γ
y : α
⊢ i.elim x f y = i.elim (x y) fun (j : γ) ↦ f j y
have rw : i.elim x f y = i.elim x f y
Tactic: rw [elim_comp fun f : α → β => f y]
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
d : α
⊢ Eq.{u_1 + 1} (α := α → α) ((fun (x : Option α) ↦ x.getD d) ∘ some) id
have h : ∀ (x : α), ((fun (x : Option α) ↦ x.getD d) ∘ some) x = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : Option α
f : α → β
⊢ none = Option.map f x ↔ x = none
have rw : Option.map f x = none ↔ x = none
Tactic: rw [eq_comm, map_eq_none_iff]
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : Option α
f : α → β
rw : Option.map f x = none ↔ x = none
⊢ none = Option.map f x ↔ x = none
have rw₁ : x = none ↔ x = none
Tactic: rw [eq_comm, map_eq_none_iff]
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
b : β
x : Option α
f : α → β
⊢ some b = Option.map f x ↔ ∃ (a : α), x = some a ∧ f a = b
have rw : Option.map f x = some b ↔ ∃ (a : α), x = some a ∧ f a = b
Tactic: rw [eq_comm, map_eq_some_iff]
-- Lean 4 proof step from Mathlib.Data.Option.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
b : β
x : Option α
f : α → β
rw : Option.map f x = some b ↔ ∃ (a : α), x = some a ∧ f a = b
⊢ some b = Option.map f x ↔ ∃ (a : α), x = some a ∧ f a = b
have rw₁ : (∃ (a : α), x = some a ∧ f a = b) ↔ ∃ (a : α), x = some a ∧ f a = b
Tactic: rw [eq_comm, map_eq_some_iff]
-- Lean 4 proof step from Mathlib.Data.Option.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
o : Option α
⊢ Option.elim' (f none) (f ∘ some) o = f o
have none : Option.elim' (f none) (f ∘ some) none = f none
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Option.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
o : Option α
none : Option.elim' (f Option.none) (f ∘ some) Option.none = f Option.none
⊢ Option.elim' (f Option.none) (f ∘ some) o = f o
have some : ∀ (val : α), Option.elim' (f Option.none) (f ∘ some) (some val) = f (some val)
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Option.Defs (goal)
Goal:
α : Type u_3
β : Type u_4
b : β
f : α → β
a : Option α
⊢ Option.elim' b f a = a.elim b f
have none : Option.elim' b f none = Option.elim none b f
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Option.Defs (goal)
Goal:
α : Type u_3
β : Type u_4
b : β
f : α → β
a : Option α
none : Option.elim' b f Option.none = Option.elim Option.none b f
⊢ Option.elim' b f a = a.elim b f
have some : ∀ (val : α), Option.elim' b f (some val) = (some val).elim b f
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Option.NAry (goal)
Goal:
α β γ : Type u
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = f <$> a <*> b
have none : map₂ f none b = f <$> none <*> b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Option.NAry (goal)
Goal:
α β γ : Type u
f : α → β → γ
a : Option α
b : Option β
none : map₂ f Option.none b = f <$> Option.none <*> b
⊢ map₂ f a b = f <$> a <*> b
have some : ∀ (val : α), map₂ f (some val) b = f <$> some val <*> b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Option.NAry (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
⊢ map₂ f a none = none
have none : map₂ f none none = none
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Option.NAry (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
none : map₂ f Option.none Option.none = Option.none
⊢ map₂ f a Option.none = Option.none
have some : ∀ (val : α), map₂ f (some val) Option.none = Option.none
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Ordering.Lemmas (goal)
Goal:
c : Prop
inst : Decidable c
a b : Ordering
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
have pos : c → ((if c then a else b) = lt) = if c then a = lt else b = lt
Tactic: by_cases c
-- Lean 4 proof step from Mathlib.Data.Ordering.Lemmas (goal)
Goal:
c : Prop
inst : Decidable c
a b : Ordering
pos : c → ((if c then a else b) = lt) = if c then a = lt else b = lt
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
have neg : ¬c → ((if c then a else b) = lt) = if c then a = lt else b = lt
Tactic: by_cases c
-- Lean 4 proof step from Mathlib.Data.Ordering.Lemmas (goal)
Goal:
c : Prop
inst : Decidable c
a b : Ordering
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
have pos : c → ((if c then a else b) = eq) = if c then a = eq else b = eq
Tactic: by_cases c
-- Lean 4 proof step from Mathlib.Data.Ordering.Lemmas (goal)
Goal:
c : Prop
inst : Decidable c
a b : Ordering
pos : c → ((if c then a else b) = eq) = if c then a = eq else b = eq
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
have neg : ¬c → ((if c then a else b) = eq) = if c then a = eq else b = eq
Tactic: by_cases c
-- Lean 4 proof step from Mathlib.Data.Ordering.Lemmas (goal)
Goal:
c : Prop
inst : Decidable c
a b : Ordering
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
have pos : c → ((if c then a else b) = gt) = if c then a = gt else b = gt
Tactic: by_cases c
-- Lean 4 proof step from Mathlib.Data.Ordering.Lemmas (goal)
Goal:
c : Prop
inst : Decidable c
a b : Ordering
pos : c → ((if c then a else b) = gt) = if c then a = gt else b = gt
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
have neg : ¬c → ((if c then a else b) = gt) = if c then a = gt else b = gt
Tactic: by_cases c
-- Lean 4 proof step from Mathlib.Data.Ordering.Lemmas (goal)
Goal:
o₁ o₂ : Ordering
⊢ (o₁.dthen fun (x : o₁ = eq) ↦ o₂) = o₁.then o₂
have lt : (lt.dthen fun (x : lt = eq) ↦ o₂) = lt.then o₂
Tactic: cases o₁
Cleared hypotheses: o₁
-- Lean 4 proof step from Mathlib.Data.Ordering.Lemmas (goal)
Goal:
o₁ o₂ : Ordering
lt : (Ordering.lt.dthen fun (x : Ordering.lt = eq) ↦ o₂) = Ordering.lt.then o₂
⊢ (o₁.dthen fun (x : o₁ = eq) ↦ o₂) = o₁.then o₂
have eq : (eq.dthen fun (x : eq = eq) ↦ o₂) = eq.then o₂
Tactic: cases o₁
Cleared hypotheses: o₁
-- Lean 4 proof step from Mathlib.Data.Ordering.Lemmas (goal)
Goal:
o₁ o₂ : Ordering
lt : (Ordering.lt.dthen fun (x : Ordering.lt = Ordering.eq) ↦ o₂) = Ordering.lt.then o₂
eq : (Ordering.eq.dthen fun (x : Ordering.eq = Ordering.eq) ↦ o₂) = Ordering.eq.then o₂
⊢ (o₁.dthen fun (x : o₁ = Ordering.eq) ↦ o₂) = o₁.then o₂
have gt : (gt.dthen fun (x : gt = Ordering.eq) ↦ o₂) = gt.then o₂
Tactic: cases o₁
Cleared hypotheses: o₁
-- Lean 4 proof step from Mathlib.Data.Ordering.Lemmas (goal)
Goal:
α : Type u
lt : α → α → Prop
inst : DecidableRel lt
inst_1 : IsStrictOrder α lt
a b : α
⊢ cmpUsing lt a b = Ordering.gt ↔ lt b a
have simp : lt b a → ¬lt a b
Tactic: simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right, and_true, if_false_left,
    and_iff_right_iff_imp, reduceCtorEq]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ node s l x r = l.node' x r
have rw : node (l.size + r.size + 1) l x r = l.node' x r
Tactic: rw [h.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
t_ih_l : ∀ (hl : l.Sized), C l
t_ih_r : ∀ (hl : r.Sized), C r
hl : (node size l x r).Sized
⊢ C (node size l x r)
have node : C (l.node' x r)
Tactic: rw [hl.eq_node']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
hl : t.Sized
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
⊢ C t
have nil : ∀ (hl : Sized.{u_1} (α := α) nil), C nil
Tactic: induction t with
  | nil => exact H0
  | node _ _ _ _ t_ih_l t_ih_r =>
    rw [hl.eq_node']
    exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)
Cleared hypotheses: t, hl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
hl : t.Sized
C : Ordnode α → Prop
H0 : C Ordnode.nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
nil : ∀ (hl : Sized.{u_1} (α := α) Ordnode.nil), C Ordnode.nil
⊢ C t
have node : ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (t_ih_l : ∀ (hl : l.Sized), C l) (t_ih_r : ∀ (hl : r.Sized), C r)
  (hl : (node size l x r).Sized), C (node size l x r)
Tactic: induction t with
  | nil => exact H0
  | node _ _ _ _ t_ih_l t_ih_r =>
    rw [hl.eq_node']
    exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)
Cleared hypotheses: t, hl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ (node s l x r).size = (node s l x r).realSize
have rw : l.realSize + r.realSize + 1 = (node (l.realSize + r.realSize + 1) l x r).realSize
Tactic: rw [size, h₁, size_eq_realSize h₂, size_eq_realSize h₃]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
ht : t.Sized
⊢ t.size = 0 ↔ t = nil
have nil : ∀ (ht : Sized.{u_1} (α := α) nil), size.{u_1} (α := α) nil = 0 ↔ Eq.{u_1 + 1} (α := Ordnode α) nil nil
Tactic: cases t
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
ht : t.Sized
nil :
  ∀ (ht : Sized.{u_1} (α := α) Ordnode.nil),
    size.{u_1} (α := α) Ordnode.nil = 0 ↔ Eq.{u_1 + 1} (α := Ordnode α) Ordnode.nil Ordnode.nil
⊢ t.size = 0 ↔ t = Ordnode.nil
have node : ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (ht : (node size l x r).Sized),
  (node size l x r).size = 0 ↔ node size l x r = Ordnode.nil
Tactic: cases t
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
ht : t.Sized
⊢ t.size = 0 ↔ t = nil
have nil : ∀ (ht : Sized.{u_1} (α := α) nil), size.{u_1} (α := α) nil = 0 ↔ Eq.{u_1 + 1} (α := Ordnode α) nil nil
Tactic: cases t <;> [simp; simp [ht.1]]
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
ht : t.Sized
nil :
  ∀ (ht : Sized.{u_1} (α := α) Ordnode.nil),
    size.{u_1} (α := α) Ordnode.nil = 0 ↔ Eq.{u_1 + 1} (α := Ordnode α) Ordnode.nil Ordnode.nil
⊢ t.size = 0 ↔ t = Ordnode.nil
have node : ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (ht : (node size l x r).Sized),
  (node size l x r).size = 0 ↔ node size l x r = Ordnode.nil
Tactic: cases t <;> [simp; simp [ht.1]]
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ 0 < s
have rw : 0 < l.size + r.size + 1
Tactic: rw [h.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ (node s l x r).dual.dual = node s l x r
have rw : (node s r.dual x l.dual).dual = node s l x r
Tactic: rw [dual, dual, dual_dual l, dual_dual r]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
rw : (node s r.dual x l.dual).dual = node s l x r
⊢ (node s l x r).dual.dual = node s l x r
have rw₁ : node s l.dual.dual x r.dual.dual = node s l x r
Tactic: rw [dual, dual, dual_dual l, dual_dual r]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
rw : (node s r.dual x l.dual).dual = node s l x r
rw₁ : node s l.dual.dual x r.dual.dual = node s l x r
⊢ (node s l x r).dual.dual = node s l x r
have rw₂ : node s l x r.dual.dual = node s l x r
Tactic: rw [dual, dual, dual_dual l, dual_dual r]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
rw : (node s r.dual x l.dual).dual = node s l x r
rw₁ : node s l.dual.dual x r.dual.dual = node s l x r
rw₂ : node s l x r.dual.dual = node s l x r
⊢ (node s l x r).dual.dual = node s l x r
have rw₃ : node s l x r = node s l x r
Tactic: rw [dual, dual, dual_dual l, dual_dual r]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
⊢ t.dual.size = t.size
have nil : size.{u_1} (α := α) (dual nil) = size.{u_1} (α := α) nil
Tactic: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
nil : size.{u_1} (α := α) (dual Ordnode.nil) = size.{u_1} (α := α) Ordnode.nil
⊢ t.dual.size = t.size
have node : ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α), (node size l x r).dual.size = (node size l x r).size
Tactic: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
l r : ℕ
⊢ l + r ≤ 1 → r + l ≤ 1
have rw : r + l ≤ 1 → r + l ≤ 1
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
⊢ BalancedSz l r₂
have refine : ∀ (h : ¬l + r₂ ≤ 1), l ≤ delta * r₂ ∧ r₂ ≤ delta * l
Tactic: refine or_iff_not_imp_left.2 fun h => ?_
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂ ∧ r₂ ≤ delta * l
have refine : l ≤ delta * r₂
Tactic: refine ⟨?_, h₂.resolve_left h⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l + r₁ ≤ 1
⊢ l ≤ delta * r₂
have inl : ∀ (h₁ : r₁ ≤ 0) (h₂ : l + 0 ≤ 1 ∨ 0 ≤ delta * l) (h : ¬l + 0 ≤ 1), l ≤ delta * 0
Tactic: cases r₂
Cleared hypotheses: r₂, h₁, h₂, h