internlm/Lean-Github huggingface dataset:
Theorem: descent
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ (a' * b' * c').natAbs ^ 3 < (a * b * c).natAbs ^ 3
Tactic:
convert lt_of_le_of_lt hsmaller haaa <;> simp [mul_pow, Int.natAbs_mul, Int.natAbs_pow]
Proof state after:
no goals
Theorem: descent
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
hgcd : (2 * p).gcd (p ^ 2 + 3 * q ^ 2) = 1
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
rw [Int.gcd_eq_one_iff_coprime] at hgcd
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.inl
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
apply descent_gcd1 a b c p q hp hcoprime hodd hcube hgcd
Proof state after:
no goals
Theorem: descent
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inr
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
hgcd : (2 * p).gcd (p ^ 2 + 3 * q ^ 2) = 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
apply descent_gcd3 a b c p q hp hq hcoprime hodd hcube hgcd
Proof state after:
no goals
Theorem: flt_three
Proof state before:
⊢ FermatLastTheoremWith ℤ 3
Tactic:
intros a b c ha hb hc
Proof state after:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
Theorem: flt_three
Proof state before:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
Tactic:
induction' h : (a * b * c).natAbs using Nat.strong_induction_on with k' IH generalizing a b c
Proof state after:
case h
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
Theorem: flt_three
Proof state before:
case h
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
Tactic:
intro H
Proof state after:
case h
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
⊢ False
Theorem: flt_three
Proof state before:
case h
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
⊢ False
Tactic:
obtain ⟨x'', y'', z'', hxle, hyle, hzle, hcoprime⟩ := exists_coprime zero_lt_three ha hb hc H
Proof state after:
case h.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
⊢ False
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
⊢ False
Tactic:
obtain ⟨x', y', z', hx'pos, hy'pos, hz'pos, hsmaller, hsolution⟩ := descent x'' y'' z'' hcoprime
Proof state after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : (x' * y' * z').natAbs < (x'' * y'' * z'').natAbs
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ False
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : (x' * y' * z').natAbs < (x'' * y'' * z'').natAbs
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ False
Tactic:
refine' IH (x' * y' * z').natAbs _ _ _ _ hx'pos hy'pos hz'pos rfl hsolution
Proof state after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : (x' * y' * z').natAbs < (x'' * y'' * z'').natAbs
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ (x' * y' * z').natAbs < k'
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : (x' * y' * z').natAbs < (x'' * y'' * z'').natAbs
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ (x' * y' * z').natAbs < k'
Tactic:
apply lt_of_lt_of_le hsmaller
Proof state after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : (x' * y' * z').natAbs < (x'' * y'' * z'').natAbs
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ (x'' * y'' * z'').natAbs ≤ k'
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : (x' * y' * z').natAbs < (x'' * y'' * z'').natAbs
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ (x'' * y'' * z'').natAbs ≤ k'
Tactic:
rw [← h]
Proof state after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : (x' * y' * z').natAbs < (x'' * y'' * z'').natAbs
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ (x'' * y'' * z'').natAbs ≤ (a * b * c).natAbs
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : (x' * y' * z').natAbs < (x'' * y'' * z'').natAbs
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ (x'' * y'' * z'').natAbs ≤ (a * b * c).natAbs
Tactic:
simp only [Int.natAbs_mul]
Proof state after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : (x' * y' * z').natAbs < (x'' * y'' * z'').natAbs
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ x''.natAbs * y''.natAbs * z''.natAbs ≤ a.natAbs * b.natAbs * c.natAbs
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : x''.natAbs ≤ a.natAbs
hyle : y''.natAbs ≤ b.natAbs
hzle : z''.natAbs ≤ c.natAbs
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : (x' * y' * z').natAbs < (x'' * y'' * z'').natAbs
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ x''.natAbs * y''.natAbs * z''.natAbs ≤ a.natAbs * b.natAbs * c.natAbs
Tactic:
exact Nat.mul_le_mul (Nat.mul_le_mul hxle hyle) hzle
Proof state after:
no goals
Theorem: systemOfUnits.nontrivial
Proof state before:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
⊢ Nontrivial G
Tactic:
by_contra! h
Proof state after:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : ¬Nontrivial G
⊢ False
Theorem: systemOfUnits.nontrivial
Proof state before:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : ¬Nontrivial G
⊢ False
Tactic:
rw [not_nontrivial_iff_subsingleton] at h
Proof state after:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : Subsingleton G
⊢ False
Theorem: systemOfUnits.nontrivial
Proof state before:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : Subsingleton G
⊢ False
Tactic:
rw [FiniteDimensional.finrank_zero_of_subsingleton] at hf
Proof state after:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : 0 = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : Subsingleton G
⊢ False
Theorem: systemOfUnits.nontrivial
Proof state before:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : 0 = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : Subsingleton G
⊢ False
Tactic:
simp only [ge_iff_le, zero_eq_mul, tsub_eq_zero_iff_le] at hf
Proof state after:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : Subsingleton G
hf : r = 0 ∨ ↑p ≤ 1
⊢ False
Theorem: systemOfUnits.nontrivial
Proof state before:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : Subsingleton G
hf : r = 0 ∨ ↑p ≤ 1
⊢ False
Tactic:
cases hf with
| inl h => exact hr h
| inr h => simpa [Nat.lt_succ_iff, h] using not_lt.2 (Nat.prime_def_lt.1 hp).1
Proof state after:
no goals
Theorem: systemOfUnits.nontrivial
Proof state before:
case inl
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h✝ : Subsingleton G
h : r = 0
⊢ False
Tactic:
exact hr h
Proof state after:
no goals
Theorem: systemOfUnits.nontrivial
Proof state before:
case inr
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h✝ : Subsingleton G
h : ↑p ≤ 1
⊢ False
Tactic:
simpa [Nat.lt_succ_iff, h] using not_lt.2 (Nat.prime_def_lt.1 hp).1
Proof state after:
no goals
Theorem: systemOfUnits.existence0
Proof state before:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
⊢ Nonempty (systemOfUnits p G 0)
Tactic:
exact ⟨⟨fun _ => 0, linearIndependent_empty_type⟩⟩
Proof state after:
no goals
Theorem: systemOfUnits.spanA_eq_spanZ
Proof state before:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
⊢ Submodule.restrictScalars ℤ (Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    Submodule.span ℤ (Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1)
Tactic:
letI := Fact.mk hp
Proof state after:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ Submodule.restrictScalars ℤ (Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    Submodule.span ℤ (Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1)
Theorem: systemOfUnits.spanA_eq_spanZ
Proof state before:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ Submodule.restrictScalars ℤ (Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    Submodule.span ℤ (Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1)
Tactic:
rw [← Submodule.span_smul_of_span_eq_top (CyclotomicIntegers.powerBasis p).basis.span_eq,
  Set.range_smul_range]
Proof state after:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ Submodule.span ℤ (Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) =
    Submodule.span ℤ (Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1)
Theorem: systemOfUnits.spanA_eq_spanZ
Proof state before:
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ Submodule.span ℤ (Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) =
    Submodule.span ℤ (Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1)
Tactic:
congr
Proof state after:
case e_s
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ (Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) =
    Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1
Theorem: systemOfUnits.spanA_eq_spanZ
Proof state before:
case e_s
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ (Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) =
    Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1
Tactic:
ext
Proof state after:
case e_s.h
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
x✝ : G
⊢ (x✝ ∈ Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) ↔
    x✝ ∈ Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1
Theorem: systemOfUnits.spanA_eq_spanZ
Proof state before:
case e_s.h
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
x✝ : G
⊢ (x✝ ∈ Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) ↔
    x✝ ∈ Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1
Tactic:
simp only [PowerBasis.coe_basis, CyclotomicIntegers.powerBasis_gen, Set.mem_range, Prod.exists]
Proof state after:
case e_s.h
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
x✝ : G
⊢ (∃ a b, zeta ↑p ^ ↑a • f b = x✝) ↔ ∃ a b, zeta ↑p ^ ↑b • f a = x✝
Theorem: systemOfUnits.spanA_eq_spanZ
Proof state before:
case e_s.h
p : ℕ+
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁴ : Field k
inst✝³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝² : AddCommGroup G
r : ℕ
inst✝¹ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
x✝ : G
⊢ (∃ a b, zeta ↑p ^ ↑a • f b = x✝) ↔ ∃ a b, zeta ↑p ^ ↑b • f a = x✝
Tactic:
rw [exists_comm, CyclotomicIntegers.powerBasis_dim]
Proof state after:
no goals