awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
have z_card : #(Icc x z) < #(Icc x y)
Tactic: have z_card := calc
      #(Icc x z) ≤ #(Ico x y) := card_le_card <| Icc_subset_Ico_right hz.1.2
      _          < #(Icc x y) := this
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Icc x z) < #(Icc x y)
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
have h₁ : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x z
Tactic: have h₁ := transGen_wcovBy_of_le hz.1.1
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Icc x z) < #(Icc x y)
h₁ : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x z
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
have h₂ : z ⩿ y
Tactic: have h₂ : z ⩿ y :=
      ⟨hz.1.2.le, fun c hzc hcy ↦ hzc.not_ge <| hz.2 ⟨hz.1.1.trans hzc.le, hcy⟩ hzc.le⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
⊢ x ≤ y ↔ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
have refine : ∀ (h : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y), x ≤ y
Tactic: refine ⟨transGen_wcovBy_of_le, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
h : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
⊢ x ≤ y
have single : ∀ {b : α} (h : x ⩿ b), x ≤ b
Tactic: induction h with
  | single h => exact h.le
  | tail _ h₁ h₂ => exact h₂.trans h₁.le
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
h : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
single : ∀ {b : α} (h : x ⩿ b), x ≤ b
⊢ x ≤ y
have tail : ∀ {b c : α}, TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x b → ∀ (h₁ : b ⩿ c) (h₂ : x ≤ b), x ≤ c
Tactic: induction h with
  | single h => exact h.le
  | tail _ h₁ h₂ => exact h₂.trans h₁.le
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
x y : α
⊢ x ≤ y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have rw : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
Tactic: rw [le_iff_transGen_wcovBy, wcovBy_eq_reflGen_covBy, transGen_reflGen]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
x y : α
rw : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
⊢ x ≤ y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have rw₁ : TransGen (ReflGen fun (x1 x2 : α) ↦ x1 ⋖ x2) x y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
Tactic: rw [le_iff_transGen_wcovBy, wcovBy_eq_reflGen_covBy, transGen_reflGen]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
x y : α
rw : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
rw₁ : TransGen (ReflGen fun (x1 x2 : α) ↦ x1 ⋖ x2) x y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
⊢ x ≤ y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have rw₂ : ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
Tactic: rw [le_iff_transGen_wcovBy, wcovBy_eq_reflGen_covBy, transGen_reflGen]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have obtain : ∀ (z : α) (hxz : x ≤ z) (hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z), TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
Tactic: obtain ⟨z, hxz, hz⟩ := (Set.finite_Ico x y).exists_le_maximal <| Set.left_mem_Ico.2 hxy
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have z_card : #(Ico x z) < #(Ico x y)
Tactic: have z_card : #(Ico x z) < #(Ico x y) := card_lt_card <| ssubset_iff_of_subset
    (Ico_subset_Ico_right hz.1.2.le) |>.mpr ⟨z, mem_Ico.2 hz.1, right_notMem_Ico⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have hzy : z ⋖ y
Tactic: have hzy : z ⋖ y :=
    ⟨hz.1.2, fun c hc hcy ↦ hc.not_ge <| hz.2 (⟨(hz.1.1.trans_lt hc).le, hcy⟩) hc.le⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have pos : ∀ (hxz : x < z), TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
Tactic: by_cases hxz : x < z
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
pos : ∀ (hxz : x < z), TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have neg : ∀ (hxz : ¬x < z), TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
Tactic: by_cases hxz : x < z
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz_1 : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : ¬x < z
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have hxz₁ : x ≤ z → z ≤ x
Tactic: simp only [lt_iff_le_not_ge, not_and, not_not] at hxz
Cleared hypotheses: hxz
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
⊢ x < y ↔ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have refine : ∀ (h : TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y), x < y
Tactic: refine ⟨transGen_covBy_of_lt, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
h : TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
⊢ x < y
have single : ∀ {b : α} (hx : x ⋖ b), x < b
Tactic: induction h with
  | single hx => exact hx.1
  | tail _ hb ih => exact ih.trans hb.1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
h : TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
single : ∀ {b : α} (hx : x ⋖ b), x < b
⊢ x < y
have tail : ∀ {b c : α}, TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x b → ∀ (hb : b ⋖ c) (ih : x < b), x < c
Tactic: induction h with
  | single hx => exact hx.1
  | tail _ hb ih => exact ih.trans hb.1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ (a b : α), a ⩿ b → f a ≤ f b
have refine : ∀ (h : ∀ (a b : α), a ⩿ b → f a ≤ f b) (a b : α) (hab : a ≤ b), f a ≤ f b
Tactic: refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b
have refine : ∀ (h : ∀ (a b : α), a ⋖ b → f a ≤ f b) (a b : α) (hab : a ≤ b), f a ≤ f b
Tactic: refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
⊢ StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b
have refine : ∀ (h : ∀ (a b : α), a ⋖ b → f a < f b) (a b : α) (hab : a < b), f a < f b
Tactic: refine ⟨fun hf _ _ h ↦ hf h.lt, fun h a b hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
⊢ f a < f b
have this : ∀ (hab : TransGen CovBy a b), TransGen LT.lt (f a) (f b)
Tactic: have := Relation.TransGen.lift f h (a := a) (b := b)
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : ∀ (hab : TransGen CovBy a b), TransGen LT.lt (f a) (f b)
⊢ f a < f b
have this₁ : ∀ (hab : a < b), f a < f b
Tactic: rw [← lt_iff_transGen_covBy, transGen_eq_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
⊢ LE.le.{u_1} (α := Finset α) ((fun (n : ℕ) ↦ (Icc (-(↑n : α)) (↑n : α) : Finset α)) m)
    ((fun (n : ℕ) ↦ (Icc (-(↑n : α)) (↑n : α) : Finset α)) n)
have ha : LE.le.{u_1} (α := α) (-(↑n : α)) (-(↑m : α))
Tactic: apply Icc_subset_Icc
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
ha : LE.le.{u_1} (α := α) (-(↑n : α)) (-(↑m : α))
⊢ LE.le.{u_1} (α := Finset α) ((fun (n : ℕ) ↦ (Icc (-(↑n : α)) (↑n : α) : Finset α)) m)
    ((fun (n : ℕ) ↦ (Icc (-(↑n : α)) (↑n : α) : Finset α)) n)
have hb : LE.le.{u_1} (α := α) (↑m : α) (↑n : α)
Tactic: apply Icc_subset_Icc
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Finset α) (box (n + 1)) (Icc (-(↑n.succ : α)) (↑n.succ : α) \ Icc (-(↑n : α)) (↑n : α))
have rw : Eq.{u_1 + 1} (α := Finset α) (Icc (-(↑(n + 1) : α)) (↑(n + 1) : α) \ Icc (-(↑n : α)) (↑n : α))
  (Icc (-(↑n.succ : α)) (↑n.succ : α) \ Icc (-(↑n : α)) (↑n : α))
Tactic: rw [box, Icc_neg_mono.disjointed_add_one]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
⊢ Disjoint.{u_1} (α := Finset α) (box (n + 1)) (Icc (-(↑n : α)) (↑n : α))
have rw : Disjoint.{u_1} (α := Finset α) (Icc (-(↑n.succ : α)) (↑n.succ : α) \ Icc (-(↑n : α)) (↑n : α))
  (Icc (-(↑n : α)) (↑n : α))
Tactic: rw [box_succ_eq_sdiff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Finset α) (disjUnion (box (n + 1)) (Icc (-(↑n : α)) (↑n : α)) ⋯)
    (Icc (-(↑n.succ : α)) (↑n.succ : α))
have rw : Eq.{u_1 + 1} (α := Finset α) (box (n + 1) ∪ Icc (-(↑n : α)) (↑n : α)) (Icc (-(↑n.succ : α)) (↑n.succ : α))
Tactic: rw [disjUnion_eq_union, box_succ_union_prod]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
rw : Eq.{u_1 + 1} (α := Finset α) (box (n + 1) ∪ Icc (-(↑n : α)) (↑n : α)) (Icc (-(↑n.succ : α)) (↑n.succ : α))
⊢ Eq.{u_1 + 1} (α := Finset α) (disjUnion (box (n + 1)) (Icc (-(↑n : α)) (↑n : α)) ⋯)
    (Icc (-(↑n.succ : α)) (↑n.succ : α))
have rw₁ : Eq.{u_1 + 1} (α := Finset α) (Icc (-(↑n.succ : α)) (↑n.succ : α)) (Icc (-(↑n.succ : α)) (↑n.succ : α))
Tactic: rw [disjUnion_eq_union, box_succ_union_prod]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
n : ℕ
inst_4 : DecidableEq α
⊢ Membership.mem (γ := Finset α) (box n) 0 ↔ n = 0
have zero : Membership.mem (γ := Finset α) (box 0) 0 ↔ Eq (α := ℕ) 0 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
n : ℕ
inst_4 : DecidableEq α
zero : Membership.mem (γ := Finset α) (box 0) 0 ↔ Eq (α := ℕ) 0 0
⊢ Membership.mem (γ := Finset α) (box n) 0 ↔ n = 0
have succ : ∀ (n : ℕ), Membership.mem (γ := Finset α) (box (n + 1)) 0 ↔ n + 1 = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
n : ℕ
inst_4 : DecidableEq α
x : α
hx : Membership.mem (γ := Finset α) (box n) x
hn : n = 0
⊢ x = 0
have rwa : ∀ (hx : Membership.mem (γ := Finset α) (box 0) x) (hn : n = 0), x = 0
Tactic: rwa [hn, box_zero, mem_singleton] at hx
Cleared hypotheses: hx, hn
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
n : ℕ
inst_4 : DecidableEq α
x : α
hx : Membership.mem (γ := Finset α) (box n) x
hn : n = 0
rwa : ∀ (hx : Membership.mem (γ := Finset α) (box 0) x) (hn : n = 0), x = 0
⊢ x = 0
have rwa₁ : ∀ (hx : Membership.mem (γ := Finset α) {0} x) (hn : n = 0), x = 0
Tactic: rwa [hn, box_zero, mem_singleton] at hx
Cleared hypotheses: hx, hn
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
n : ℕ
inst_4 : DecidableEq α
x : α
hx : Membership.mem (γ := Finset α) (box n) x
hn : n = 0
rwa : ∀ (hx : Membership.mem (γ := Finset α) (box 0) x) (hn : n = 0), x = 0
rwa₁ : ∀ (hx : Membership.mem (γ := Finset α) {0} x) (hn : n = 0), x = 0
⊢ x = 0
have rwa₂ : ∀ (hx : x = 0) (hn : n = 0), x = 0
Tactic: rwa [hn, box_zero, mem_singleton] at hx
Cleared hypotheses: hx, hn
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : Ring β
inst_4 : PartialOrder β
inst_5 : IsOrderedRing β
inst_6 : LocallyFiniteOrder α
inst_7 : LocallyFiniteOrder β
inst_8 : DecidableEq α
inst_9 : DecidableEq β
inst_10 : DecidableLE (α × β)
n : ℕ
⊢ card (α := α × β) (box (n + 1)) =
    card.{u_1} (α := α) (Icc (-(↑n.succ : α)) (↑n.succ : α)) *
        card.{u_2} (α := β) (Icc (-(↑n.succ : β)) (↑n.succ : β)) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
have rw : card.{u_1} (α := α) (Icc (-(↑n.succ : α × β)).1 (↑n.succ : α × β).1) *
      card.{u_2} (α := β) (Icc (-(↑n.succ : α × β)).2 (↑n.succ : α × β).2) -
    card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
      card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
  card.{u_1} (α := α) (Icc (-(↑n.succ : α)) (↑n.succ : α)) * card.{u_2} (α := β) (Icc (-(↑n.succ : β)) (↑n.succ : β)) -
    card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
Tactic: rw [box_succ_eq_sdiff, card_sdiff_of_subset (Icc_neg_mono n.le_succ), Finset.card_Icc_prod,
    Finset.card_Icc_prod]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : Ring β
inst_4 : PartialOrder β
inst_5 : IsOrderedRing β
inst_6 : LocallyFiniteOrder α
inst_7 : LocallyFiniteOrder β
inst_8 : DecidableEq α
inst_9 : DecidableEq β
inst_10 : DecidableLE (α × β)
n : ℕ
simp_rw :
  card.{u_1} (α := α) (Icc (-(↑(n + 1) : α × β)).1 (↑(n + 1) : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑(n + 1) : α × β)).2 (↑(n + 1) : α × β).2) -
      card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
    card.{u_1} (α := α) (Icc (-(↑(n + 1) : α)) (↑(n + 1) : α)) *
        card.{u_2} (α := β) (Icc (-(↑(n + 1) : β)) (↑(n + 1) : β)) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
⊢ card.{u_1} (α := α) (Icc (-(↑n.succ : α × β)).1 (↑n.succ : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n.succ : α × β)).2 (↑n.succ : α × β).2) -
      card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
    card.{u_1} (α := α) (Icc (-(↑n.succ : α)) (↑n.succ : α)) *
        card.{u_2} (α := β) (Icc (-(↑n.succ : β)) (↑n.succ : β)) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
have simp_rw₁ : #(Icc (-HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).1 (HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).1) *
      #(Icc (-HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).2
          (HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).2) -
    card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
      card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
  #(Icc (-HAdd.hAdd (α := α) (↑n : α) (↑1 : α)) (HAdd.hAdd (α := α) (↑n : α) (↑1 : α))) *
      #(Icc (-HAdd.hAdd (α := β) (↑n : β) (↑1 : β)) (HAdd.hAdd (α := β) (↑n : β) (↑1 : β))) -
    card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
Tactic: simp_rw [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, neg_add_rev, fst_add, fst_neg,
    fst_one, fst_natCast, snd_add, snd_neg, snd_one, snd_natCast]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : Ring β
inst_4 : PartialOrder β
inst_5 : IsOrderedRing β
inst_6 : LocallyFiniteOrder α
inst_7 : LocallyFiniteOrder β
inst_8 : DecidableEq α
inst_9 : DecidableEq β
inst_10 : DecidableLE (α × β)
n : ℕ
simp_rw :
  card.{u_1} (α := α) (Icc (-(↑(n + 1) : α × β)).1 (↑(n + 1) : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑(n + 1) : α × β)).2 (↑(n + 1) : α × β).2) -
      card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
    card.{u_1} (α := α) (Icc (-(↑(n + 1) : α)) (↑(n + 1) : α)) *
        card.{u_2} (α := β) (Icc (-(↑(n + 1) : β)) (↑(n + 1) : β)) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
simp_rw₁ :
  #(Icc (-HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).1 (HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).1) *
        #(Icc (-HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).2
            (HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).2) -
      card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
    #(Icc (-HAdd.hAdd (α := α) (↑n : α) (↑1 : α)) (HAdd.hAdd (α := α) (↑n : α) (↑1 : α))) *
        #(Icc (-HAdd.hAdd (α := β) (↑n : β) (↑1 : β)) (HAdd.hAdd (α := β) (↑n : β) (↑1 : β))) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
⊢ card.{u_1} (α := α) (Icc (-(↑n.succ : α × β)).1 (↑n.succ : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n.succ : α × β)).2 (↑n.succ : α × β).2) -
      card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
    card.{u_1} (α := α) (Icc (-(↑n.succ : α)) (↑n.succ : α)) *
        card.{u_2} (α := β) (Icc (-(↑n.succ : β)) (↑n.succ : β)) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
have simp_rw₂ : #(Icc (-HAdd.hAdd (α := α × β) (↑n : α × β) 1).1 (HAdd.hAdd (α := α × β) (↑n : α × β) 1).1) *
      #(Icc (-HAdd.hAdd (α := α × β) (↑n : α × β) 1).2 (HAdd.hAdd (α := α × β) (↑n : α × β) 1).2) -
    card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
      card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
  #(Icc (-HAdd.hAdd (α := α) (↑n : α) 1) (HAdd.hAdd (α := α) (↑n : α) 1)) *
      #(Icc (-HAdd.hAdd (α := β) (↑n : β) 1) (HAdd.hAdd (α := β) (↑n : β) 1)) -
    card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
Tactic: simp_rw [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, neg_add_rev, fst_add, fst_neg,
    fst_one, fst_natCast, snd_add, snd_neg, snd_one, snd_natCast]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
n : ℕ
h : n + 1 ≠ 0
⊢ card (α := ℤ × ℤ) (box (n + 1)) = 8 * (n + 1)
have simp_rw : (HAdd.hAdd (α := ℤ) (↑n.succ : ℤ) 1 + (↑n.succ : ℤ)).toNat *
      (HAdd.hAdd (α := ℤ) (↑n.succ : ℤ) 1 + (↑n.succ : ℤ)).toNat -
    (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + (↑n : ℤ)).toNat * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + (↑n : ℤ)).toNat =
  8 * (n + 1)
Tactic: simp_rw [Prod.card_box_succ, card_Icc, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
n : ℕ
h : n + 1 ≠ 0
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) - (n + 1 + n) * (n + 1 + n) = 8 * (n + 1)
have refine : (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) = 8 * (n + 1) + (n + 1 + n) * (n + 1 + n)
Tactic: refine tsub_eq_of_eq_add ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
n : ℕ
h : n + 1 ≠ 0
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) = 8 * (n + 1) + (n + 1 + n) * (n + 1 + n)
have zify : (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) *
    (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
  8 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 +
    (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + (↑n : ℤ)) * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + (↑n : ℤ))
Tactic: zify
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
x : ℤ × ℤ
n : ℕ
⊢ Membership.mem (γ := Finset (ℤ × ℤ)) (box (n + 1)) x ↔ max x.1.natAbs x.2.natAbs = n + 1
have simp : ((-1 ≤ x.1 + (↑n : ℤ) ∧ -1 ≤ x.2 + (↑n : ℤ)) ∧
      x.1 ≤ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ∧ x.2 ≤ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ∧
    (-(↑n : ℤ) ≤ x.1 → -(↑n : ℤ) ≤ x.2 → x.1 ≤ (↑n : ℤ) → (↑n : ℤ) < x.2) ↔
  max x.1.natAbs x.2.natAbs = n + 1
Tactic: simp [box_succ_eq_sdiff, Prod.le_def]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
x : ℤ × ℤ
⊢ ∃! n : ℕ, Membership.mem (γ := Finset (ℤ × ℤ)) (box n) x
have h : (fun (n : ℕ) ↦ Membership.mem (γ := Finset (ℤ × ℤ)) (box n) x) (max x.1.natAbs x.2.natAbs) ∧
  ∀ (y : ℕ), (fun (n : ℕ) ↦ Membership.mem (γ := Finset (ℤ × ℤ)) (box n) x) y → y = max x.1.natAbs x.2.natAbs
Tactic: use max x.1.natAbs x.2.natAbs
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬b ≤ x} ↔ a ≤ x ∧ x < b
have rw : x ∈ finsetIcc a b ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_not_ge]