awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
⊢ 0 ≤ HDiv.hDiv (α := α) 1 (↑n : α)

Tactic:
one_div_nonneg.mpr (cast_nonneg' n)

Premises used: Iff.mpr, one_div_nonneg, Nat.cast_nonneg'
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
hn : n ≠ 0
⊢ HDiv.hDiv (α := α) 1 (↑n : α) ≠ 0

Tactic:
_root_.ne_of_gt (one_div_cast_pos hn)

Premises used: Nat.one_div_cast_pos, ne_of_gt
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddRightMono α
n : ℕ
rw : LE.le.{u_1} (α := α) (↑n : α)⁻¹ 1
⊢ 0 ≤ 1 - HDiv.hDiv (α := α) 1 (↑n : α)

Tactic:
rw [sub_nonneg, one_div]

Premises used: one_div, sub_nonneg
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddRightMono α
n : ℕ
⊢ LE.le.{u_1} (α := α) (↑n : α)⁻¹ 1

Tactic:
cast_inv_le_one n

Premises used: Nat.cast_inv_le_one
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddRightMono α
n : ℕ
⊢ LE.le.{u_1} (α := α) (↑n : α)⁻¹ 1

Tactic:
exact cast_inv_le_one n

Premises used: Nat.cast_inv_le_one
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddLeftMono α
n : ℕ
rw : 0 ≤ HDiv.hDiv (α := α) 1 (↑n : α)
⊢ 1 - HDiv.hDiv (α := α) 1 (↑n : α) ≤ 1

Tactic:
rw [sub_le_self_iff]

Premises used: sub_le_self_iff
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddLeftMono α
n : ℕ
⊢ 0 ≤ HDiv.hDiv (α := α) 1 (↑n : α)

Tactic:
one_div_cast_nonneg n

Premises used: Nat.one_div_cast_nonneg
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddLeftMono α
n : ℕ
⊢ 0 ≤ HDiv.hDiv (α := α) 1 (↑n : α)

Tactic:
exact one_div_cast_nonneg n

Premises used: Nat.one_div_cast_nonneg
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
α : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
n : ℕ
⊢ LE.le.{u_3} (α := α) 0 (↑n : α)

Tactic:
cast_nonneg' n

Premises used: Nat.cast_nonneg'
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
α : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
n : ℕ
inst_3 : n.AtLeastTwo
⊢ LE.le.{u_3} (α := α) 0 (OfNat.ofNat n)

Tactic:
ofNat_nonneg' n

Premises used: Nat.ofNat_nonneg'
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
α : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
⊢ Eq.{u_3 + 1} (α := α) (↑(min m n) : α) (min (↑m : α) (↑n : α))

Tactic:
(@mono_cast α _).map_min

Premises used: Nat.mono_cast, Monotone.map_min
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
α : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
⊢ Eq.{u_3 + 1} (α := α) (↑(max m n) : α) (max (↑m : α) (↑n : α))

Tactic:
(@mono_cast α _).map_max

Premises used: Nat.mono_cast, Monotone.map_max
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
α : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : Nontrivial α
n : ℕ
⊢ LT.lt.{u_3} (α := α) 0 (↑n : α) ↔ 0 < n

Tactic:
cast_pos'

Premises used: Nat.cast_pos'
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
α : Type u_2
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_2} (R := α) 1
n : ℕ
inst_5 : n.AtLeastTwo
⊢ LT.lt.{u_2} (α := α) 0 (OfNat.ofNat n)

Tactic:
cast_pos'.mpr (NeZero.pos n)

Premises used: Iff.mpr, NeZero.pos, Nat.cast_pos'
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
α : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : Nontrivial α
n : ℕ
inst_4 : n.AtLeastTwo
⊢ LT.lt.{u_3} (α := α) 0 (OfNat.ofNat n)

Tactic:
ofNat_pos'

Premises used: Nat.ofNat_pos'
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
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 : α)
inr : ∀ (h : n ≤ m), (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)
⊢ (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)

Tactic:
rcases le_total m n with h | h

Premises used: le_total
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
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
inl : LE.le.{u_2} (α := α) (↑m : α) (↑n : α)
⊢ (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)

Tactic:
rw [Nat.sub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]

Premises used: tsub_eq_zero_of_le, Nat.cast_zero, Nat.sub_eq_zero_of_le
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
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
⊢ LE.le.{u_2} (α := α) (↑m : α) (↑n : α)

Tactic:
mono_cast h

Premises used: Nat.mono_cast
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
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
⊢ LE.le.{u_2} (α := α) (↑m : α) (↑n : α)

Tactic:
exact mono_cast h

Premises used: Nat.mono_cast
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
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
inr : ∀ (m : ℕ) (h : n ≤ m + n), (↑(m + n - n) : α) = HSub.hSub (α := α) (↑(m + n) : α) (↑n : α)
⊢ (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)

Tactic:
rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩

Premises used: Iff.mp, le_iff_exists_add', rfl
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
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 : α)
inr₂ inr₃ : Eq.{u_2 + 1} (α := α) (↑m : α) (↑m : α)
⊢ (↑(m + n - n) : α) = HSub.hSub (α := α) (↑(m + n) : α) (↑n : α)

Tactic:
rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]

Premises used: Nat.cast_add, add_tsub_cancel_right
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
R : Type u_1
inst : Ring R
inst_1 : Lattice R
inst_2 : IsOrderedRing R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) |(↑n : R)| (↑n : R)

Tactic:
abs_of_nonneg n.cast_nonneg

Premises used: Nat.cast_nonneg, abs_of_nonneg
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
R : Type u_1
inst : Ring R
inst_1 : Lattice R
inst_2 : IsOrderedRing R
n : ℕ
inst_3 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) |OfNat.ofNat n| (OfNat.ofNat n)

Tactic:
abs_cast n

Premises used: Nat.abs_cast
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
m n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (-(↑m : R)) (↑n : R) ↔ m = 0 ∧ n = 0

Tactic:
simp [neg_eq_iff_add_eq_zero, ← cast_add]

Premises used: neg_eq_iff_add_eq_zero, Nat.cast_add
-- Module: Mathlib.Data.Nat.Cast.Order.Ring
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
m n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑m : R) (-(↑n : R)) ↔ m = 0 ∧ n = 0

Tactic:
simp [eq_neg_iff_add_eq_zero, ← cast_add]

Premises used: Nat.cast_add, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Data.Nat.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
n : ℕ
zero : Eq.{u_1 + 1} (α := α) (↑0 : α × β).1 (↑0 : α)
succ :
  ∀ (n : ℕ), Eq.{u_1 + 1} (α := α) (↑n : α × β).1 (↑n : α) → Eq.{u_1 + 1} (α := α) (↑(n + 1) : α × β).1 (↑(n + 1) : α)
⊢ Eq.{u_1 + 1} (α := α) (↑n : α × β).1 (↑n : α)

Tactic:
induction n
-- Module: Mathlib.Data.Nat.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
⊢ Eq.{u_1 + 1} (α := α) (↑0 : α × β).1 (↑0 : α)

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
n : ℕ
h : Eq.{u_1 + 1} (α := α) (↑n : α × β).1 (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(n + 1) : α × β).1 (↑(n + 1) : α)

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := α) (OfNat.ofNat n).1 (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
n : ℕ
zero : Eq.{u_2 + 1} (α := β) (↑0 : α × β).2 (↑0 : β)
succ :
  ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) (↑n : α × β).2 (↑n : β) → Eq.{u_2 + 1} (α := β) (↑(n + 1) : α × β).2 (↑(n + 1) : β)
⊢ Eq.{u_2 + 1} (α := β) (↑n : α × β).2 (↑n : β)

Tactic:
induction n
-- Module: Mathlib.Data.Nat.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
⊢ Eq.{u_2 + 1} (α := β) (↑0 : α × β).2 (↑0 : β)

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
n : ℕ
h : Eq.{u_2 + 1} (α := β) (↑n : α × β).2 (↑n : β)
⊢ Eq.{u_2 + 1} (α := β) (↑(n + 1) : α × β).2 (↑(n + 1) : β)

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddMonoidWithOne α
inst_1 : AddMonoidWithOne β
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Eq.{u_2 + 1} (α := β) (OfNat.ofNat n).2 (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.SetInterval
Goal:
⊢ Eq (α := Set ℤ) (range Nat.cast) (Ici 0)

Tactic:
Subset.antisymm (range_subset_iff.2 Int.natCast_nonneg) CanLift.prf

Premises used: Set.Subset.antisymm, Iff.mpr, Set.range_subset_iff, Int.natCast_nonneg, CanLift.prf
-- Module: Mathlib.Data.Nat.Cast.SetInterval
Goal:
a b : ℕ
⊢ OrdConnected (α := ℤ) (range (ι := ℕ) (⇑castOrderEmbedding : (a : ℕ) → ℤ))

Tactic:
simp [ordConnected_Ici]

Premises used: Set.ordConnected_Ici
-- Module: Mathlib.Data.Nat.Cast.SetInterval
Goal:
a : ℕ
rw : Eq (α := Set ℤ) (Icc (↑⊥ : ℤ) (↑a : ℤ)) (Icc 0 (↑a : ℤ))
⊢ Eq (α := Set ℤ) (Nat.cast '' Iic a) (Icc 0 (↑a : ℤ))

Tactic:
rw [← Icc_bot, image_cast_int_Icc]

Premises used: Nat.image_cast_int_Icc, Set.Icc_bot
-- Module: Mathlib.Data.Nat.Cast.SetInterval
Goal:
a : ℕ
⊢ Eq (α := Set ℤ) (Icc (↑⊥ : ℤ) (↑a : ℤ)) (Icc 0 (↑a : ℤ))

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Cast.SetInterval
Goal:
a : ℕ
rw : Eq (α := Set ℤ) (Ico (↑⊥ : ℤ) (↑a : ℤ)) (Ico 0 (↑a : ℤ))
⊢ Eq (α := Set ℤ) (Nat.cast '' Iio a) (Ico 0 (↑a : ℤ))

Tactic:
rw [← Ico_bot, image_cast_int_Ico]

Premises used: Set.Ico_bot, Nat.image_cast_int_Ico
-- Module: Mathlib.Data.Nat.Cast.SetInterval
Goal:
a : ℕ
⊢ Eq (α := Set ℤ) (Ico (↑⊥ : ℤ) (↑a : ℤ)) (Ico 0 (↑a : ℤ))

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Cast.SetInterval
Goal:
a : ℕ
⊢ IsUpperSet (α := ℤ) (range (ι := ℕ) (⇑castOrderEmbedding : (a : ℕ) → ℤ))

Tactic:
simp [isUpperSet_Ici]

Premises used: isUpperSet_Ici
-- Module: Mathlib.Data.Nat.Cast.Synonym
Goal:
α : Type u_1
inst : NatCast α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Lex α) ((toLex : (a : α) → Lex α) (↑n : α) : Lex α) ((↑n : Lex α) : Lex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Synonym
Goal:
α : Type u_1
inst : NatCast α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := Lex α) ((toLex : (a : α) → Lex α) (OfNat.ofNat n) : Lex α) (OfNat.ofNat n : Lex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Synonym
Goal:
α : Type u_1
inst : NatCast α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) ((ofLex : (a : Lex α) → α) (↑n : Lex α) : α) ((↑n : α) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Synonym
Goal:
α : Type u_1
inst : NatCast α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := α) ((ofLex : (a : Lex α) → α) (OfNat.ofNat n) : α) (OfNat.ofNat n : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.WithTop
Goal:
n : ℕ
⊢ (↑n : WithTop ℕ) = (↑n : WithTop ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.WithTop
Goal:
n : ℕ
⊢ (↑n : WithBot ℕ) = (↑n : WithBot ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
a b : ℕ
co : List.Pairwise Coprime []
⊢ a ≡ b [MOD List.prod []] ↔ ∀ (i : Fin (List.length (α := ℕ) [])), a ≡ b [MOD List.get [] i]

Tactic:
simp [modEq_one]

Premises used: Nat.modEq_one
-- Module: Mathlib.Data.Nat.ChineseRemainder
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)
⊢ m.Coprime l.prod

Tactic:
have : Coprime m l.prod := coprime_list_prod_right_iff.mpr (List.pairwise_cons.mp co).1
-- Module: Mathlib.Data.Nat.ChineseRemainder
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 :: l).prod] ↔ ∀ (i : Fin (m :: l).length), 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]

Premises used: List.length_cons, Nat.modEq_and_modEq_iff_modEq_mul, List.prod_cons, List.Pairwise.of_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
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]
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]
⊢ (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
-- Module: Mathlib.Data.Nat.ChineseRemainder
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]
cons₁ : ∀ (i : Fin l.length), a ≡ b [MOD (m :: l).get i.succ]
⊢ a ≡ b [MOD (m :: l).get i]

Tactic:
cases i using Fin.cases
-- Module: Mathlib.Data.Nat.ChineseRemainder
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]
⊢ a ≡ b [MOD (m :: l).get 0]

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.ChineseRemainder
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
⊢ a ≡ b [MOD (m :: l).get i.succ]

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.ChineseRemainder
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
h : ∀ (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:
⟨h 0, fun i => h i.succ⟩

Premises used: Fin.succ, And.intro, OfNat.ofNat
-- Module: Mathlib.Data.Nat.ChineseRemainder
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
h : ∀ (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:
exact ⟨h 0, fun i => h i.succ⟩
-- Module: Mathlib.Data.Nat.ChineseRemainder
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]
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]
⊢ a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD 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⟩

Premises used: Nat.modEq_one, List.length_cons, List.prod_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a b : ℕ
s : ι → ℕ
co : List.Pairwise (Coprime on s) []
⊢ a ≡ b [MOD (List.map s []).prod] ↔ ∀ (i : ι), Membership.mem (γ := List ι) [] i → a ≡ b [MOD s i]

Tactic:
simp [modEq_one]

Premises used: Nat.modEq_one
-- Module: Mathlib.Data.Nat.ChineseRemainder
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)
simp : ∀ a ∈ l, (s i).Coprime (s a)
⊢ (s i).Coprime (List.map s l).prod

Tactic:
simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]

Premises used: and_imp, forall_exists_index, List.mem_map, Nat.coprime_list_prod_right_iff, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Data.Nat.ChineseRemainder
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)
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Tactic:
(List.pairwise_cons.mp co).1 j hj

Premises used: List.pairwise_cons, And.left, Iff.mp
-- Module: Mathlib.Data.Nat.ChineseRemainder
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)
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Tactic:
exact (List.pairwise_cons.mp co).1 j hj

Premises used: List.pairwise_cons, And.left, Iff.mp
-- Module: Mathlib.Data.Nat.ChineseRemainder
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

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
-- Module: Mathlib.Data.Nat.ChineseRemainder
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)
this : (s i).Coprime (List.map s l).prod
⊢ a ≡ b [MOD (List.map s (i :: l)).prod] ↔ ∀ i_1 ∈ i :: l, a ≡ b [MOD s i_1]

Tactic:
simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]

Premises used: Nat.modEq_and_modEq_iff_modEq_mul, List.Pairwise.of_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
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]
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]
⊢ a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, 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)]

Premises used: Nat.modEq_one
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
h : List.Pairwise (Coprime on s) []
⊢ ∀ (i : ι), Membership.mem (γ := List ι) [] i → 0 ≡ a i [MOD s i]

Tactic:
simp
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
simp : ∀ a ∈ l, (s i).Coprime (s a)
⊢ (s i).Coprime (List.map s l).prod

Tactic:
simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]

Premises used: and_imp, forall_exists_index, List.mem_map, Nat.coprime_list_prod_right_iff, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Tactic:
(List.pairwise_cons.mp co).1 j hj

Premises used: List.pairwise_cons, And.left, Iff.mp
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Tactic:
exact (List.pairwise_cons.mp co).1 j hj

Premises used: List.pairwise_cons, And.left, Iff.mp
-- Module: Mathlib.Data.Nat.ChineseRemainder
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

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
-- Module: Mathlib.Data.Nat.ChineseRemainder
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
have : (ih : { k : ℕ // ∀ i ∈ l, k ≡ a i [MOD s i] }) → { k : ℕ // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }
⊢ { k : ℕ // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }

Tactic:
have ih := chineseRemainderOfList l co.of_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
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] }
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] }
⊢ { k : ℕ // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }

Tactic:
have k := chineseRemainder this (a i) ih
-- Module: Mathlib.Data.Nat.ChineseRemainder
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] }
property : ∀ i_1 ∈ i :: l, (↑k : ℕ) ≡ a i_1 [MOD s i_1]
⊢ { k : ℕ // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }

Tactic:
use k