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

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ ¬IsCoprime a b ↔ a + b ≠ ⊤
Tactic:
apply not_congr
State after:
case h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ IsCoprime a b ↔ a + b = ⊤

State before:
case h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ IsCoprime a b ↔ a + b = ⊤
Tactic:
rw [IsCoprime]
State after:
case h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ (∃ a_1 b_1, a_1 * a + b_1 * b = 1) ↔ a + b = ⊤

State before:
case h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ (∃ a_1 b_1, a_1 * a + b_1 * b = 1) ↔ a + b = ⊤
Tactic:
constructor
State after:
case h.mp
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ (∃ a_1 b_1, a_1 * a + b_1 * b = 1) → a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1

State before:
case h.mp
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ (∃ a_1 b_1, a_1 * a + b_1 * b = 1) → a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
intro h
State after:
case h.mp
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : ∃ a_1 b_1, a_1 * a + b_1 * b = 1
⊢ a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1

State before:
case h.mp
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : ∃ a_1 b_1, a_1 * a + b_1 * b = 1
⊢ a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
obtain ⟨x, y, hxy⟩ := h
State after:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1

State before:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
rw [eq_top_iff_one]
State after:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ 1 ∈ a + b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1

State before:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ 1 ∈ a + b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
have h2 : x * a + y * b ≤ a + b := by apply Ideal.le_add; all_goals apply mul_le_left
State after:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ a + b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1

State before:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ a + b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
apply h2
State after:
case h.mp.intro.intro.a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ x * a + y * b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1

State before:
case h.mp.intro.intro.a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ x * a + y * b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
rw [hxy]
State after:
case h.mp.intro.intro.a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ 1

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1

State before:
case h.mp.intro.intro.a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ 1

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
simp
State after:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1

State before:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
intro h
State after:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ ∃ a_1 b_1, a_1 * a + b_1 * b = 1

State before:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ ∃ a_1 b_1, a_1 * a + b_1 * b = 1
Tactic:
refine' ⟨1, 1, _⟩
State after:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ 1 * a + 1 * b = 1

State before:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ 1 * a + 1 * b = 1
Tactic:
simp only [one_eq_top, top_mul, Submodule.add_eq_sup, ge_iff_le]
State after:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ a ⊔ b = ⊤

State before:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ a ⊔ b = ⊤
Tactic:
rw [← h]
State after:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ a ⊔ b = a + b

State before:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ a ⊔ b = a + b
Tactic:
rfl
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ x * a + y * b ≤ a + b
Tactic:
apply Ideal.le_add
State after:
case hab
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ x * a ≤ a

case hcd
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ y * b ≤ b

State before:
case hab
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ x * a ≤ a

case hcd
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ y * b ≤ b
Tactic:
all_goals apply mul_le_left
State after:
no goals

State before:
case hcd
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ y * b ≤ b
Tactic:
apply mul_le_left
State after:
no goals