internlm/Lean-Github huggingface dataset:
Theorem: Hilbert90_integral
Proof state before:
case intro.intro.intro.intro.intro.refine_2
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = 0
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
e : σ (IsLocalization.mk' L x y) = 0
⊢ False
Tactic:
rw [hε, Algebra.norm_zero] at hη
Proof state after:
case intro.intro.intro.intro.intro.refine_2
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : 0 = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = 0
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
e : σ (IsLocalization.mk' L x y) = 0
⊢ False
Theorem: Hilbert90_integral
Proof state before:
case intro.intro.intro.intro.intro.refine_2
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : 0 = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = 0
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
e : σ (IsLocalization.mk' L x y) = 0
⊢ False
Tactic:
exact zero_ne_one hη
Proof state after:
no goals
Theorem: FltRegular.MayAssume.p_ne_three
Proof state before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
⊢ n ≠ 3
Tactic:
intro hn
Proof state after:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
⊢ False
Theorem: FltRegular.MayAssume.p_ne_three
Proof state before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
⊢ False
Tactic:
have ha : a ≠ 0 := fun ha => by simp [ha] at hprod
Proof state after:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
⊢ False
Theorem: FltRegular.MayAssume.p_ne_three
Proof state before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
⊢ False
Tactic:
have hb : b ≠ 0 := fun hb => by simp [hb] at hprod
Proof state after:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
⊢ False
Theorem: FltRegular.MayAssume.p_ne_three
Proof state before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
⊢ False
Tactic:
have hc : c ≠ 0 := fun hc => by simp [hc] at hprod
Proof state after:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ False
Theorem: FltRegular.MayAssume.p_ne_three
Proof state before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ False
Tactic:
simp [hn, flt_three a b c ha hb hc] at h
Proof state after:
no goals
Theorem: FltRegular.MayAssume.p_ne_three
Proof state before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a = 0
⊢ False
Tactic:
simp [ha] at hprod
Proof state after:
no goals
Theorem: FltRegular.MayAssume.p_ne_three
Proof state before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b = 0
⊢ False
Tactic:
simp [hb] at hprod
Proof state after:
no goals
Theorem: FltRegular.MayAssume.p_ne_three
Proof state before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
hc : c = 0
⊢ False
Tactic:
simp [hc] at hprod
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have ha : a ≠ 0 := fun ha => by simp [ha] at hprod
Proof state after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hb : b ≠ 0 := fun hb => by simp [hb] at hprod
Proof state after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hc : c ≠ 0 := fun hc => by simp [hc] at hprod
Proof state after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
let s : Finset ℤ := {a, b, c}
Proof state after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
set d : ℤ := s.gcd id
Proof state after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hadiv : d ∣ a := gcd_dvd (by simp [s])
Proof state after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hbdiv : d ∣ b := gcd_dvd (by simp [s])
Proof state after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hcdiv : d ∣ c := gcd_dvd (by simp [s])
Proof state after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hdzero : d ≠ 0 := fun hdzero => by
  simpa [ha] using Finset.gcd_eq_zero_iff.1 hdzero a (by simp [s])
Proof state after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hdp : d ^ n ≠ 0 := fun hdn => hdzero (pow_eq_zero hdn)
Proof state after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
refine' ⟨_, _, fun habs => _⟩
Proof state after:
case refine'_1
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n

case refine'_2
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ {a / d, b / d, c / d}.gcd id = 1

case refine'_3
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
habs : a / d * (b / d) * (c / d) = 0
⊢ False
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a = 0
⊢ False
Tactic:
simp [ha] at hprod
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b = 0
⊢ False
Tactic:
simp [hb] at hprod
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c = 0
⊢ False
Tactic:
simp [hc] at hprod
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
⊢ a ∈ s
Tactic:
simp [s]
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
⊢ b ∈ s
Tactic:
simp [s]
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
⊢ c ∈ s
Tactic:
simp [s]
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d = 0
⊢ False
Tactic:
simpa [ha] using Finset.gcd_eq_zero_iff.1 hdzero a (by simp [s])
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d = 0
⊢ a ∈ s
Tactic:
simp [s]
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
case refine'_1
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Tactic:
obtain ⟨na, hna⟩ := hadiv
Proof state after:
case refine'_1.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Theorem: FltRegular.MayAssume.coprime
Proof state before:
case refine'_1.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Tactic:
obtain ⟨nb, hnb⟩ := hbdiv
Proof state after:
case refine'_1.intro.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
nb : ℤ
hnb : b = d * nb
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Theorem: FltRegular.MayAssume.coprime
Proof state before:
case refine'_1.intro.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
nb : ℤ
hnb : b = d * nb
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Tactic:
obtain ⟨nc, hnc⟩ := hcdiv
Proof state after:
case refine'_1.intro.intro.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
nb : ℤ
hnb : b = d * nb
nc : ℤ
hnc : c = d * nc
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Theorem: FltRegular.MayAssume.coprime
Proof state before:
case refine'_1.intro.intro.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
nb : ℤ
hnb : b = d * nb
nc : ℤ
hnc : c = d * nc
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Tactic:
rwa [← mul_left_inj' hdp, add_mul, ← mul_pow, ← mul_pow, ← mul_pow, hna, hnb, hnc,
  Int.mul_ediv_cancel_left _ hdzero, Int.mul_ediv_cancel_left _ hdzero,
  Int.mul_ediv_cancel_left _ hdzero, mul_comm, ← hna, mul_comm, ← hnb, mul_comm, ← hnc]
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
case refine'_2
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ {a / d, b / d, c / d}.gcd id = 1
Tactic:
simpa [gcd_eq_gcd_image, d] using
  Finset.gcd_div_id_eq_one (show a ∈ ({a, b, c} : Finset ℤ) by simp) ha
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ a ∈ {a, b, c}
Tactic:
simp
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
case refine'_3
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
habs : a / d * (b / d) * (c / d) = 0
⊢ False
Tactic:
simp only [mul_eq_zero] at habs
Proof state after:
case refine'_3
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
habs : (a / d = 0 ∨ b / d = 0) ∨ c / d = 0
⊢ False
Theorem: FltRegular.MayAssume.coprime
Proof state before:
case refine'_3
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
habs : (a / d = 0 ∨ b / d = 0) ∨ c / d = 0
⊢ False
Tactic:
rcases habs with ((Ha | Hb) | Hc)
Proof state after:
case refine'_3.inl.inl
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Ha : a / d = 0
⊢ False

case refine'_3.inl.inr
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hb : b / d = 0
⊢ False

case refine'_3.inr
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hc : c / d = 0
⊢ False
Theorem: FltRegular.MayAssume.coprime
Proof state before:
case refine'_3.inl.inl
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Ha : a / d = 0
⊢ False
Tactic:
exact ha (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Ha)
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Ha : a / d = 0
⊢ a ∈ s
Tactic:
simp [s]
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
case refine'_3.inl.inr
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hb : b / d = 0
⊢ False
Tactic:
exact hb (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Hb)
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hb : b / d = 0
⊢ b ∈ s
Tactic:
simp [s]
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
case refine'_3.inr
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hc : c / d = 0
⊢ False
Tactic:
exact hc (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Hc)
Proof state after:
no goals
Theorem: FltRegular.MayAssume.coprime
Proof state before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hc : c / d = 0
⊢ c ∈ s
Tactic:
simp [s]
Proof state after:
no goals
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
h : a ^ p + b ^ p = c ^ p
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
⊢ ↑p ∣ c
Tactic:
letI : Fact p.Prime := ⟨hpri⟩
Proof state after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
h : a ^ p + b ^ p = c ^ p
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
⊢ ↑p ∣ c
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
h : a ^ p + b ^ p = c ^ p
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
⊢ ↑p ∣ c
Tactic:
replace h := congr_arg (fun n : ℤ => (n : ZMod p)) h
Proof state after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : (fun n => ↑n) (a ^ p + b ^ p) = (fun n => ↑n) (c ^ p)
⊢ ↑p ∣ c