awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Prime (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ a :: l₁ ~ b :: l₂
have hl : l₁.prod = ((b :: l₂).erase a).prod
Tactic: have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
⊢ a :: l₁ ~ b :: l₂
have have : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p), a :: l₁ ~ b :: l₂
Tactic: classical
      have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
      have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
      have ha : a ∈ b :: l₂ :=
        mem_list_primes_of_dvd_prod (hl₁ a mem_cons_self) hl₂
          (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
      have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
      have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
      exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
have have₁ have₂ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p), a :: l₁ ~ b :: l₂
⊢ a :: l₁ ~ b :: l₂
have have₃ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p), a :: l₁ ~ b :: l₂
Tactic: classical
      have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
      have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
      have ha : a ∈ b :: l₂ :=
        mem_list_primes_of_dvd_prod (hl₁ a mem_cons_self) hl₂
          (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
      have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
      have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
      exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
have have₁ have₂ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p), a :: l₁ ~ b :: l₂
have₃ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p), a :: l₁ ~ b :: l₂
⊢ a :: l₁ ~ b :: l₂
have have₄ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p) (ha : a ∈ b :: l₂),
  a :: l₁ ~ b :: l₂
Tactic: classical
      have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
      have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
      have ha : a ∈ b :: l₂ :=
        mem_list_primes_of_dvd_prod (hl₁ a mem_cons_self) hl₂
          (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
      have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
      have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
      exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
have have₁ have₂ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p), a :: l₁ ~ b :: l₂
have₃ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p), a :: l₁ ~ b :: l₂
have₄ :
  ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p) (ha : a ∈ b :: l₂),
    a :: l₁ ~ b :: l₂
⊢ a :: l₁ ~ b :: l₂
have have₅ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p) (ha : a ∈ b :: l₂)
  (hb : b :: l₂ ~ a :: (b :: l₂).erase a), a :: l₁ ~ b :: l₂
Tactic: classical
      have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
      have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
      have ha : a ∈ b :: l₂ :=
        mem_list_primes_of_dvd_prod (hl₁ a mem_cons_self) hl₂
          (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
      have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
      have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
      exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
have have₁ have₂ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p), a :: l₁ ~ b :: l₂
have₃ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p), a :: l₁ ~ b :: l₂
have₄ :
  ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p) (ha : a ∈ b :: l₂),
    a :: l₁ ~ b :: l₂
have₅ :
  ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p) (ha : a ∈ b :: l₂)
    (hb : b :: l₂ ~ a :: (b :: l₂).erase a), a :: l₁ ~ b :: l₂
⊢ a :: l₁ ~ b :: l₂
have have₆ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p) (ha : a ∈ b :: l₂)
  (hb : b :: l₂ ~ a :: (b :: l₂).erase a) (hl : l₁.prod = ((b :: l₂).erase a).prod), a :: l₁ ~ b :: l₂
Tactic: classical
      have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
      have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
      have ha : a ∈ b :: l₂ :=
        mem_list_primes_of_dvd_prod (hl₁ a mem_cons_self) hl₂
          (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
      have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
      have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
      exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
-- Lean 4 proof step from Mathlib.Data.List.ProdSigma (goal)
Goal:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ (l₁ ×ˢ l₂).length = l₁.length * l₂.length
have nil : (SProd.sprod (α := List α) [] l₂).length = length.{u_1} (α := α) [] * l₂.length
Tactic: induction l₁ with
  | nil => exact (Nat.zero_mul _).symm
  | cons x l₁ IH =>
    simp only [length, product_cons, length_append, IH, Nat.add_mul, Nat.one_mul, length_map,
      Nat.add_comm]
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.ProdSigma (goal)
Goal:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
nil : (SProd.sprod (α := List α) [] l₂).length = length.{u_1} (α := α) [] * l₂.length
⊢ (l₁ ×ˢ l₂).length = l₁.length * l₂.length
have cons : ∀ (x : α) (l₁ : List α) (IH : (l₁ ×ˢ l₂).length = l₁.length * l₂.length),
  ((x :: l₁) ×ˢ l₂).length = (x :: l₁).length * l₂.length
Tactic: induction l₁ with
  | nil => exact (Nat.zero_mul _).symm
  | cons x l₁ IH =>
    simp only [length, product_cons, length_append, IH, Nat.add_mul, Nat.one_mul, length_map,
      Nat.add_comm]
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ
⊢ IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m < n + 1 - 1 → r m m.succ
have succ : ∀ (hn : IsChain r (range n) ↔ ∀ (m : ℕ), m + 1 < n → r m m.succ),
  IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
Tactic: simp only [range_succ, Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m + 1 < n + 1 → r m m.succ
⊢ IsChain r (range (n + 1) ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ
have succ : ∀ (hn : IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (m + 1)),
  IsChain r (range n ++ [n]) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)
Tactic: simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (m + 1)
⊢ IsChain r (range n ++ [n]) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)
have succ : (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)
Tactic: rw [hn, forall_lt_succ_right]
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (m + 1)
succ : (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)
⊢ IsChain r (range n ++ [n]) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)
have succ₁ : (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1) ↔ (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1)
Tactic: rw [hn, forall_lt_succ_right]
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n) ↔ ∀ (m : ℕ), m + 1 < n → r m m.succ
⊢ IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
have succ : ∀ (hn : IsChain r (range 0) ↔ ∀ (m : ℕ), m + 1 < 0 → r m m.succ),
  IsChain r (range 0 ++ [0]) ↔ ∀ (m : ℕ), m < 0 → r m m.succ
Tactic: cases n with
    | zero => simp
    | succ n =>
      simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n) ↔ ∀ (m : ℕ), m + 1 < n → r m m.succ
succ :
  ∀ (hn : IsChain r (range 0) ↔ ∀ (m : ℕ), m + 1 < 0 → r m m.succ),
    IsChain r (range 0 ++ [0]) ↔ ∀ (m : ℕ), m < 0 → r m m.succ
⊢ IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
have succ₁ : ∀ (n : ℕ) (hn : IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m + 1 < n + 1 → r m m.succ),
  IsChain r (range (n + 1) ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ
Tactic: cases n with
    | zero => simp
    | succ n =>
      simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
⊢ IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ
have zero : IsChain r (range 0) ↔ ∀ (m : ℕ), m < HSub.hSub (α := ℕ) 0 1 → r m m.succ
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    simp only [range_succ, Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt] at hn ⊢
    cases n with
    | zero => simp
    | succ n =>
      simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
zero : IsChain r (range 0) ↔ ∀ (m : ℕ), m < HSub.hSub (α := ℕ) 0 1 → r m m.succ
⊢ IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ
have succ : ∀ (n : ℕ) (hn : IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ),
  IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m < n + 1 - 1 → r m m.succ
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    simp only [range_succ, Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt] at hn ⊢
    cases n with
    | zero => simp
    | succ n =>
      simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
⊢ IsChain r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
have rw : (∀ (m : ℕ), m < n.succ - 1 → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
Tactic: rw [isChain_range, succ_eq_add_one, Nat.add_one_sub_one]
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
rw : (∀ (m : ℕ), m < n.succ - 1 → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
rw₁ : (∀ (m : ℕ), m < n + 1 - 1 → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
⊢ IsChain r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
have rw₂ : (∀ (m : ℕ), m < n → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
Tactic: rw [isChain_range, succ_eq_add_one, Nat.add_one_sub_one]
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ IsChain r (a :: range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ
have rw : r a 0 → (IsChain r (0 :: map succ (range n)) ↔ IsChain r (0 :: map succ (range n)))
Tactic: rw [range_succ_eq_map, isChain_cons_cons, and_congr_right_iff,
    ← isChain_range_succ, range_succ_eq_map]
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (a :: l).ranges
have cons : (∀ (a' : List ℕ),
    Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) a' → (range a).Disjoint a') ∧
  Pairwise (α := List ℕ) Disjoint (map (map fun (x : ℕ) ↦ a + x) l.ranges)
Tactic: simp only [ranges, pairwise_cons]
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ (∀ (a' : List ℕ),
      Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) a' → (range a).Disjoint a') ∧
    Pairwise (α := List ℕ) Disjoint (map (map fun (x : ℕ) ↦ a + x) l.ranges)
have cons : ∀ (a' : List ℕ), Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) a' → (range a).Disjoint a'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
cons :
  ∀ (a' : List ℕ),
    Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) a' → (range a).Disjoint a'
⊢ (∀ (a' : List ℕ),
      Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) a' → (range a).Disjoint a') ∧
    Pairwise (α := List ℕ) Disjoint (map (map fun (x : ℕ) ↦ a + x) l.ranges)
have cons₁ : Pairwise (α := List ℕ) Disjoint (map (map fun (x : ℕ) ↦ a + x) l.ranges)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s : List ℕ
hs : Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) s
⊢ (range a).Disjoint s
have cons : ∀ (s' : List ℕ),
  s' ∈ l.ranges →
    ∀
      (hs :
        Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) (map (fun (x : ℕ) ↦ a + x) s')),
      (range a).Disjoint (map (fun (x : ℕ) ↦ a + x) s')
Tactic: obtain ⟨s', _, rfl⟩ := mem_map.mp hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left : s' ∈ l.ranges
hs : Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) (map (fun (x : ℕ) ↦ a + x) s')
u : ℕ
hu : u ∈ range a
⊢ Membership.mem (γ := List ℕ) (map (fun (x : ℕ) ↦ a + x) s') u → False
have cons : (∃ (a_1 : ℕ), a_1 ∈ s' ∧ a + a_1 = u) → False
Tactic: rw [mem_map]
-- Lean 4 proof step from Mathlib.Data.List.Range (hypothesis)
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left : s' ∈ l.ranges
hs : Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) (map (fun (x : ℕ) ↦ a + x) s')
u : ℕ
hu : u ∈ range a
⊢ (∃ (a_1 : ℕ), a_1 ∈ s' ∧ a + a_1 = u) → False
have hu₁ : u < a
Tactic: rw [mem_range] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise (α := List ℕ) Disjoint (map (map fun (x : ℕ) ↦ a + x) l.ranges)
have cons : Pairwise (fun (a_1 b : List ℕ) ↦ Disjoint (α := ℕ) (map (fun (x : ℕ) ↦ a + x) a_1) (map (fun (x : ℕ) ↦ a + x) b))
  l.ranges
Tactic: rw [pairwise_map]
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise (fun (a_1 b : List ℕ) ↦ Disjoint (α := ℕ) (map (fun (x : ℕ) ↦ a + x) a_1) (map (fun (x : ℕ) ↦ a + x) b))
    l.ranges
have apply : ∀ {a_1 b : List ℕ}, a_1.Disjoint b → Disjoint (α := ℕ) (map (fun (x : ℕ) ↦ a + x) a_1) (map (fun (x : ℕ) ↦ a + x) b)
Tactic: apply Pairwise.imp _ hl
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
⊢ u.Disjoint v → Disjoint (α := ℕ) (map (fun (x : ℕ) ↦ a + x) u) (map (fun (x : ℕ) ↦ a + x) v)
have hf : Function.Injective (β := ℕ) fun (x : ℕ) ↦ a + x
Tactic: apply disjoint_map
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
l : List ℕ
⊢ Pairwise Disjoint l.ranges
have nil : Pairwise Disjoint (ranges [])
Tactic: induction l with
  | nil => exact Pairwise.nil
  | cons a l hl =>
    simp only [ranges, pairwise_cons]
    constructor
    · intro s hs
      obtain ⟨s', _, rfl⟩ := mem_map.mp hs
      intro u hu
      rw [mem_map]
      rw [mem_range] at hu
      lia
    · rw [pairwise_map]
      apply Pairwise.imp _ hl
      intro u v
      apply disjoint_map
      exact fun u v => Nat.add_left_cancel
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
l : List ℕ
nil : Pairwise Disjoint (ranges [])
⊢ Pairwise Disjoint l.ranges
have cons : ∀ (a : ℕ) (l : List ℕ) (hl : Pairwise Disjoint l.ranges), Pairwise Disjoint (a :: l).ranges
Tactic: induction l with
  | nil => exact Pairwise.nil
  | cons a l hl =>
    simp only [ranges, pairwise_cons]
    constructor
    · intro s hs
      obtain ⟨s', _, rfl⟩ := mem_map.mp hs
      intro u hu
      rw [mem_map]
      rw [mem_range] at hu
      lia
    · rw [pairwise_map]
      apply Pairwise.imp _ hl
      intro u v
      apply disjoint_map
      exact fun u v => Nat.add_left_cancel
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map length (a :: l).ranges = a :: l
have cons : map (Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x)) l.ranges = l
Tactic: simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
| l
have rw : map length l.ranges
Tactic: rw [← hl]
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map (Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x)) l.ranges = l
have cons : map (Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x)) l.ranges = map length l.ranges
Tactic: conv_rhs => rw [← hl]
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map (Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x)) l.ranges = map length l.ranges
have cons : ∀ (a_1 : List ℕ), a_1 ∈ l.ranges → Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x) a_1 = a_1.length
Tactic: apply map_congr_left
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
l : List ℕ
⊢ map length l.ranges = l
have nil : map length (ranges []) = []
Tactic: induction l with
  | nil => simp only [ranges, map_nil]
  | cons a l hl => -- (a :: l)
    simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]
    conv_rhs => rw [← hl]
    apply map_congr_left
    intro s _
    simp only [Function.comp_apply, length_map]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Range (goal)
Goal:
l : List ℕ
nil : map length (ranges []) = []
⊢ map length l.ranges = l
have cons : ∀ (a : ℕ) (l : List ℕ) (hl : map length l.ranges = l), map length (a :: l).ranges = a :: l
Tactic: induction l with
  | nil => simp only [ranges, map_nil]
  | cons a l hl => -- (a :: l)
    simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]
    conv_rhs => rw [← hl]
    apply map_congr_left
    intro s _
    simp only [Function.comp_apply, length_map]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hd : Option α
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
⊢ (map (Option.map f) (hd :: tl)).reduceOption = map f (hd :: tl).reduceOption
have cons : (map (Option.map f) (none :: tl)).reduceOption = map f (none :: tl).reduceOption
Tactic: cases hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hd : Option α
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
cons : (map (Option.map f) (none :: tl)).reduceOption = map f (none :: tl).reduceOption
⊢ (map (Option.map f) (hd :: tl)).reduceOption = map f (hd :: tl).reduceOption
have cons₁ : ∀ (val : α), (map (Option.map f) (some val :: tl)).reduceOption = map f (some val :: tl).reduceOption
Tactic: cases hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
β : Type u_2
l : List (Option α)
f : α → β
⊢ (map (Option.map f) l).reduceOption = map f l.reduceOption
have nil : (map (Option.map f) []).reduceOption = map f (reduceOption [])
Tactic: induction l with
  | nil => simp only [reduceOption_nil, map_nil]
  | cons hd tl hl =>
    cases hd <;> simpa [Option.map_some, map, eq_self_iff_true, reduceOption_cons_of_some] using hl
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
β : Type u_2
l : List (Option α)
f : α → β
nil : (map (Option.map f) []).reduceOption = map f (reduceOption [])
⊢ (map (Option.map f) l).reduceOption = map f l.reduceOption
have cons : ∀ (hd : Option α) (tl : List (Option α)) (hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption),
  (map (Option.map f) (hd :: tl)).reduceOption = map f (hd :: tl).reduceOption
Tactic: induction l with
  | nil => simp only [reduceOption_nil, map_nil]
  | cons hd tl hl =>
    cases hd <;> simpa [Option.map_some, map, eq_self_iff_true, reduceOption_cons_of_some] using hl
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
n : ℕ
⊢ Eq.{u_1 + 1} (α := List α) (filterMap id (replicate n none)) []
have rw : Eq.{u_1 + 1} (α := List α) [] []
Tactic: rw [filterMap_replicate_of_none (id_def _)]