awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
he : ¬AddChar.IsPrimitive.{0, u_1} (R := ZMod N) (R' := R) e
hχ : gaussSum χ e ≠ 0
rcases :
  ∀ (d : ℕ) (hd₁ : d ∣ N) (hd₂ : d < N) (hed : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1),
    ¬χ.IsPrimitive
⊢ ¬χ.IsPrimitive

Tactic:
rcases e.exists_divisor_of_not_isPrimitive he with ⟨d, hd₁, hd₂, hed⟩

Premises used: AddChar.exists_divisor_of_not_isPrimitive
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
he : ¬AddChar.IsPrimitive.{0, u_1} (R := ZMod N) (R' := R) e
hχ : gaussSum χ e ≠ 0
d : ℕ
hd₁ : d ∣ N
hd₂ : d < N
hed : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
⊢ χ.conductor ≤ d

Tactic:
have : χ.conductor ≤ d := Nat.sInf_le <| factorsThrough_of_gaussSum_ne_zero e hd₁ hed hχ
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
he : ¬AddChar.IsPrimitive.{0, u_1} (R := ZMod N) (R' := R) e
hχ : gaussSum χ e ≠ 0
d : ℕ
hd₁ : d ∣ N
hd₂ : d < N
hed : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
this : χ.conductor ≤ d
⊢ ¬χ.IsPrimitive

Tactic:
(this.trans_lt hd₂).ne

Premises used: DirichletCharacter.IsPrimitive, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
he : ¬AddChar.IsPrimitive.{0, u_1} (R := ZMod N) (R' := R) e
hχ : gaussSum χ e ≠ 0
d : ℕ
hd₁ : d ∣ N
hd₂ : d < N
hed : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
this : χ.conductor ≤ d
⊢ ¬χ.IsPrimitive

Tactic:
exact (this.trans_lt hd₂).ne

Premises used: LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
pos : ∀ (ha : IsUnit a), gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)
neg : ∀ (ha : ¬IsUnit a), gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)
⊢ gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)

Tactic:
by_cases ha : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : IsUnit a
⊢ gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)

Tactic:
simpa [ha.unit_spec] using gaussSum_mulShift_eq χ e ha.unit

Premises used: gaussSum_mulShift_eq, IsUnit.unit, IsUnit.unit_spec
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
neg : gaussSum χ (e.mulShift a) = 0
⊢ gaussSum χ (e.mulShift a) = HMul.hMul (α := R) ((χ⁻¹ : (a : ZMod N) → R) a : R) (gaussSum χ e)

Tactic:
rw [MulChar.map_nonunit _ ha, zero_mul]

Premises used: MulZeroClass.zero_mul, MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = 0

Tactic:
gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive _ hχ (not_isPrimitive_mulShift e ha)

Premises used: gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive, AddChar.not_isPrimitive_mulShift
-- Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
inst_2 : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = 0

Tactic:
exact gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive _ hχ (not_isPrimitive_mulShift e ha)

Premises used: gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive, AddChar.not_isPrimitive_mulShift
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nonempty.{max 1 (u_1 + 1)} (DirichletCharacter R n ≃* (ZMod n)ˣ)

Tactic:
MulChar.mulEquiv_units ..

Premises used: MulChar.mulEquiv_units
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
rw : Nat.card.{u_1} (DirichletCharacter R n) = Nat.card (ZMod n)ˣ
⊢ Nat.card.{u_1} (DirichletCharacter R n) = n.totient

Tactic:
rw [← ZMod.card_units_eq_totient n, ← Nat.card_eq_fintype_card]

Premises used: ZMod.card_units_eq_totient, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nat.card.{u_1} (DirichletCharacter R n) = Nat.card (ZMod n)ˣ

Tactic:
Nat.card_congr (mulEquiv_units R n).some.toEquiv

Premises used: DirichletCharacter.mulEquiv_units, Nonempty.some, MulEquiv.toEquiv, Nat.card_congr
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nat.card.{u_1} (DirichletCharacter R n) = Nat.card (ZMod n)ˣ

Tactic:
exact Nat.card_congr (mulEquiv_units R n).some.toEquiv

Premises used: DirichletCharacter.mulEquiv_units, Nonempty.some, MulEquiv.toEquiv, Nat.card_congr
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : Nontrivial R
a : ZMod n
ha : a ≠ 1
⊢ ∃ (χ : DirichletCharacter R n), Ne (α := R) ((χ : (a : ZMod n) → R) a : R) (1 : R)

Tactic:
MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity (ZMod n) R ha

Premises used: ZMod, MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : a ≠ 1
obtain :
  ∀ (χ : DirichletCharacter R n) (hχ : Ne (α := R) ((χ : (a : ZMod n) → R) a : R) (1 : R)),
    Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0

Tactic:
obtain ⟨χ, hχ⟩ := exists_apply_ne_one_of_hasEnoughRootsOfUnity R ha

Premises used: DirichletCharacter.exists_apply_ne_one_of_hasEnoughRootsOfUnity
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : Ne (α := R) ((χ : (a : ZMod n) → R) a : R) (1 : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0

Tactic:
eq_zero_of_mul_eq_self_left hχ ?_

Premises used: eq_zero_of_mul_eq_self_left
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : Ne (α := R) ((χ : (a : ZMod n) → R) a : R) (1 : R)
refine :
  HMul.hMul (α := R) (β := R) ((χ : (a : ZMod n) → R) a : R)
      (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a : R) =
    ∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0

Tactic:
refine eq_zero_of_mul_eq_self_left hχ ?_

Premises used: eq_zero_of_mul_eq_self_left
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : Ne (α := R) ((χ : (a : ZMod n) → R) a : R) (1 : R)
simp :
  Eq.{u_1 + 1} (α := R) (∑ x : DirichletCharacter R n, (χ * x : (a : ZMod n) → R) a)
    (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a)
⊢ HMul.hMul (α := R) (β := R) ((χ : (a : ZMod n) → R) a : R)
      (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a : R) =
    ∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a

Tactic:
simp only [Finset.mul_sum, ← MulChar.mul_apply]

Premises used: Finset.mul_sum, MulChar.mul_apply
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : Ne (α := R) ((χ : (a : ZMod n) → R) a : R) (1 : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ x : DirichletCharacter R n, (χ * x : (a : ZMod n) → R) a)
    (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a)

Tactic:
Fintype.sum_bijective _ (Group.mulLeft_bijective χ) _ _ fun χ' ↦ rfl

Premises used: Group.mulLeft_bijective, Fintype.sum_bijective, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : Ne (α := R) ((χ : (a : ZMod n) → R) a : R) (1 : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ x : DirichletCharacter R n, (χ * x : (a : ZMod n) → R) a)
    (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a)

Tactic:
exact Fintype.sum_bijective _ (Group.mulLeft_bijective χ) _ _ fun χ' ↦ rfl

Premises used: Group.mulLeft_bijective, Fintype.sum_bijective, rfl
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
pos : ∀ (ha : a = 1), Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) (↑n.totient : R)
neg : ∀ (ha : ¬a = 1), Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) (if a = 1 then (↑n.totient : R) else 0)

Tactic:
split_ifs with ha
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : a = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) (↑n.totient : R)

Tactic:
simpa only [ha, map_one, Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one,
      ← Nat.card_eq_fintype_card]
      using congrArg Nat.cast <| card_eq_totient_of_hasEnoughRootsOfUnity R n

Premises used: Finset.card_univ, congrArg, Nat.cast, map_one, nsmul_eq_mul, DirichletCharacter.card_eq_totient_of_hasEnoughRootsOfUnity, mul_one, Nat.card_eq_fintype_card, Finset.sum_const
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : ¬a = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0

Tactic:
sum_characters_eq_zero R ha

Premises used: DirichletCharacter.sum_characters_eq_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : ¬a = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0

Tactic:
exact sum_characters_eq_zero R ha

Premises used: DirichletCharacter.sum_characters_eq_zero
-- Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
ha : IsUnit a
b : ZMod n
⊢ Eq.{u_1 + 1} (α := R)
    (∑ χ : DirichletCharacter R n,
      HMul.hMul (α := R) (β := R) ((χ : (a : ZMod n) → R) a⁻¹ : R) ((χ : (a : ZMod n) → R) b : R))
    (if a = b then (↑n.totient : R) else 0)

Tactic:
simp only [← map_mul, sum_characters_eq, ZMod.inv_mul_eq_one_of_isUnit ha]

Premises used: DirichletCharacter.sum_characters_eq, map_mul, ZMod.inv_mul_eq_one_of_isUnit
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n x₁ x₂ : ℕ
x_1 : ℕ × ℕ
x y : ℕ
hx₁ :
  Membership.mem (γ := Option (ℕ × ℕ))
    ((fun (x : ℕ) ↦
        let y := n / x;
        if x * y = n then some (x, y) else none)
      x₁)
    (x, y)
hx₂ :
  Membership.mem (γ := Option (ℕ × ℕ))
    ((fun (x : ℕ) ↦
        let y := n / x;
        if x * y = n then some (x, y) else none)
      x₂)
    (x, y)
⊢ x₁ = x₂

Tactic:
aesop
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
h₁ : ∀ (a : ℕ), a ∈ {d ∈ range n.succ | d ∣ n} ↔ a ∈ n.divisors
⊢ {d ∈ range n.succ | d ∣ n} = n.divisors

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
a : ℕ
h₁ : a ∣ n → a < n.succ → 1 ≤ a
⊢ a ∈ {d ∈ range n.succ | d ∣ n} ↔ a ∈ n.divisors

Tactic:
simp only [divisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]

Premises used: Finset.mem_range, Nat.divisors, and_congr_left_iff, Finset.mem_filter, iff_and_self, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
a : ℕ
⊢ a ∣ n → a < n.succ → 1 ≤ a

Tactic:
fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Premises used: Iff.mpr, Nat.pos_of_dvd_of_pos, Nat.succ_le_iff, Ne.bot_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
a : ℕ
⊢ a ∣ n → a < n.succ → 1 ≤ a

Tactic:
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Premises used: Iff.mpr, Nat.pos_of_dvd_of_pos, Nat.succ_le_iff, Ne.bot_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
h₁ : ∀ (a : ℕ), a ∈ {d ∈ range n | d ∣ n} ↔ a ∈ n.properDivisors
⊢ {d ∈ range n | d ∣ n} = n.properDivisors

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
a : ℕ
h₁ : a ∣ n → a < n → 1 ≤ a
⊢ a ∈ {d ∈ range n | d ∣ n} ↔ a ∈ n.properDivisors

Tactic:
simp only [properDivisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]

Premises used: Finset.mem_range, Nat.properDivisors, and_congr_left_iff, Finset.mem_filter, iff_and_self, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
a : ℕ
⊢ a ∣ n → a < n → 1 ≤ a

Tactic:
fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Premises used: Iff.mpr, Nat.pos_of_dvd_of_pos, Nat.succ_le_iff, Ne.bot_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
a : ℕ
⊢ a ∣ n → a < n → 1 ≤ a

Tactic:
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Premises used: Iff.mpr, Nat.pos_of_dvd_of_pos, Nat.succ_le_iff, Ne.bot_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n ∉ n.properDivisors

Tactic:
simp [properDivisors]

Premises used: Nat.properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
inl : n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0
inr : ∀ (hm : m ≠ 0), n ∈ m.properDivisors ↔ n ∣ m ∧ n < m
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0

Tactic:
simp [properDivisors]

Premises used: Nat.properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m

Tactic:
simp only [and_comm, ← filter_dvd_eq_properDivisors hm, mem_filter, mem_range]

Premises used: Finset.mem_range, and_comm, Nat.filter_dvd_eq_properDivisors, Finset.mem_filter
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
rw : insert n n.properDivisors = {d ∈ Ico 1 (n + 1) | d ∣ n}
rw₁ : insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ Ico 1 (n + 1) | d ∣ n}
rw₂ : insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ insert n (Ico 1 n) | d ∣ n}
rw₃ : insert n ({d ∈ Ico 1 n | d ∣ n}) = if n ∣ n then insert n ({d ∈ Ico 1 n | d ∣ n}) else {d ∈ Ico 1 n | d ∣ n}
rw₄ rw₅ : insert n ({d ∈ Ico 1 n | d ∣ n}) = insert n ({d ∈ Ico 1 n | d ∣ n})
⊢ insert n n.properDivisors = n.divisors

Tactic:
rw [divisors, properDivisors,
    ← Finset.insert_Ico_right_eq_Ico_add_one (one_le_iff_ne_zero.2 h),
    Finset.filter_insert, if_pos (dvd_refl n)]

Premises used: Iff.mpr, if_pos, Nat.properDivisors, Nat.divisors, Finset.insert_Ico_right_eq_Ico_add_one, Finset.filter_insert, Nat.one_le_iff_ne_zero, dvd_refl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
rw : insert n n.properDivisors = n.divisors
rw₁ rw₂ : n.divisors = n.divisors
⊢ cons n n.properDivisors ⋯ = n.divisors

Tactic:
rw [cons_eq_insert, insert_self_properDivisors h]

Premises used: Finset.cons_eq_insert, Nat.insert_self_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
inl : n ∈ divisors 0 ↔ n ∣ 0 ∧ Ne (α := ℕ) 0 0
inr : ∀ (hm : m ≠ 0), n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ Ne (α := ℕ) 0 0

Tactic:
simp [divisors]

Premises used: Nat.divisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hm : m ≠ 0
inr : n ∣ m → n ≤ m
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

Tactic:
simp only [hm, Ne, not_false_iff, and_true, ← filter_dvd_eq_divisors hm, mem_filter,
    mem_range, and_iff_right_iff_imp, Nat.lt_succ_iff]

Premises used: and_true, Ne, Finset.mem_range, Nat.lt_succ_iff, Nat.filter_dvd_eq_divisors, and_iff_right_iff_imp, Finset.mem_filter, not_false_iff
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hm : m ≠ 0
⊢ n ∣ m → n ≤ m

Tactic:
le_of_dvd hm.bot_lt

Premises used: Nat.le_of_dvd, Ne.bot_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hm : m ≠ 0
⊢ n ∣ m → n ≤ m

Tactic:
exact le_of_dvd hm.bot_lt

Premises used: Nat.le_of_dvd, Ne.bot_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
h : n ∈ m.divisors
⊢ n ∣ m

Tactic:
(mem_divisors.mp h).1

Premises used: Nat.mem_divisors, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
h : n ∈ m.divisors
⊢ m ≠ 0

Tactic:
(mem_divisors.mp h).2

Premises used: Nat.mem_divisors, And.right, Iff.mp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ 1 ∈ n.divisors ↔ n ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n ≠ 0
⊢ n ∈ n.divisors

Tactic:
mem_divisors.2 ⟨dvd_rfl, h⟩

Premises used: Iff.mpr, Nat.mem_divisors, And.intro, dvd_rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
x : ℕ × ℕ
obtain : ∀ (a b : ℕ), (a, b) ∈ n.divisorsAntidiagonal ↔ (a, b).1 * (a, b).2 = n ∧ n ≠ 0
⊢ x ∈ n.divisorsAntidiagonal ↔ x.1 * x.2 = n ∧ n ≠ 0

Tactic:
obtain ⟨a, b⟩ := x
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n a b : ℕ
simp : a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b ↔ a * b = n ∧ n ≠ 0
⊢ (a, b) ∈ n.divisorsAntidiagonal ↔ (a, b).1 * (a, b).2 = n ∧ n ≠ 0

Tactic:
simp only [divisorsAntidiagonal, mul_div_eq_iff_dvd, mem_filterMap, mem_Icc, one_le_iff_ne_zero,
    Option.ite_none_right_eq_some, Option.some.injEq, Prod.ext_iff, and_left_comm, exists_eq_left]

Premises used: Nat.divisorsAntidiagonal, Option.some.injEq, Finset.mem_Icc, Prod.ext_iff, Finset.mem_filterMap, and_left_comm, exists_eq_left, Nat.mul_div_eq_iff_dvd, Nat.one_le_iff_ne_zero, Option.ite_none_right_eq_some
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n a b : ℕ
mp : a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b → a * b = n ∧ n ≠ 0
mpr : a * b = n ∧ n ≠ 0 → a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b ↔ a * b = n ∧ n ≠ 0

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n a : ℕ
han : a ∣ n
ha : a ≠ 0
han' : a ≤ n
mp : ¬n = 0
⊢ a * (n / a) = n ∧ n ≠ 0

Tactic:
simp [Nat.mul_div_eq_iff_dvd, han]

Premises used: Nat.mul_div_eq_iff_dvd
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n a : ℕ
han : a ∣ n
ha : a ≠ 0
han' : a ≤ n
⊢ ¬n = 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a b : ℕ
hab : a * b ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
rw [mul_ne_zero_iff] at hab

Premises used: mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a b : ℕ
hab : a ≠ 0 ∧ b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b

Tactic:
simpa [hab.1, hab.2] using Nat.le_mul_of_pos_right _ hab.2.bot_lt

Premises used: Nat.le_mul_of_pos_right, And.right, And.left, Ne.bot_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ divisorsAntidiagonalList 0 = []

Tactic:
rfl

Premises used: Nat.divisorsAntidiagonalList, List.filterMap, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ divisorsAntidiagonalList 1 = [(1, 1)]

Tactic:
rfl

Premises used: Nat.divisorsAntidiagonalList, List.filterMap, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ ∀ (a a' : ℕ) (b : ℕ × ℕ),
    (have y := n / a;
        if a * y = n then some (a, y) else none) =
        some b →
      (have y := n / a';
          if a' * y = n then some (a', y) else none) =
          some b →
        a = a'

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
rw :
  List.toFinset
      (List.filterMap
        (fun (x : ℕ) ↦
          have y := n / x;
          if x * y = n then some (x, y) else none)
        (List.range' 1 n)) =
    n.divisorsAntidiagonal
rw₁ :
  List.toFinset
      (List.filterMap
        (fun (x : ℕ) ↦
          have y := n / x;
          if x * y = n then some (x, y) else none)
        (List.range' 1 n)) =
    filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Icc 1 n) ⋯
rw₂ :
  filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (List.range' 1 n).toFinset ⋯ =
    filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Icc 1 n) ⋯
rw₃ rw₄ :
  filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Icc 1 n) ⋯ =
    filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Icc 1 n) ⋯
⊢ n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal

Tactic:
rw [divisorsAntidiagonalList, divisorsAntidiagonal, List.toFinset_filterMap
    (f_inj := by simp_all), List.toFinset_range'_1_1]

Premises used: Nat.divisorsAntidiagonalList, Nat.divisorsAntidiagonal, List.toFinset_range'_1_1, List.toFinset_filterMap
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.1 < x2.1) n.divisorsAntidiagonalList

Tactic:
(List.sortedLT_range' _ _ Nat.one_ne_zero).pairwise.filterMap _ fun a b c d h ha h' => ?_

Premises used: Nat.divisorsAntidiagonalList, List.SortedLT.pairwise, Nat.one_ne_zero, List.Pairwise.filterMap, List.sortedLT_range'
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
refine :
  ∀ (a b : ℕ) (c : a < b) (d : ℕ × ℕ)
    (h :
      (have y := n / a;
        if a * y = n then some (a, y) else none) =
        some d)
    (ha : ℕ × ℕ)
    (h' :
      (have y := n / b;
        if b * y = n then some (b, y) else none) =
        some ha),
    d.1 < ha.1
⊢ List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.1 < x2.1) n.divisorsAntidiagonalList

Tactic:
refine (List.sortedLT_range' _ _ Nat.one_ne_zero).pairwise.filterMap _ fun a b c d h ha h' => ?_

Premises used: List.SortedLT.pairwise, Nat.one_ne_zero, List.Pairwise.filterMap, List.sortedLT_range'