awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I J : Ideal α
h : ∀ (x : α), x ∈ I ↔ x ∈ J
⊢ I = J

Tactic:
Submodule.ext h

Premises used: Submodule.ext
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
⊢ y * x ∈ I ↔ x ∈ I

Tactic:
⟨fun h => ?_, fun h => I.mul_mem_left y h⟩

Premises used: Iff.intro, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
refine : ∀ (h : y * x ∈ I), x ∈ I
⊢ y * x ∈ I ↔ x ∈ I

Tactic:
refine ⟨fun h => ?_, fun h => I.mul_mem_left y h⟩
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
obtain : ∀ (y' : α) (hy' : y' * y = 1), x ∈ I
⊢ x ∈ I

Tactic:
obtain ⟨y', hy'⟩ := hy.exists_left_inv

Premises used: IsUnit.exists_left_inv
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
⊢ y' * (y * x) ∈ I

Tactic:
have := I.mul_mem_left y' h
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : y' * (y * x) ∈ I
rwa : ∀ (this : y' * y * x ∈ I), x ∈ I
rwa₁ : ∀ (this : 1 * x ∈ I), x ∈ I
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : x ∈ I), x ∈ I
⊢ x ∈ I

Tactic:
rwa [← mul_assoc, hy', one_mul] at this

Premises used: mul_assoc, one_mul
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
a : α
ha : a ∈ I
n : ℕ
hn : 0 < n
⊢ ¬0 < Nat.zero

Tactic:
decide
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
rw : a ^ (n - m) * a ^ m ∈ I
⊢ a ^ n ∈ I

Tactic:
rw [← Nat.add_sub_of_le h, add_comm, pow_add]

Premises used: pow_add, Nat.add_sub_of_le, add_comm
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ (n - m) * a ^ m ∈ I

Tactic:
I.mul_mem_left _ ha

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ (n - m) * a ^ m ∈ I

Tactic:
exact I.mul_mem_left _ ha

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
β : Type v
F : Type w
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m m' : M
a b : R
h : Membership.mem (γ := Set R) {r : R | r • m = r • m'} a
h' : Membership.mem (γ := Set R) {r : R | r • m = r • m'} b
⊢ Membership.mem (γ := Set R) {r : R | r • m = r • m'} (a + b)

Tactic:
simpa [add_smul] using congr($h + $h')

Premises used: add_smul
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
β : Type v
F : Type w
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m m' : M
x x_1 : R
h : Membership.mem (γ := Set R) {r : R | r • m = r • m'} x_1
⊢ Membership.mem (γ := Set R) {r : R | r • m = r • m'} (x • x_1)

Tactic:
simpa [mul_smul] using congr(_ • $h)

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
β : Type v
F : Type w
a b : α
inst : CommSemiring α
I : Ideal α
⊢ I.IsTwoSided

Tactic:
⟨fun b ha ↦ mul_comm b _ ▸ I.smul_mem _ ha⟩

Premises used: Eq.rec, mul_comm, Ideal.IsTwoSided.mk, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α_1 : Type u
β : Type v
F : Type w
a b : α_1
inst : CommSemiring α_1
I_1 : Ideal α_1
α : Type u_1
inst_1 : CommRing α
I : Ideal α
⊢ I.IsTwoSided

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
x y : α
hy : IsUnit y
⊢ x * y ∈ I ↔ x ∈ I

Tactic:
mul_comm y x ▸ unit_mul_mem_iff_mem I hy

Premises used: Set.Mem, Eq.rec, Ideal.unit_mul_mem_iff_mem, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
a b : α
inst : CommSemiring α
I : Ideal α
hab : a ∣ b
ha : a ∈ I
obtain : ∀ (c : α), a * c ∈ I
⊢ b ∈ I

Tactic:
obtain ⟨c, rfl⟩ := hab

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
a : α
inst : CommSemiring α
I : Ideal α
ha : a ∈ I
c : α
⊢ a * c ∈ I

Tactic:
I.mul_mem_right _ ha

Premises used: Set.Mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
a : α
inst : CommSemiring α
I : Ideal α
ha : a ∈ I
c : α
⊢ a * c ∈ I

Tactic:
exact I.mul_mem_right _ ha

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Ring α
I : Ideal α
a : α
⊢ -a ∈ I ↔ a ∈ I

Tactic:
Submodule.neg_mem_iff I

Premises used: Set.Mem, Submodule.neg_mem_iff
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Ring α
I : Ideal α
a b : α
⊢ b ∈ I → (a + b ∈ I ↔ a ∈ I)

Tactic:
Submodule.add_mem_iff_left I

Premises used: Set.Mem, Submodule.add_mem_iff_left
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Ring α
I : Ideal α
a b : α
⊢ a ∈ I → (a + b ∈ I ↔ b ∈ I)

Tactic:
Submodule.add_mem_iff_right I

Premises used: Set.Mem, Submodule.add_mem_iff_right
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Ring α
I : Ideal α
a b : α
⊢ a ∈ I → b ∈ I → a - b ∈ I

Tactic:
Submodule.sub_mem I

Premises used: Set.Mem, Submodule.sub_mem
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Ring α
I : Ideal α
a b c d : α
inst_1 : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
rw : a * c - b * d = a * c - b * c + (b * c - b * d)
⊢ a * c - b * d = (a - b) * c + b * (c - d)

Tactic:
rw [sub_mul, mul_sub]

Premises used: mul_sub, sub_mul
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Ring α
I : Ideal α
a b c d : α
inst_1 : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + (b * c - b * d)

Tactic:
abel
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Ring α
I : Ideal α
a b c d : α
inst_1 : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
rw : (a - b) * c + b * (c - d) ∈ I
⊢ a * c - b * d ∈ I

Tactic:
rw [show a * c - b * d = (a - b) * c + b * (c - d) by rw [sub_mul, mul_sub]; abel]
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Ring α
I : Ideal α
a b c d : α
inst_1 : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ (a - b) * c + b * (c - d) ∈ I

Tactic:
I.add_mem (I.mul_mem_right _ h1) (I.mul_mem_left _ h2)

Premises used: Ideal.add_mem, Ideal.mul_mem_right, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Ring α
I : Ideal α
a b c d : α
inst_1 : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ (a - b) * c + b * (c - d) ∈ I

Tactic:
exact I.add_mem (I.mul_mem_right _ h1) (I.mul_mem_left _ h2)

Premises used: Ideal.add_mem, Ideal.mul_mem_right, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hle : p ≤ q
pos : ∀ (h : p = q), ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
neg : ∀ (h : ¬p = q), ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
by_cases h : p = q
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hle : p ≤ q
h : p = q
⊢ p.IsPrime

Tactic:
subst h
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hle : p ≤ q
h : p = q
inst : p.IsPrime
⊢ Q.LiesOver p

Tactic:
subst h
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hle : p ≤ q
h : p = q
inst : p.IsPrime
inst₁ : Q.LiesOver p
⊢ p ≤ p

Tactic:
subst h
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p : Ideal R
inst_4 : p.IsPrime
Q : Ideal S
inst_5 : Q.IsPrime
inst_6 : p.IsPrime
inst_7 : Q.LiesOver p
hle : p ≤ p
w : Ideal S
h : Q ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
use Q
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
⊢ q = under R Q

Tactic:
have := Q.over_def q
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
this : q = under R Q
⊢ IsPrime (under R Q)

Tactic:
subst this
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
this : q = under R Q
inst : IsPrime (under R Q)
⊢ Q.LiesOver (under R Q)

Tactic:
subst this
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
this : q = under R Q
inst : IsPrime (under R Q)
inst₁ : Q.LiesOver (under R Q)
⊢ p ≤ under R Q

Tactic:
subst this
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
this : q = under R Q
inst : IsPrime (under R Q)
inst₁ : Q.LiesOver (under R Q)
hle₁ : p ≤ under R Q
⊢ ¬p = under R Q

Tactic:
subst this
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p : Ideal R
inst_4 : p.IsPrime
Q : Ideal S
inst_5 : Q.IsPrime
inst_6 : IsPrime (under R Q)
inst_7 : Q.LiesOver (under R Q)
hle : p ≤ under R Q
h : ¬p = under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt Q (lt_of_le_of_ne hle h)

Premises used: Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p : Ideal R
inst_4 : p.IsPrime
Q : Ideal S
inst_5 : Q.IsPrime
inst_6 : IsPrime (under R Q)
inst_7 : Q.LiesOver (under R Q)
hle : p ≤ under R Q
h : ¬p = under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
exact Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt Q (lt_of_le_of_ne hle h)

Premises used: Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hpq : p < q
obtain : ∀ (P : Ideal S) (hPQ : P ≤ Q), P.IsPrime → P.LiesOver p → ∃ P < Q, P.IsPrime ∧ P.LiesOver p
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p

Tactic:
obtain ⟨P, hPQ, _, _⟩ := Q.exists_ideal_le_liesOver_of_le (p := p) (q := q) hpq.le

Premises used: Ideal.exists_ideal_le_liesOver_of_le, LT.lt.le
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p

Tactic:
⟨P, ?_, inferInstance, inferInstance⟩

Premises used: inferInstance, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
refine : P < Q
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p

Tactic:
refine ⟨P, ?_, inferInstance, inferInstance⟩
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
by_contra : ∀ (hc : ¬P < Q), False
⊢ P < Q

Tactic:
by_contra hc
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
hc : ¬P < Q
⊢ P = Q

Tactic:
have : P = Q := eq_of_le_of_not_lt hPQ hc
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
hc : ¬P < Q
this : P = Q
⊢ P.IsPrime

Tactic:
subst this
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
hc : ¬P < Q
this : P = Q
inst : P.IsPrime
⊢ P.LiesOver q

Tactic:
subst this
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
hc : ¬P < Q
this : P = Q
inst : P.IsPrime
inst₁ : P.LiesOver q
⊢ P ≤ P

Tactic:
subst this
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
hc : ¬P < Q
this : P = Q
inst : P.IsPrime
inst₁ : P.LiesOver q
hPQ₁ : P ≤ P
⊢ ¬P < P

Tactic:
subst this
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
hpq : p < q
P : Ideal S
left : P.IsPrime
right : P.LiesOver p
inst_6 : P.IsPrime
inst_7 : P.LiesOver q
hPQ : P ≤ P
hc : ¬P < P
⊢ False

Tactic:
simp [P.over_def p, P.over_def q] at hpq

Premises used: Ideal.over_def
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
q : PrimeSpectrum R
P : Ideal S
inst_4 : P.IsPrime
lo :
  P.LiesOver
    (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        (RelSeries.singleton
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}
          q)).asIdeal
h :
  PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S }) =
    q.asIdeal
⊢ PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S } = q

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
q : PrimeSpectrum R
P : Ideal S
inst_4 : P.IsPrime
lo :
  P.LiesOver
    (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        (RelSeries.singleton
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}
          q)).asIdeal
⊢ PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S }) =
    q.asIdeal

Tactic:
simpa using lo.over.symm

Premises used: Ideal.LiesOver.over, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
l :
  RelSeries (α := PrimeSpectrum R)
    {x : PrimeSpectrum R × PrimeSpectrum R |
      match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
      | (a, b) => a < b}
q : PrimeSpectrum R
lt :
  Membership.mem (γ := SetRel (PrimeSpectrum R) (PrimeSpectrum R))
    {x : PrimeSpectrum R × PrimeSpectrum R |
      match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
      | (a, b) => a < b}
    (q,
      l.head (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b}))
ih :
  ∀ (P : Ideal S) [inst_5 : P.IsPrime]
    [lo :
      P.LiesOver
        l.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b}).asIdeal],
    ∃ (L : LTSeries (PrimeSpectrum S)),
      L.length (r :=
            {x : PrimeSpectrum S × PrimeSpectrum S |
              match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
              | (a, b) => a < b}) =
          l.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b}) ∧
        RelSeries.last (r :=
              {x : PrimeSpectrum S × PrimeSpectrum S |
                match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
                | (a, b) => a < b})
              L =
            { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S))
              (RelSeries.toList (r :=
                {x : PrimeSpectrum S × PrimeSpectrum S |
                  match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
                  | (a, b) => a < b})
                L) =
            l.toList (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
P : Ideal S
inst_4 : P.IsPrime
lo :
  P.LiesOver
    (l.cons (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            q lt).last
        (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b}).asIdeal
⊢ P.LiesOver l.last (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2}).asIdeal

Tactic:
simp only [RelSeries.last_cons] at lo

Premises used: RelSeries.last_cons
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ HasGoingDown R S ↔
    GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))

Tactic:
⟨?_, fun h ↦ ⟨fun {p} hp Q hQ hlt ↦ ?_⟩⟩

Premises used: Algebra.HasGoingDown.mk, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
refine_1 :
  HasGoingDown R S →
    GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
refine_2 :
  ∀ (h : GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)))
    {p : Ideal R} (hp : p.IsPrime) (Q : Ideal S) (hQ : Q.IsPrime) (hlt : p < Ideal.under R Q),
    ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
⊢ HasGoingDown R S ↔
    GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))

Tactic:
refine ⟨?_, fun h ↦ ⟨fun {p} hp Q hQ hlt ↦ ?_⟩⟩
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ⤳ PrimeSpectrum.comap (algebraMap R S) Q
⊢ p ≤ PrimeSpectrum.comap (algebraMap R S) Q

Tactic:
rw [← PrimeSpectrum.le_iff_specializes] at hp

Premises used: PrimeSpectrum.le_iff_specializes
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
refine_1 :
  ∀ (P : Ideal S) (hle : P ≤ Q.asIdeal) (hP : P.IsPrime) (h : P.LiesOver p.asIdeal),
    ∃ (a' : PrimeSpectrum S),
      (fun (x1 x2 : PrimeSpectrum S) ↦ x1 ⤳ x2) a' Q ∧ PrimeSpectrum.comap (algebraMap R S) a' = p
⊢ ∃ (a' : PrimeSpectrum S), (fun (x1 x2 : PrimeSpectrum S) ↦ x1 ⤳ x2) a' Q ∧ PrimeSpectrum.comap (algebraMap R S) a' = p

Tactic:
obtain ⟨P, hle, hP, h⟩ := Q.asIdeal.exists_ideal_le_liesOver_of_le (p := p.asIdeal)
      (q := Q.asIdeal.under R) hp

Premises used: Ideal.exists_ideal_le_liesOver_of_le, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h_1 : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ ∃ (a' : PrimeSpectrum S), (fun (x1 x2 : PrimeSpectrum S) ↦ x1 ⤳ x2) a' Q ∧ PrimeSpectrum.comap (algebraMap R S) a' = p

Tactic:
⟨⟨P, hP⟩, (PrimeSpectrum.le_iff_specializes _ Q).mp hle, ?_⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.le_iff_specializes, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h_1 : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
refine_1 : PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP : PrimeSpectrum S } = p
⊢ ∃ (a' : PrimeSpectrum S), (fun (x1 x2 : PrimeSpectrum S) ↦ x1 ⤳ x2) a' Q ∧ PrimeSpectrum.comap (algebraMap R S) a' = p

Tactic:
refine ⟨⟨P, hP⟩, (PrimeSpectrum.le_iff_specializes _ Q).mp hle, ?_⟩