awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
⊢ (↑(m / n) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑n : α)
have zero : (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑0 : α)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
zero : (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑0 : α)
⊢ (↑(m / n) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑n : α)
have succ : ∀ (n : ℕ), (↑(m / (n + 1)) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑(n + 1) : α)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m : ℕ
⊢ (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑0 : α)
have zero : (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) 0
Tactic: rw [cast_zero, div_zero, Nat.div_zero, cast_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m : ℕ
zero : (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) 0
⊢ (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑0 : α)
have zero₁ : LE.le.{u_1} (α := α) (↑(m / 0) : α) 0
Tactic: rw [cast_zero, div_zero, Nat.div_zero, cast_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m : ℕ
zero : (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) 0
zero₁ : LE.le.{u_1} (α := α) (↑(m / 0) : α) 0
⊢ (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑0 : α)
have zero₂ : LE.le.{u_1} (α := α) (↑0 : α) 0
Tactic: rw [cast_zero, div_zero, Nat.div_zero, cast_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m : ℕ
zero : (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) 0
zero₁ : LE.le.{u_1} (α := α) (↑(m / 0) : α) 0
zero₂ : LE.le.{u_1} (α := α) (↑0 : α) 0
⊢ (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑0 : α)
have zero₃ : LE.le.{u_1} (α := α) 0 0
Tactic: rw [cast_zero, div_zero, Nat.div_zero, cast_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
⊢ (↑(m / (n + 1)) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑(n + 1) : α)
have succ : m / (n + 1) * (n + 1) ≤ m
Tactic: rw [le_div_iff₀, ← Nat.cast_mul, @Nat.cast_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
succ : m / (n + 1) * (n + 1) ≤ m
⊢ (↑(m / (n + 1)) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑(n + 1) : α)
have succ₁ : LT.lt.{u_1} (α := α) 0 (↑(n + 1) : α)
Tactic: rw [le_div_iff₀, ← Nat.cast_mul, @Nat.cast_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
⊢ 0 < 1 / HAdd.hAdd (α := α) (↑n : α) 1
have rw : 0 < (HAdd.hAdd (α := α) (↑n : α) 1)⁻¹
Tactic: rw [one_div]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ 1 / HAdd.hAdd (α := α) (↑m : α) 1 ≤ 1 / HAdd.hAdd (α := α) (↑n : α) 1
have refine_1 : 0 < HAdd.hAdd (α := α) (↑n : α) 1
Tactic: refine one_div_le_one_div_of_le ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
refine_1 : 0 < HAdd.hAdd (α := α) (↑n : α) 1
⊢ 1 / HAdd.hAdd (α := α) (↑m : α) 1 ≤ 1 / HAdd.hAdd (α := α) (↑n : α) 1
have refine_2 : HAdd.hAdd (α := α) (↑n : α) 1 ≤ HAdd.hAdd (α := α) (↑m : α) 1
Tactic: refine one_div_le_one_div_of_le ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ 1 / HAdd.hAdd (α := α) (↑m : α) 1 < 1 / HAdd.hAdd (α := α) (↑n : α) 1
have refine_1 : 0 < HAdd.hAdd (α := α) (↑n : α) 1
Tactic: refine one_div_lt_one_div_of_lt ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n < m
refine_1 : 0 < HAdd.hAdd (α := α) (↑n : α) 1
⊢ 1 / HAdd.hAdd (α := α) (↑m : α) 1 < 1 / HAdd.hAdd (α := α) (↑n : α) 1
have refine_2 : HAdd.hAdd (α := α) (↑n : α) 1 < HAdd.hAdd (α := α) (↑m : α) 1
Tactic: refine one_div_lt_one_div_of_lt ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddRightMono α
n : ℕ
⊢ 0 ≤ 1 - HDiv.hDiv (α := α) 1 (↑n : α)
have rw : LE.le.{u_1} (α := α) (↑n : α)⁻¹ 1
Tactic: rw [sub_nonneg, one_div]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Field (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddLeftMono α
n : ℕ
⊢ 1 - HDiv.hDiv (α := α) 1 (↑n : α) ≤ 1
have rw : 0 ≤ HDiv.hDiv (α := α) 1 (↑n : α)
Tactic: rw [sub_le_self_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Ring (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : CanonicallyOrderedAdd α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : AddLeftReflectLE α
m n : ℕ
⊢ (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)
have inl : ∀ (h : m ≤ n), (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)
Tactic: rcases le_total m n with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Ring (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : CanonicallyOrderedAdd α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : AddLeftReflectLE α
m n : ℕ
inl : ∀ (h : m ≤ n), (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)
⊢ (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)
have inr : ∀ (h : n ≤ m), (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)
Tactic: rcases le_total m n with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Ring (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : CanonicallyOrderedAdd α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)
have inl : LE.le.{u_2} (α := α) (↑m : α) (↑n : α)
Tactic: rw [Nat.sub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Ring (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : CanonicallyOrderedAdd α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : AddLeftReflectLE α
m n : ℕ
h : n ≤ m
⊢ (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)
have inr : ∀ (m : ℕ) (h : n ≤ m + n), (↑(m + n - n) : α) = HSub.hSub (α := α) (↑(m + n) : α) (↑n : α)
Tactic: rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Ring (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : CanonicallyOrderedAdd α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : AddLeftReflectLE α
n m : ℕ
h : n ≤ m + n
⊢ (↑(m + n - n) : α) = HSub.hSub (α := α) (↑(m + n) : α) (↑n : α)
have inr : (↑m : α) = HSub.hSub (α := α) (↑(m + n) : α) (↑n : α)
Tactic: rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Ring (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : CanonicallyOrderedAdd α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : AddLeftReflectLE α
n m : ℕ
h : n ≤ m + n
inr : (↑m : α) = HSub.hSub (α := α) (↑(m + n) : α) (↑n : α)
⊢ (↑(m + n - n) : α) = HSub.hSub (α := α) (↑(m + n) : α) (↑n : α)
have inr₁ : (↑m : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α) - (↑n : α)
Tactic: rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Ring (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : CanonicallyOrderedAdd α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : AddLeftReflectLE α
n m : ℕ
h : n ≤ m + n
inr : (↑m : α) = HSub.hSub (α := α) (↑(m + n) : α) (↑n : α)
inr₁ : (↑m : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α) - (↑n : α)
⊢ (↑(m + n - n) : α) = HSub.hSub (α := α) (↑(m + n) : α) (↑n : α)
have inr₂ : Eq.{u_2 + 1} (α := α) (↑m : α) (↑m : α)
Tactic: rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑n : α × β).1 (↑n : α)
have zero : Eq.{u_1 + 1} (α := α) (↑0 : α × β).1 (↑0 : α)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
n : ℕ
zero : Eq.{u_1 + 1} (α := α) (↑0 : α × β).1 (↑0 : α)
⊢ Eq.{u_1 + 1} (α := α) (↑n : α × β).1 (↑n : α)
have succ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := α) (↑n : α × β).1 (↑n : α) → Eq.{u_1 + 1} (α := α) (↑(n + 1) : α × β).1 (↑(n + 1) : α)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
n : ℕ
⊢ Eq.{u_2 + 1} (α := β) (↑n : α × β).2 (↑n : β)
have zero : Eq.{u_2 + 1} (α := β) (↑0 : α × β).2 (↑0 : β)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
n : ℕ
zero : Eq.{u_2 + 1} (α := β) (↑0 : α × β).2 (↑0 : β)
⊢ Eq.{u_2 + 1} (α := β) (↑n : α × β).2 (↑n : β)
have succ : ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) (↑n : α × β).2 (↑n : β) → Eq.{u_2 + 1} (α := β) (↑(n + 1) : α × β).2 (↑(n + 1) : β)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.SetInterval (goal)
Goal:
a : ℕ
⊢ Eq (α := Set ℤ) (Nat.cast '' Iic a) (Icc 0 (↑a : ℤ))
have rw : Eq (α := Set ℤ) (Icc (↑⊥ : ℤ) (↑a : ℤ)) (Icc 0 (↑a : ℤ))
Tactic: rw [← Icc_bot, image_cast_int_Icc]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.SetInterval (goal)
Goal:
a : ℕ
⊢ Eq (α := Set ℤ) (Nat.cast '' Iio a) (Ico 0 (↑a : ℤ))
have rw : Eq (α := Set ℤ) (Ico (↑⊥ : ℤ) (↑a : ℤ)) (Ico 0 (↑a : ℤ))
Tactic: rw [← Ico_bot, image_cast_int_Ico]
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (hypothesis)
Goal:
a b m : ℕ
l : List ℕ
ih : ∀ (co : List.Pairwise Coprime l), a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
co : List.Pairwise Coprime (m :: l)
⊢ a ≡ b [MOD (m :: l).prod] ↔ ∀ (i : Fin (m :: l).length), a ≡ b [MOD (m :: l).get i]
have this : m.Coprime l.prod
Tactic: have : Coprime m l.prod := coprime_list_prod_right_iff.mpr (List.pairwise_cons.mp co).1
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
a b m : ℕ
l : List ℕ
ih : ∀ (co : List.Pairwise Coprime l), a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
⊢ a ≡ b [MOD (m :: l).prod] ↔ ∀ (i : Fin (m :: l).length), a ≡ b [MOD (m :: l).get i]
have cons : (a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]) ↔ ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]
Tactic: simp only [List.prod_cons, ← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co),
      List.length_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
a b m : ℕ
l : List ℕ
ih : ∀ (co : List.Pairwise Coprime l), a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
⊢ (a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]) ↔ ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]
have cons : (a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]) → ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
a b m : ℕ
l : List ℕ
ih : ∀ (co : List.Pairwise Coprime l), a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
cons :
  (a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]) → ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]
⊢ (a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]) ↔ ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]
have cons₁ : (∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]) → a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
a b m : ℕ
l : List ℕ
ih : ∀ (co : List.Pairwise Coprime l), a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
i : Fin (l.length + 1)
⊢ a ≡ b [MOD (m :: l).get i]
have cons : a ≡ b [MOD (m :: l).get 0]
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
a b m : ℕ
l : List ℕ
ih : ∀ (co : List.Pairwise Coprime l), a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
i : Fin (l.length + 1)
cons : a ≡ b [MOD (m :: l).get 0]
⊢ a ≡ b [MOD (m :: l).get i]
have cons₁ : ∀ (i : Fin l.length), a ≡ b [MOD (m :: l).get i.succ]
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
a b : ℕ
l : List ℕ
co : List.Pairwise Coprime l
⊢ a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
have nil : ∀ (co : List.Pairwise Coprime []),
  a ≡ b [MOD List.prod []] ↔ ∀ (i : Fin (List.length (α := ℕ) [])), a ≡ b [MOD List.get [] i]
Tactic: induction l with
  | nil => simp [modEq_one]
  | cons m l ih =>
    have : Coprime m l.prod := coprime_list_prod_right_iff.mpr (List.pairwise_cons.mp co).1
    simp only [List.prod_cons, ← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co),
      List.length_cons]
    constructor
    · rintro ⟨h0, hs⟩ i
      cases i using Fin.cases <;> simp_all
    · intro h; exact ⟨h 0, fun i => h i.succ⟩
Cleared hypotheses: l, co
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
a b : ℕ
l : List ℕ
co : List.Pairwise Coprime l
nil :
  ∀ (co : List.Pairwise Coprime []),
    a ≡ b [MOD List.prod []] ↔ ∀ (i : Fin (List.length (α := ℕ) [])), a ≡ b [MOD List.get [] i]
⊢ a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
have cons : ∀ (m : ℕ) (l : List ℕ)
  (ih : ∀ (co : List.Pairwise Coprime l), a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
  (co : List.Pairwise Coprime (m :: l)),
  a ≡ b [MOD (m :: l).prod] ↔ ∀ (i : Fin (m :: l).length), a ≡ b [MOD (m :: l).get i]
Tactic: induction l with
  | nil => simp [modEq_one]
  | cons m l ih =>
    have : Coprime m l.prod := coprime_list_prod_right_iff.mpr (List.pairwise_cons.mp co).1
    simp only [List.prod_cons, ← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co),
      List.length_cons]
    constructor
    · rintro ⟨h0, hs⟩ i
      cases i using Fin.cases <;> simp_all
    · intro h; exact ⟨h 0, fun i => h i.succ⟩
Cleared hypotheses: l, co
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : ∀ (co : List.Pairwise (Coprime on s) l), a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i]
co : List.Pairwise (Coprime on s) (i :: l)
⊢ (s i).Coprime (List.map s l).prod
have simp : ∀ a ∈ l, (s i).Coprime (s a)
Tactic: simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (hypothesis)
Goal:
ι : Type u_1
a b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : ∀ (co : List.Pairwise (Coprime on s) l), a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i]
co : List.Pairwise (Coprime on s) (i :: l)
⊢ a ≡ b [MOD (List.map s (i :: l)).prod] ↔ ∀ i_1 ∈ i :: l, a ≡ b [MOD s i_1]
have this : (s i).Coprime (List.map s l).prod
Tactic: have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a b : ℕ
s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
⊢ a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i]
have nil : ∀ (co : List.Pairwise (Coprime on s) []),
  a ≡ b [MOD (List.map s []).prod] ↔ ∀ (i : ι), Membership.mem (γ := List ι) [] i → a ≡ b [MOD s i]
Tactic: induction l with
  | nil => simp [modEq_one]
  | cons i l ih =>
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]
Cleared hypotheses: l, co
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a b : ℕ
s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
nil :
  ∀ (co : List.Pairwise (Coprime on s) []),
    a ≡ b [MOD (List.map s []).prod] ↔ ∀ (i : ι), Membership.mem (γ := List ι) [] i → a ≡ b [MOD s i]
⊢ a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i]
have cons : ∀ (i : ι) (l : List ι)
  (ih : ∀ (co : List.Pairwise (Coprime on s) l), a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
  (co : List.Pairwise (Coprime on s) (i :: l)),
  a ≡ b [MOD (List.map s (i :: l)).prod] ↔ ∀ i_1 ∈ i :: l, a ≡ b [MOD s i_1]
Tactic: induction l with
  | nil => simp [modEq_one]
  | cons i l ih =>
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]
Cleared hypotheses: l, co
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
⊢ (s i).Coprime (List.map s l).prod
have simp : ∀ a ∈ l, (s i).Coprime (s a)
Tactic: simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (hypothesis)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
⊢ { k : ℕ // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }
have this : (s i).Coprime (List.map s l).prod
Tactic: have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
⊢ { k : ℕ // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }
have have : (ih : { k : ℕ // ∀ i ∈ l, k ≡ a i [MOD s i] }) → { k : ℕ // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }
Tactic: have ih := chineseRemainderOfList l co.of_cons
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k : ℕ // ∀ i ∈ l, k ≡ a i [MOD s i] }
⊢ { k : ℕ // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }
have have : (k : { k : ℕ // k ≡ a i [MOD s i] ∧ k ≡ (↑ih : ℕ) [MOD (List.map s l).prod] }) →
  { k : ℕ // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }
Tactic: have k := chineseRemainder this (a i) ih
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k : ℕ // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k : ℕ // k ≡ a i [MOD s i] ∧ k ≡ (↑ih : ℕ) [MOD (List.map s l).prod] }
⊢ { k : ℕ // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }
have property : ∀ i_1 ∈ i :: l, (↑k : ℕ) ≡ a i_1 [MOD s i_1]
Tactic: use k
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k : ℕ // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k : ℕ // k ≡ a i [MOD s i] ∧ k ≡ (↑ih : ℕ) [MOD (List.map s l).prod] }
⊢ ∀ i_1 ∈ i :: l, (↑k : ℕ) ≡ a i_1 [MOD s i_1]
have property : ∀ a_1 ∈ l, (↑k : ℕ) ≡ a a_1 [MOD s a_1]
Tactic: simp only [List.mem_cons, forall_eq_or_imp, k.prop.1, true_and]
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ (↑(chineseRemainderOfList a s (i :: l) co) : ℕ) < (List.map s (i :: l)).prod
have cons : (↑(chineseRemainder sorry (a i) (↑(chineseRemainderOfList a s l sorry) : ℕ)) : ℕ) < s i * (List.map s l).prod
Tactic: simp only [chineseRemainderOfList, List.map_cons, List.prod_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ (s i).Coprime (List.map s l).prod
have simp : ∀ a ∈ l, (s i).Coprime (s a)
Tactic: simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (hypothesis)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ (↑(chineseRemainder ⋯ (a i) (↑(chineseRemainderOfList a s l ⋯) : ℕ)) : ℕ) < s i * (List.map s l).prod
have this : (s i).Coprime (List.map s l).prod
Tactic: have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ (↑(chineseRemainder ⋯ (a i) (↑(chineseRemainderOfList a s l ⋯) : ℕ)) : ℕ) < s i * (List.map s l).prod
have cons : (List.map s l).prod ≠ 0
Tactic: refine chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons)
      (hs i List.mem_cons_self) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ (List.map s l).prod ≠ 0
have cons : ∀ x ∈ l, ¬s x = 0
Tactic: simp only [ne_eq, List.prod_eq_zero_iff, List.mem_map, not_exists, not_and]