Theorem: aux_lem_flt (FltRegular/NumberTheory/Cyclotomic/CyclRat.lean)

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
⊢ ¬↑↑p ∣ x + y
Tactic:
intro habs
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑↑p ∣ x + y
⊢ False

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑↑p ∣ x + y
⊢ False
Tactic:
rw [← ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_add] at habs
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
⊢ False

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
⊢ False
Tactic:
replace H := congr_arg (fun x : ℤ => (x : ZMod p)) H.symm
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : (fun x => ↑x) (z ^ ↑p) = (fun x => ↑x) (x ^ ↑p + y ^ ↑p)
⊢ False

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : (fun x => ↑x) (z ^ ↑p) = (fun x => ↑x) (x ^ ↑p + y ^ ↑p)
⊢ False
Tactic:
simp only [Int.cast_add, Int.cast_pow, ZMod.pow_card, habs,
  ZMod.intCast_zmod_eq_zero_iff_dvd] at H
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : ↑↑p ∣ z
⊢ False

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : ↑↑p ∣ z
⊢ False
Tactic:
exact caseI (Dvd.dvd.mul_left H _)
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑↑p ∣ x + y
⊢ ↑↑p ∣ x + y
Tactic:
simpa using habs
State after:
no goals