[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R_hat R K
⊢ ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) }
      (x + y) =
    ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) } x +
      ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) } y
[PROOFSTEP]
refine funext fun v => ?_
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : R_hat R K
v : HeightOneSpectrum R
⊢ ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) } (x + y)
      v =
    (ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) } x +
        ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) }
          y)
      v
[PROOFSTEP]
simp only [coe_apply, Pi.add_apply, Subring.coe_add]
  -- Porting note: added
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : R_hat R K
v : HeightOneSpectrum R
⊢ ↑((x + y) v) = ((fun v => ↑(x v)) + fun v => ↑(y v)) v
[PROOFSTEP]
erw [Pi.add_apply, Pi.add_apply, Subring.coe_add]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
src✝ : R_hat R K →+ K_hat R K := addMonoidHom R K
x y : R_hat R K
⊢ OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } (x * y) =
    OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } x *
      OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } y
[PROOFSTEP]
refine funext fun p => ?_
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
src✝ : R_hat R K →+ K_hat R K := addMonoidHom R K
x y : R_hat R K
p : HeightOneSpectrum R
⊢ OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } (x * y)
      p =
    (OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } x *
        OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } y)
      p
[PROOFSTEP]
simp only [Pi.mul_apply, Subring.coe_mul]
  -- Porting note: added
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
src✝ : R_hat R K →+ K_hat R K := addMonoidHom R K
x y : R_hat R K
p : HeightOneSpectrum R
⊢ ↑((x * y) p) = ((fun v => ↑(x v)) * fun v => ↑(y v)) p
[PROOFSTEP]
erw [Pi.mul_apply, Pi.mul_apply, Subring.coe_mul]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Algebra K ((v : HeightOneSpectrum R) → HeightOneSpectrum.adicCompletion K v)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Algebra R ((v : HeightOneSpectrum R) → HeightOneSpectrum.adicCompletion K v)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsScalarTower R K ((v : HeightOneSpectrum R) → HeightOneSpectrum.adicCompletion K v)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Algebra R ((v : HeightOneSpectrum R) → { x // x ∈ adicCompletionIntegers K v })
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsScalarTower R ((v : HeightOneSpectrum R) → { x // x ∈ adicCompletionIntegers K v })
    ((v : HeightOneSpectrum R) → HeightOneSpectrum.adicCompletion K v)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : IsFiniteAdele x
hy : IsFiniteAdele y
⊢ IsFiniteAdele (x + y)
[PROOFSTEP]
rw [IsFiniteAdele, Filter.eventually_cofinite] at hx hy ⊢
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
⊢ Set.Finite {x_1 | ¬(x + y) x_1 ∈ adicCompletionIntegers K x_1}
[PROOFSTEP]
have h_subset :
  {v : HeightOneSpectrum R | ¬(x + y) v ∈ v.adicCompletionIntegers K} ⊆
    {v : HeightOneSpectrum R | ¬x v ∈ v.adicCompletionIntegers K} ∪
      {v : HeightOneSpectrum R | ¬y v ∈ v.adicCompletionIntegers K} :=
  by
  intro v hv
  rw [mem_union, mem_setOf, mem_setOf]
  rw [mem_setOf] at hv
  contrapose! hv
  rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, ← max_le_iff] at hv
  rw [mem_adicCompletionIntegers, Pi.add_apply]
  exact le_trans (Valued.v.map_add_le_max' (x v) (y v)) hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
⊢ {v | ¬(x + y) v ∈ adicCompletionIntegers K v} ⊆
    {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
[PROOFSTEP]
intro v hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : v ∈ {v | ¬(x + y) v ∈ adicCompletionIntegers K v}
⊢ v ∈ {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
[PROOFSTEP]
rw [mem_union, mem_setOf, mem_setOf]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : v ∈ {v | ¬(x + y) v ∈ adicCompletionIntegers K v}
⊢ ¬x v ∈ adicCompletionIntegers K v ∨ ¬y v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_setOf] at hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : ¬(x + y) v ∈ adicCompletionIntegers K v
⊢ ¬x v ∈ adicCompletionIntegers K v ∨ ¬y v ∈ adicCompletionIntegers K v
[PROOFSTEP]
contrapose! hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : x v ∈ adicCompletionIntegers K v ∧ y v ∈ adicCompletionIntegers K v
⊢ (x + y) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, ← max_le_iff] at hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : max (↑Valued.v (x v)) (↑Valued.v (y v)) ≤ 1
⊢ (x + y) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, Pi.add_apply]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : max (↑Valued.v (x v)) (↑Valued.v (y v)) ≤ 1
⊢ ↑Valued.v (x v + y v) ≤ 1
[PROOFSTEP]
exact le_trans (Valued.v.map_add_le_max' (x v) (y v)) hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
h_subset :
  {v | ¬(x + y) v ∈ adicCompletionIntegers K v} ⊆
    {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
⊢ Set.Finite {x_1 | ¬(x + y) x_1 ∈ adicCompletionIntegers K x_1}
[PROOFSTEP]
exact (hx.union hy).subset h_subset
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsFiniteAdele 0
[PROOFSTEP]
rw [IsFiniteAdele, Filter.eventually_cofinite]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Set.Finite {x | ¬OfNat.ofNat 0 x ∈ adicCompletionIntegers K x}
[PROOFSTEP]
have h_empty : {v : HeightOneSpectrum R | ¬(0 : v.adicCompletion K) ∈ v.adicCompletionIntegers K} = ∅ :=
  by
  ext v; rw [mem_empty_iff_false, iff_false_iff]; intro hv
  rw [mem_setOf] at hv ; apply hv; rw [mem_adicCompletionIntegers]
  have h_zero : (Valued.v (0 : v.adicCompletion K) : WithZero (Multiplicative ℤ)) = 0 := Valued.v.map_zero'
  rw [h_zero];
  exact
    zero_le_one'
      _
        -- Porting note: was `exact`, but `OfNat` got in the way.
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ {v | ¬0 ∈ adicCompletionIntegers K v} = ∅
[PROOFSTEP]
ext v
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
⊢ v ∈ {v | ¬0 ∈ adicCompletionIntegers K v} ↔ v ∈ ∅
[PROOFSTEP]
rw [mem_empty_iff_false, iff_false_iff]
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
⊢ ¬v ∈ {v | ¬0 ∈ adicCompletionIntegers K v}
[PROOFSTEP]
intro hv
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : v ∈ {v | ¬0 ∈ adicCompletionIntegers K v}
⊢ False
[PROOFSTEP]
rw [mem_setOf] at hv
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬0 ∈ adicCompletionIntegers K v
⊢ False
[PROOFSTEP]
apply hv
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬0 ∈ adicCompletionIntegers K v
⊢ 0 ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers]
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬0 ∈ adicCompletionIntegers K v
⊢ ↑Valued.v 0 ≤ 1
[PROOFSTEP]
have h_zero : (Valued.v (0 : v.adicCompletion K) : WithZero (Multiplicative ℤ)) = 0 := Valued.v.map_zero'
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬0 ∈ adicCompletionIntegers K v
h_zero : ↑Valued.v 0 = 0
⊢ ↑Valued.v 0 ≤ 1
[PROOFSTEP]
rw [h_zero]
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬0 ∈ adicCompletionIntegers K v
h_zero : ↑Valued.v 0 = 0
⊢ 0 ≤ 1
[PROOFSTEP]
exact
  zero_le_one'
    _
      -- Porting note: was `exact`, but `OfNat` got in the way.
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
h_empty : {v | ¬0 ∈ adicCompletionIntegers K v} = ∅
⊢ Set.Finite {x | ¬OfNat.ofNat 0 x ∈ adicCompletionIntegers K x}
[PROOFSTEP]
convert finite_empty
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K_hat R K
hx : IsFiniteAdele x
⊢ IsFiniteAdele (-x)
[PROOFSTEP]
rw [IsFiniteAdele] at hx ⊢
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, (-x) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
have h : ∀ v : HeightOneSpectrum R, -x v ∈ v.adicCompletionIntegers K ↔ x v ∈ v.adicCompletionIntegers K :=
  by
  intro v
  rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, Valuation.map_neg]
    -- Porting note: was `simpa only [Pi.neg_apply, h] using hx` but `Pi.neg_apply` no longer works
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
⊢ ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
[PROOFSTEP]
intro v
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
v : HeightOneSpectrum R
⊢ -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, Valuation.map_neg]
  -- Porting note: was `simpa only [Pi.neg_apply, h] using hx` but `Pi.neg_apply` no longer works
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
h : ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, (-x) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
convert hx using 2 with v
[GOAL]
case h.e'_2.h.a
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
h : ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
v : HeightOneSpectrum R
⊢ (-x) v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
[PROOFSTEP]
convert h v
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : IsFiniteAdele x
hy : IsFiniteAdele y
⊢ IsFiniteAdele (x * y)
[PROOFSTEP]
rw [IsFiniteAdele, Filter.eventually_cofinite] at hx hy ⊢
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
⊢ Set.Finite {x_1 | ¬(x * y) x_1 ∈ adicCompletionIntegers K x_1}
[PROOFSTEP]
have h_subset :
  {v : HeightOneSpectrum R | ¬(x * y) v ∈ v.adicCompletionIntegers K} ⊆
    {v : HeightOneSpectrum R | ¬x v ∈ v.adicCompletionIntegers K} ∪
      {v : HeightOneSpectrum R | ¬y v ∈ v.adicCompletionIntegers K} :=
  by
  intro v hv
  rw [mem_union, mem_setOf, mem_setOf]
  rw [mem_setOf] at hv
  contrapose! hv
  rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers] at hv
  have h_mul : Valued.v (x v * y v) = Valued.v (x v) * Valued.v (y v) := Valued.v.map_mul' (x v) (y v)
  rw [mem_adicCompletionIntegers, Pi.mul_apply, h_mul]
  exact @mul_le_one' (WithZero (Multiplicative ℤ)) _ _ (OrderedCommMonoid.to_covariantClass_left _) _ _ hv.left hv.right
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
⊢ {v | ¬(x * y) v ∈ adicCompletionIntegers K v} ⊆
    {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
[PROOFSTEP]
intro v hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : v ∈ {v | ¬(x * y) v ∈ adicCompletionIntegers K v}
⊢ v ∈ {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
[PROOFSTEP]
rw [mem_union, mem_setOf, mem_setOf]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : v ∈ {v | ¬(x * y) v ∈ adicCompletionIntegers K v}
⊢ ¬x v ∈ adicCompletionIntegers K v ∨ ¬y v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_setOf] at hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : ¬(x * y) v ∈ adicCompletionIntegers K v
⊢ ¬x v ∈ adicCompletionIntegers K v ∨ ¬y v ∈ adicCompletionIntegers K v
[PROOFSTEP]
contrapose! hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : x v ∈ adicCompletionIntegers K v ∧ y v ∈ adicCompletionIntegers K v
⊢ (x * y) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers] at hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : ↑Valued.v (x v) ≤ 1 ∧ ↑Valued.v (y v) ≤ 1
⊢ (x * y) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
have h_mul : Valued.v (x v * y v) = Valued.v (x v) * Valued.v (y v) := Valued.v.map_mul' (x v) (y v)
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : ↑Valued.v (x v) ≤ 1 ∧ ↑Valued.v (y v) ≤ 1
h_mul : ↑Valued.v (x v * y v) = ↑Valued.v (x v) * ↑Valued.v (y v)
⊢ (x * y) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, Pi.mul_apply, h_mul]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : ↑Valued.v (x v) ≤ 1 ∧ ↑Valued.v (y v) ≤ 1
h_mul : ↑Valued.v (x v * y v) = ↑Valued.v (x v) * ↑Valued.v (y v)
⊢ ↑Valued.v (x v) * ↑Valued.v (y v) ≤ 1
[PROOFSTEP]
exact @mul_le_one' (WithZero (Multiplicative ℤ)) _ _ (OrderedCommMonoid.to_covariantClass_left _) _ _ hv.left hv.right
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
h_subset :
  {v | ¬(x * y) v ∈ adicCompletionIntegers K v} ⊆
    {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
⊢ Set.Finite {x_1 | ¬(x * y) x_1 ∈ adicCompletionIntegers K x_1}
[PROOFSTEP]
exact (hx.union hy).subset h_subset
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsFiniteAdele 1
[PROOFSTEP]
rw [IsFiniteAdele, Filter.eventually_cofinite]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Set.Finite {x | ¬OfNat.ofNat 1 x ∈ adicCompletionIntegers K x}
[PROOFSTEP]
have h_empty : {v : HeightOneSpectrum R | ¬(1 : v.adicCompletion K) ∈ v.adicCompletionIntegers K} = ∅ :=
  by
  ext v; rw [mem_empty_iff_false, iff_false_iff]; intro hv
  rw [mem_setOf] at hv ; apply hv; rw [mem_adicCompletionIntegers]
  exact le_of_eq Valued.v.map_one'
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ {v | ¬1 ∈ adicCompletionIntegers K v} = ∅
[PROOFSTEP]
ext v
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
⊢ v ∈ {v | ¬1 ∈ adicCompletionIntegers K v} ↔ v ∈ ∅
[PROOFSTEP]
rw [mem_empty_iff_false, iff_false_iff]
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
⊢ ¬v ∈ {v | ¬1 ∈ adicCompletionIntegers K v}
[PROOFSTEP]
intro hv
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : v ∈ {v | ¬1 ∈ adicCompletionIntegers K v}
⊢ False
[PROOFSTEP]
rw [mem_setOf] at hv
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬1 ∈ adicCompletionIntegers K v
⊢ False
[PROOFSTEP]
apply hv
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬1 ∈ adicCompletionIntegers K v
⊢ 1 ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers]
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬1 ∈ adicCompletionIntegers K v
⊢ ↑Valued.v 1 ≤ 1
[PROOFSTEP]
exact le_of_eq Valued.v.map_one'
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
h_empty : {v | ¬1 ∈ adicCompletionIntegers K v} = ∅
⊢ Set.Finite {x | ¬OfNat.ofNat 1 x ∈ adicCompletionIntegers K x}
[PROOFSTEP]
convert finite_empty


[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hpx : eval₂ (algebraMap O R) x p = 0
hvx : 1 < ↑v x
⊢ False
[PROOFSTEP]
rw [hpm.as_sum, eval₂_add, eval₂_pow, eval₂_X, eval₂_finset_sum, add_eq_zero_iff_eq_neg] at hpx
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hpx : x ^ natDegree p = -∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i)
hvx : 1 < ↑v x
⊢ False
[PROOFSTEP]
replace hpx := congr_arg v hpx
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
⊢ False
[PROOFSTEP]
refine' ne_of_gt _ hpx
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
⊢ ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i)) < ↑v (x ^ natDegree p)
[PROOFSTEP]
rw [v.map_neg, v.map_pow]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
⊢ ↑v (∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i)) < ↑v x ^ natDegree p
[PROOFSTEP]
refine' v.map_sum_lt' (zero_lt_one.trans_le (one_le_pow_of_one_le' hvx.le _)) fun i hi => _
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
⊢ ↑v (eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i)) < ↑v x ^ natDegree p
[PROOFSTEP]
rw [eval₂_mul, eval₂_pow, eval₂_C, eval₂_X, v.map_mul, v.map_pow, ← one_mul (v x ^ p.natDegree)]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
⊢ ↑v (↑(algebraMap O R) (coeff p i)) * ↑v x ^ i < 1 * ↑v x ^ natDegree p
[PROOFSTEP]
cases' (hv.2 <| p.coeff i).lt_or_eq with hvpi hvpi
[GOAL]
case inl
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
hvpi : ↑v (↑(algebraMap O R) (coeff p i)) < 1
⊢ ↑v (↑(algebraMap O R) (coeff p i)) * ↑v x ^ i < 1 * ↑v x ^ natDegree p
[PROOFSTEP]
exact mul_lt_mul₀ hvpi (pow_lt_pow₀ hvx <| Finset.mem_range.1 hi)
[GOAL]
case inr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
hvpi : ↑v (↑(algebraMap O R) (coeff p i)) = 1
⊢ ↑v (↑(algebraMap O R) (coeff p i)) * ↑v x ^ i < 1 * ↑v x ^ natDegree p
[PROOFSTEP]
erw [hvpi]
[GOAL]
case inr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
hvpi : ↑v (↑(algebraMap O R) (coeff p i)) = 1
⊢ 1 * ↑v x ^ i < 1 * ↑v x ^ natDegree p
[PROOFSTEP]
rw [one_mul, one_mul]
[GOAL]
case inr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
hvpi : ↑v (↑(algebraMap O R) (coeff p i)) = 1
⊢ ↑v x ^ i < ↑v x ^ natDegree p
[PROOFSTEP]
exact pow_lt_pow₀ hvx (Finset.mem_range.1 hi)


[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ f : R →+* S
a✝ b✝ : R ⧸ ker f
a b : R
h : ↑f a = ↑f b
⊢ a - b ∈ ker f
[PROOFSTEP]
rw [mem_ker, map_sub, h, sub_self]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
⊢ Function.Injective ↑(Ideal.Quotient.lift I f H)
[PROOFSTEP]
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
⊢ ∀ (x : R ⧸ I), ↑(Ideal.Quotient.lift I f H) x = 0 → x = 0
[PROOFSTEP]
intro u hu
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
u : R ⧸ I
hu : ↑(Ideal.Quotient.lift I f H) u = 0
⊢ u = 0
[PROOFSTEP]
obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective u
[GOAL]
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑(Ideal.Quotient.lift I f H) (↑(Ideal.Quotient.mk I) v) = 0
⊢ ↑(Ideal.Quotient.mk I) v = 0
[PROOFSTEP]
rw [Ideal.Quotient.lift_mk] at hu
[GOAL]
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑f v = 0
⊢ ↑(Ideal.Quotient.mk I) v = 0
[PROOFSTEP]
rw [Ideal.Quotient.eq_zero_iff_mem]
[GOAL]
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑f v = 0
⊢ v ∈ I
[PROOFSTEP]
exact hI ((RingHom.mem_ker f).mpr hu)
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
g : S → R
hf : Function.RightInverse g ↑f
src✝ : R ⧸ ker f →+* S := kerLift f
⊢ Function.LeftInverse (↑(Ideal.Quotient.mk (ker f)) ∘ g) ↑(kerLift f)
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
g : S → R
hf : Function.RightInverse g ↑f
src✝ : R ⧸ ker f →+* S := kerLift f
x✝ : R ⧸ ker f
x : R
⊢ (↑(Ideal.Quotient.mk (ker f)) ∘ g) (↑(kerLift f) (Quot.mk Setoid.r x)) = Quot.mk Setoid.r x
[PROOFSTEP]
apply kerLift_injective
[GOAL]
case mk.a
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
g : S → R
hf : Function.RightInverse g ↑f
src✝ : R ⧸ ker f →+* S := kerLift f
x✝ : R ⧸ ker f
x : R
⊢ ↑(kerLift f) ((↑(Ideal.Quotient.mk (ker f)) ∘ g) (↑(kerLift f) (Quot.mk Setoid.r x))) =
    ↑(kerLift f) (Quot.mk Setoid.r x)
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, kerLift_mk, Function.comp_apply, hf (f x)]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ RingHom.ker (Quotient.mk I) = I
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
x✝ : R
⊢ x✝ ∈ RingHom.ker (Quotient.mk I) ↔ x✝ ∈ I
[PROOFSTEP]
rw [RingHom.ker, mem_comap, @Submodule.mem_bot _ _ _ _ Semiring.toModule _, Quotient.eq_zero_iff_mem]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
h : I ≤ J
⊢ map (Quotient.mk J) I = ⊥
[PROOFSTEP]
rw [map_eq_bot_iff_le_ker, mk_ker]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
h : I ≤ J
⊢ I ≤ J
[PROOFSTEP]
exact h
[GOAL]
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
⊢ RingHom.ker (Quotient.lift I f H) = map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
apply Ideal.ext
[GOAL]
case h
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
⊢ ∀ (x : R ⧸ I), x ∈ RingHom.ker (Quotient.lift I f H) ↔ x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ RingHom.ker (Quotient.lift I f H) ↔ x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ RingHom.ker (Quotient.lift I f H) → x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
intro hx
[GOAL]
case h.mp
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ RingHom.ker (Quotient.lift I f H)
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
obtain ⟨y, hy⟩ := Quotient.mk_surjective x
[GOAL]
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ RingHom.ker (Quotient.lift I f H)
y : R
hy : ↑(Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
rw [RingHom.mem_ker, ← hy, Ideal.Quotient.lift_mk, ← RingHom.mem_ker] at hx
[GOAL]
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hx : y ∈ RingHom.ker f
hy : ↑(Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]
[GOAL]
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hx : y ∈ RingHom.ker f
hy : ↑(Quotient.mk I) y = x
⊢ ∃ x, x ∈ RingHom.ker f ∧ ↑(Quotient.mk I) x = ↑(Quotient.mk I) y
[PROOFSTEP]
exact ⟨y, hx, rfl⟩
[GOAL]
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f) → x ∈ RingHom.ker (Quotient.lift I f H)
[PROOFSTEP]
intro hx
[GOAL]
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ map (Quotient.mk I) (RingHom.ker f)
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
[PROOFSTEP]
rw [mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective] at hx
[GOAL]
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : ∃ x_1, x_1 ∈ RingHom.ker f ∧ ↑(Quotient.mk I) x_1 = x
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
[PROOFSTEP]
obtain ⟨y, hy⟩ := hx
[GOAL]
case h.mpr.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hy : y ∈ RingHom.ker f ∧ ↑(Quotient.mk I) y = x
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
[PROOFSTEP]
rw [RingHom.mem_ker, ← hy.right, Ideal.Quotient.lift_mk]
[GOAL]
case h.mpr.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hy : y ∈ RingHom.ker f ∧ ↑(Quotient.mk I) y = x
⊢ ↑f y = 0
[PROOFSTEP]
exact hy.left
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
⊢ IsMaximal ⊥
[PROOFSTEP]
skip
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
⊢ IsMaximal ⊥
[PROOFSTEP]
letI := Quotient.field I
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
this : Field (R ⧸ I) := Quotient.field I
⊢ IsMaximal ⊥
[PROOFSTEP]
exact bot_isMaximal
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
⊢ ↑(Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J ⊔ I
[PROOFSTEP]
rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot, mk_ker]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
hIJ : I ≤ J
x : R
⊢ ↑(Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J
[PROOFSTEP]
rw [mem_quotient_iff_mem_sup, sup_eq_left.mpr hIJ]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Algebra R₁ B
inst✝¹ : SMul R₁ R₂
inst✝ : IsScalarTower R₁ R₂ A
I : Ideal A
⊢ IsScalarTower R₁ R₂ (A ⧸ I)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
f : A →ₐ[R₁] B
hI : ∀ (a : A), a ∈ I → ↑f a = 0
src✝ : A ⧸ I →+* B := lift I (↑f) hI
r : R₁
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : A ⧸ I), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R₁ (A ⧸ I)) r) =
    ↑(algebraMap R₁ B) r
[PROOFSTEP]
have : algebraMap R₁ (A ⧸ I) r = algebraMap A (A ⧸ I) (algebraMap R₁ A r) := by
  simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
f : A →ₐ[R₁] B
hI : ∀ (a : A), a ∈ I → ↑f a = 0
src✝ : A ⧸ I →+* B := lift I (↑f) hI
r : R₁
⊢ ↑(algebraMap R₁ (A ⧸ I)) r = ↑(algebraMap A (A ⧸ I)) (↑(algebraMap R₁ A) r)
[PROOFSTEP]
simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
f : A →ₐ[R₁] B
hI : ∀ (a : A), a ∈ I → ↑f a = 0
src✝ : A ⧸ I →+* B := lift I (↑f) hI
r : R₁
this : ↑(algebraMap R₁ (A ⧸ I)) r = ↑(algebraMap A (A ⧸ I)) (↑(algebraMap R₁ A) r)
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : A ⧸ I), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R₁ (A ⧸ I)) r) =
    ↑(algebraMap R₁ B) r
[PROOFSTEP]
rw [this, Ideal.Quotient.algebraMap_eq, RingHom.toFun_eq_coe, Ideal.Quotient.lift_mk, AlgHom.coe_toRingHom,
  Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, map_one]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
x : A ⧸ RingHom.ker ↑f
⊢ ↑(RingHom.kerLift ↑f) (r • x) = r • ↑(RingHom.kerLift ↑f) x
[PROOFSTEP]
obtain ⟨a, rfl⟩ := Quotient.mkₐ_surjective R₁ _ x
[GOAL]
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
a : A
⊢ ↑(RingHom.kerLift ↑f) (r • ↑(Quotient.mkₐ R₁ (RingHom.ker ↑f)) a) =
    r • ↑(RingHom.kerLift ↑f) (↑(Quotient.mkₐ R₁ (RingHom.ker ↑f)) a)
[PROOFSTEP]
exact f.map_smul _ _
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
a : A
⊢ ↑(kerLiftAlg f) (↑(Quotient.mk (RingHom.ker f)) a) = ↑f a
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R →+* S
hIJ : I ≤ comap f J
x✝ : R
ha : x✝ ∈ I
⊢ ↑(RingHom.comp (Quotient.mk J) f) x✝ = 0
[PROOFSTEP]
simpa [Function.comp_apply, RingHom.coe_comp, Quotient.eq_zero_iff_mem] using hIJ ha
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
x : R
⊢ ↑(RingHom.comp (quotientMap I f H) (Quotient.mk J)) x = ↑(RingHom.comp (Quotient.mk I) f) x
[PROOFSTEP]
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.quotientMap_mk]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
⊢ I ≤ comap (↑f) J
[PROOFSTEP]
rw [hIJ]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
⊢ I ≤ comap (↑f) (map (↑f) I)
[PROOFSTEP]
exact @le_comap_map _ S _ _ _ _ _ _
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
⊢ J ≤ comap (↑(RingEquiv.symm f)) I
[PROOFSTEP]
rw [hIJ]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
⊢ map (↑f) I ≤ comap (↑(RingEquiv.symm f)) I
[PROOFSTEP]
exact le_of_eq (map_comap_of_equiv I f)
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
⊢ Function.LeftInverse (↑(quotientMap I ↑(RingEquiv.symm f) (_ : J ≤ comap (↑(RingEquiv.symm f)) I))) src✝.toFun
[PROOFSTEP]
rintro ⟨r⟩
[GOAL]
case mk
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
x✝ : R ⧸ I
r : R
⊢ ↑(quotientMap I ↑(RingEquiv.symm f) (_ : J ≤ comap (↑(RingEquiv.symm f)) I))
      (OneHom.toFun (↑↑src✝) (Quot.mk Setoid.r r)) =
    Quot.mk Setoid.r r
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe, quotientMap_mk,
  RingEquiv.coe_toRingHom, RingEquiv.symm_apply_apply]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
⊢ Function.RightInverse (↑(quotientMap I ↑(RingEquiv.symm f) (_ : J ≤ comap (↑(RingEquiv.symm f)) I))) src✝.toFun
[PROOFSTEP]
rintro ⟨s⟩
[GOAL]
case mk
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
x✝ : S ⧸ J
s : S
⊢ OneHom.toFun (↑↑src✝)
      (↑(quotientMap I ↑(RingEquiv.symm f) (_ : J ≤ comap (↑(RingEquiv.symm f)) I)) (Quot.mk Setoid.r s)) =
    Quot.mk Setoid.r s
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe, quotientMap_mk,
  RingEquiv.coe_toRingHom, RingEquiv.apply_symm_apply]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
⊢ Function.Injective ↑(quotientMap I f H)
[PROOFSTEP]
refine' (injective_iff_map_eq_zero (quotientMap I f H)).2 fun a ha => _
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
a : R ⧸ J
ha : ↑(quotientMap I f H) a = 0
⊢ a = 0
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
[GOAL]
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : ↑(quotientMap I f H) (↑(Quotient.mk J) r) = 0
⊢ ↑(Quotient.mk J) r = 0
[PROOFSTEP]
rw [quotientMap_mk, Quotient.eq_zero_iff_mem] at ha
[GOAL]
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : ↑f r ∈ I
⊢ ↑(Quotient.mk J) r = 0
[PROOFSTEP]
exact Quotient.eq_zero_iff_mem.mpr (h ha)
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
hf : Function.Surjective ↑f
x✝ : S ⧸ I
x : S
hx : ↑(Quotient.mk I) x = x✝
y : R
hy : ↑f y = x
⊢ ↑(quotientMap I f H) (↑(Quotient.mk J) y) = x✝
[PROOFSTEP]
simp [hx, hy]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Algebra R₁ B
R' : Type u_5
S' : Type u_6
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : RingHom.comp f' g = RingHom.comp g' f
I : Ideal S'
⊢ let leq := (_ : comap f (comap g' I) ≤ comap g (comap f' I));
  RingHom.comp (quotientMap I g' (_ : comap g' I ≤ comap g' I))
      (quotientMap (comap g' I) f (_ : comap f (comap g' I) ≤ comap f (comap g' I))) =
    RingHom.comp (quotientMap I f' (_ : comap f' I ≤ comap f' I)) (quotientMap (comap f' I) g leq)
[PROOFSTEP]
refine RingHom.ext fun a => ?_
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Algebra R₁ B
R' : Type u_5
S' : Type u_6
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : RingHom.comp f' g = RingHom.comp g' f
I : Ideal S'
a : R ⧸ comap f (comap g' I)
⊢ ↑(RingHom.comp (quotientMap I g' (_ : comap g' I ≤ comap g' I))
          (quotientMap (comap g' I) f (_ : comap f (comap g' I) ≤ comap f (comap g' I))))
      a =
    ↑(RingHom.comp (quotientMap I f' (_ : comap f' I ≤ comap f' I))
          (quotientMap (comap f' I) g (_ : comap f (comap g' I) ≤ comap g (comap f' I))))
      a
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
[GOAL]
case intro
R : Type u
S : Type v
F : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Algebra R₁ B
R' : Type u_5
S' : Type u_6
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : RingHom.comp f' g = RingHom.comp g' f
I : Ideal S'
r : R
⊢ ↑(RingHom.comp (quotientMap I g' (_ : comap g' I ≤ comap g' I))
          (quotientMap (comap g' I) f (_ : comap f (comap g' I) ≤ comap f (comap g' I))))
      (↑(Quotient.mk (comap f (comap g' I))) r) =
    ↑(RingHom.comp (quotientMap I f' (_ : comap f' I ≤ comap f' I))
          (quotientMap (comap f' I) g (_ : comap f (comap g' I) ≤ comap g (comap f' I))))
      (↑(Quotient.mk (comap f (comap g' I))) r)
[PROOFSTEP]
simp only [RingHom.comp_apply, quotientMap_mk]
[GOAL]
case intro
R : Type u
S : Type v
F : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Algebra R₁ B
R' : Type u_5
S' : Type u_6
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : RingHom.comp f' g = RingHom.comp g' f
I : Ideal S'
r : R
⊢ ↑(Quotient.mk I) (↑g' (↑f r)) = ↑(Quotient.mk I) (↑f' (↑g r))
[PROOFSTEP]
exact congr_arg (Ideal.Quotient.mk I) (_root_.trans (g'.comp_apply f r).symm (hfg ▸ f'.comp_apply g r))
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A →ₐ[R₁] B
hIJ : I ≤ comap f J
src✝ : A ⧸ I →+* B ⧸ J := quotientMap J (↑f) hIJ
r : R₁
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : A ⧸ I), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R₁ (A ⧸ I)) r) =
    ↑(algebraMap R₁ (B ⧸ J)) r
[PROOFSTEP]
simp only [RingHom.toFun_eq_coe, quotientMap_algebraMap, AlgHom.coe_toRingHom, AlgHom.commutes, Quotient.mk_algebraMap]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A →ₐ[R₁] B
H : I ≤ comap f J
x : A
⊢ ↑(AlgHom.comp (quotientMapₐ J f H) (Quotient.mkₐ R₁ I)) x = ↑(AlgHom.comp (Quotient.mkₐ R₁ J) f) x
[PROOFSTEP]
simp only [quotient_map_mkₐ, Quotient.mkₐ_eq_mk, AlgHom.comp_apply]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A ≃ₐ[R₁] B
hIJ : J = map (↑f) I
src✝ : A ⧸ I ≃+* B ⧸ J := quotientEquiv I J (↑f) hIJ
r : R₁
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R₁ (A ⧸ I)) r) = ↑(algebraMap R₁ (B ⧸ J)) r
[PROOFSTEP]
have : ∀ (e : RingEquiv (A ⧸ I) (B ⧸ J)), Equiv.toFun e.toEquiv = FunLike.coe e := fun _ ↦ rfl
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A ≃ₐ[R₁] B
hIJ : J = map (↑f) I
src✝ : A ⧸ I ≃+* B ⧸ J := quotientEquiv I J (↑f) hIJ
r : R₁
this : ∀ (e : A ⧸ I ≃+* B ⧸ J), e.toFun = ↑e
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R₁ (A ⧸ I)) r) = ↑(algebraMap R₁ (B ⧸ J)) r
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A ≃ₐ[R₁] B
hIJ : J = map (↑f) I
src✝ : A ⧸ I ≃+* B ⧸ J := quotientEquiv I J (↑f) hIJ
r : R₁
this : ∀ (e : A ⧸ I ≃+* B ⧸ J), e.toFun = ↑e
⊢ ↑src✝ (↑(algebraMap R₁ (A ⧸ I)) r) = ↑(algebraMap R₁ (B ⧸ J)) r
[PROOFSTEP]
simp only [quotientEquiv_apply, RingHom.toFun_eq_coe, quotientMap_algebraMap, RingEquiv.coe_toRingHom,
  AlgEquiv.coe_ringEquiv, AlgEquiv.commutes, Quotient.mk_algebraMap]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
⊢ Function.Injective ↑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I))
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩ hab
[GOAL]
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab :
  ↑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I)) (Quot.mk Setoid.r a) =
    ↑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I)) (Quot.mk Setoid.r b)
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
[PROOFSTEP]
replace hab := Quotient.eq.mp hab
[GOAL]
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : ↑(algebraMap R A) a - ↑(algebraMap R A) b ∈ I
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
[PROOFSTEP]
rw [← RingHom.map_sub] at hab
[GOAL]
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : ↑(algebraMap R A) (a - b) ∈ I
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
[PROOFSTEP]
exact Quotient.eq.mpr hab
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal A
h : I = J
⊢ AlgEquiv.symm (quotientEquivAlgOfEq R₁ h) = quotientEquivAlgOfEq R₁ (_ : J = I)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal A
h : I = J
a✝ : A ⧸ J
⊢ ↑(AlgEquiv.symm (quotientEquivAlgOfEq R₁ h)) a✝ = ↑(quotientEquivAlgOfEq R₁ (_ : J = I)) a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal R
h : I ≤ J
⊢ comap (Quotient.mk I) (map (Quotient.mk I) J) = J
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ x✝ ∈ comap (Quotient.mk I) (map (Quotient.mk I) J) ↔ x✝ ∈ J
[PROOFSTEP]
rw [← Ideal.mem_quotient_iff_mem h, Ideal.mem_comap]
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.ker (quotLeftToQuotSup I J) = map (Ideal.Quotient.mk I) J
[PROOFSTEP]
simp only [mk_ker, sup_idem, sup_comm, quotLeftToQuotSup, Quotient.factor, ker_quotient_lift,
  map_eq_iff_sup_ker_eq_of_surjective (Ideal.Quotient.mk I) Quotient.mk_surjective, ← sup_assoc]
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.ker (quotQuotMk I J) = I ⊔ J
[PROOFSTEP]
rw [RingHom.ker_eq_comap_bot, quotQuotMk, ← comap_comap, ← RingHom.ker, mk_ker,
  comap_map_of_surjective (Ideal.Quotient.mk I) Quotient.mk_surjective, ← RingHom.ker, mk_ker, sup_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp ↑(liftSupQuotQuotMk I J) ↑(quotQuotToQuotSup I J) = RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
[PROOFSTEP]
repeat apply Ideal.Quotient.ringHom_ext
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp ↑(liftSupQuotQuotMk I J) ↑(quotQuotToQuotSup I J) = RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp (RingHom.comp ↑(liftSupQuotQuotMk I J) ↑(quotQuotToQuotSup I J))
      (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)) =
    RingHom.comp (RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)) (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J))
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case h.h
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp
      (RingHom.comp (RingHom.comp ↑(liftSupQuotQuotMk I J) ↑(quotQuotToQuotSup I J))
        (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I) =
    RingHom.comp
      (RingHom.comp (RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J))
        (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I)
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case h.h
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp
      (RingHom.comp (RingHom.comp ↑(liftSupQuotQuotMk I J) ↑(quotQuotToQuotSup I J))
        (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I) =
    RingHom.comp
      (RingHom.comp (RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J))
        (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp ↑(quotQuotToQuotSup I J) ↑(liftSupQuotQuotMk I J) = RingHom.id (R ⧸ I ⊔ J)
[PROOFSTEP]
repeat apply Ideal.Quotient.ringHom_ext
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp ↑(quotQuotToQuotSup I J) ↑(liftSupQuotQuotMk I J) = RingHom.id (R ⧸ I ⊔ J)
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp (RingHom.comp ↑(quotQuotToQuotSup I J) ↑(liftSupQuotQuotMk I J)) (Ideal.Quotient.mk (I ⊔ J)) =
    RingHom.comp (RingHom.id (R ⧸ I ⊔ J)) (Ideal.Quotient.mk (I ⊔ J))
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp (RingHom.comp ↑(quotQuotToQuotSup I J) ↑(liftSupQuotQuotMk I J)) (Ideal.Quotient.mk (I ⊔ J)) =
    RingHom.comp (RingHom.id (R ⧸ I ⊔ J)) (Ideal.Quotient.mk (I ⊔ J))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingEquiv.symm (quotQuotEquivComm I J) = quotQuotEquivComm J I
[PROOFSTEP]
change
  (((quotQuotEquivQuotSup I J).trans (quotEquivOfEq (sup_comm))).trans (quotQuotEquivQuotSup J I).symm).symm =
    ((quotQuotEquivQuotSup J I).trans (quotEquivOfEq (sup_comm))).trans (quotQuotEquivQuotSup I J).symm
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingEquiv.symm
      (RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup I J) (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
        (RingEquiv.symm (quotQuotEquivQuotSup J I))) =
    RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup J I) (quotEquivOfEq (_ : J ⊔ I = I ⊔ J)))
      (RingEquiv.symm (quotQuotEquivQuotSup I J))
[PROOFSTEP]
ext r
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ ↑(RingEquiv.symm
          (RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup I J) (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
            (RingEquiv.symm (quotQuotEquivQuotSup J I))))
      r =
    ↑(RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup J I) (quotEquivOfEq (_ : J ⊔ I = I ⊔ J)))
          (RingEquiv.symm (quotQuotEquivQuotSup I J)))
      r
[PROOFSTEP]
dsimp
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ ↑(RingEquiv.symm (quotQuotEquivQuotSup I J))
      (↑(RingEquiv.symm (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
        (↑(RingEquiv.symm (RingEquiv.symm (quotQuotEquivQuotSup J I))) r)) =
    ↑(RingEquiv.symm (quotQuotEquivQuotSup I J)) (↑(quotEquivOfEq (_ : J ⊔ I = I ⊔ J)) (↑(quotQuotEquivQuotSup J I) r))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ RingHom.comp (↑(quotQuotEquivQuotOfLE h)) (quotQuotMk I J) = Ideal.Quotient.mk J
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ↑(RingHom.comp (↑(quotQuotEquivQuotOfLE h)) (quotQuotMk I J)) x✝ = ↑(Ideal.Quotient.mk J) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ RingHom.comp (↑(RingEquiv.symm (quotQuotEquivQuotOfLE h))) (Ideal.Quotient.mk J) = quotQuotMk I J
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ↑(RingHom.comp (↑(RingEquiv.symm (quotQuotEquivQuotOfLE h))) (Ideal.Quotient.mk J)) x✝ = ↑(quotQuotMk I J) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
⊢ AlgEquiv.symm (quotQuotEquivCommₐ R I J) = quotQuotEquivCommₐ R J I
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ ↑(AlgEquiv.symm (quotQuotEquivCommₐ R I J)) a✝ = ↑(quotQuotEquivCommₐ R J I) a✝
[PROOFSTEP]
unfold quotQuotEquivCommₐ
[GOAL]
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ ↑(AlgEquiv.symm
          (AlgEquiv.ofRingEquiv
            (_ :
              ∀ (x : R),
                ↑(quotQuotEquivComm I J) (↑(algebraMap R ((A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)) x) =
                  ↑(quotQuotEquivComm I J) (↑(algebraMap R ((A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)) x))))
      a✝ =
    ↑(AlgEquiv.ofRingEquiv
          (_ :
            ∀ (x : R),
              ↑(quotQuotEquivComm J I) (↑(algebraMap R ((A ⧸ J) ⧸ map (Quotient.mkₐ R J) I)) x) =
                ↑(quotQuotEquivComm J I) (↑(algebraMap R ((A ⧸ J) ⧸ map (Quotient.mkₐ R J) I)) x)))
      a✝
[PROOFSTEP]
congr


[GOAL]
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
s : { x // x ∈ ⊥ }
h : ↑s * x✝¹ = ↑s * x✝
⊢ x✝¹ * ↑s = x✝ * ↑s
[PROOFSTEP]
rcases s with ⟨s, hs⟩
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ s : R
hs : s ∈ ⊥
h : ↑{ val := s, property := hs } * x✝¹ = ↑{ val := s, property := hs } * x✝
⊢ x✝¹ * ↑{ val := s, property := hs } = x✝ * ↑{ val := s, property := hs }
[PROOFSTEP]
rw [Submonoid.mem_bot] at hs
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ s : R
hs✝ : s ∈ ⊥
hs : s = 1
h : ↑{ val := s, property := hs✝ } * x✝¹ = ↑{ val := s, property := hs✝ } * x✝
⊢ x✝¹ * ↑{ val := s, property := hs✝ } = x✝ * ↑{ val := s, property := hs✝ }
[PROOFSTEP]
subst hs
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
hs : 1 ∈ ⊥
h : ↑{ val := 1, property := hs } * x✝¹ = ↑{ val := 1, property := hs } * x✝
⊢ x✝¹ * ↑{ val := 1, property := hs } = x✝ * ↑{ val := 1, property := hs }
[PROOFSTEP]
rw [one_mul, one_mul] at h
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
hs : 1 ∈ ⊥
h : x✝¹ = x✝
⊢ x✝¹ * ↑{ val := 1, property := hs } = x✝ * ↑{ val := 1, property := hs }
[PROOFSTEP]
subst h
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ : R
hs : 1 ∈ ⊥
⊢ x✝ * ↑{ val := 1, property := hs } = x✝ * ↑{ val := 1, property := hs }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ : R
s : { x // x ∈ ⊥ }
⊢ x✝ * ↑((fun x s => s) x✝ s) = ↑s * (fun r x => r) x✝ s
[PROOFSTEP]
rcases s with ⟨s, hs⟩
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ s : R
hs : s ∈ ⊥
⊢ x✝ * ↑((fun x s => s) x✝ { val := s, property := hs }) =
    ↑{ val := s, property := hs } * (fun r x => r) x✝ { val := s, property := hs }
[PROOFSTEP]
rw [Submonoid.mem_bot] at hs
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ s : R
hs✝ : s ∈ ⊥
hs : s = 1
⊢ x✝ * ↑((fun x s => s) x✝ { val := s, property := hs✝ }) =
    ↑{ val := s, property := hs✝ } * (fun r x => r) x✝ { val := s, property := hs✝ }
[PROOFSTEP]
simp [hs]
[GOAL]
R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.7831
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : { x // x ∈ S }
h : ↑s * m = ↑s * n
⊢ m * ↑s = n * ↑s
[PROOFSTEP]
rw [mul_comm n s, mul_comm m s, h]
[GOAL]
R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.7831
inst✝ : CommMonoid R
S : Submonoid R
r : R
s : { x // x ∈ S }
⊢ r * ↑((fun x s => s) r s) = ↑s * (fun r x => r) r s
[PROOFSTEP]
rw [mul_comm]


[GOAL]
⊢ WellFounded DvdNotUnit
[PROOFSTEP]
refine'
  RelHomClass.wellFounded (⟨fun x : ℕ => if x = 0 then (⊤ : ℕ∞) else x, _⟩ : DvdNotUnit →r (· < ·))
    (WithTop.wellFounded_lt Nat.lt_wfRel.wf)
[GOAL]
⊢ ∀ {a b : ℕ}, DvdNotUnit a b → (fun x => if x = 0 then ⊤ else ↑x) a < (fun x => if x = 0 then ⊤ else ↑x) b
[PROOFSTEP]
intro a b h
[GOAL]
a b : ℕ
h : DvdNotUnit a b
⊢ (fun x => if x = 0 then ⊤ else ↑x) a < (fun x => if x = 0 then ⊤ else ↑x) b
[PROOFSTEP]
cases' a with a
[GOAL]
case zero
b : ℕ
h : DvdNotUnit zero b
⊢ (fun x => if x = 0 then ⊤ else ↑x) zero < (fun x => if x = 0 then ⊤ else ↑x) b
[PROOFSTEP]
exfalso
[GOAL]
case zero.h
b : ℕ
h : DvdNotUnit zero b
⊢ False
[PROOFSTEP]
revert h
[GOAL]
case zero.h
b : ℕ
⊢ DvdNotUnit zero b → False
[PROOFSTEP]
simp [DvdNotUnit]
[GOAL]
case succ
b a : ℕ
h : DvdNotUnit (succ a) b
⊢ (fun x => if x = 0 then ⊤ else ↑x) (succ a) < (fun x => if x = 0 then ⊤ else ↑x) b
[PROOFSTEP]
cases b
[GOAL]
case succ.zero
a : ℕ
h : DvdNotUnit (succ a) zero
⊢ (fun x => if x = 0 then ⊤ else ↑x) (succ a) < (fun x => if x = 0 then ⊤ else ↑x) zero
[PROOFSTEP]
simpa [succ_ne_zero] using WithTop.coe_lt_top (a + 1)
[GOAL]
case succ.succ
a n✝ : ℕ
h : DvdNotUnit (succ a) (succ n✝)
⊢ (fun x => if x = 0 then ⊤ else ↑x) (succ a) < (fun x => if x = 0 then ⊤ else ↑x) (succ n✝)
[PROOFSTEP]
cases' dvd_and_not_dvd_iff.2 h with h1 h2
[GOAL]
case succ.succ.intro
a n✝ : ℕ
h : DvdNotUnit (succ a) (succ n✝)
h1 : succ a ∣ succ n✝
h2 : ¬succ n✝ ∣ succ a
⊢ (fun x => if x = 0 then ⊤ else ↑x) (succ a) < (fun x => if x = 0 then ⊤ else ↑x) (succ n✝)
[PROOFSTEP]
simp only [succ_ne_zero, cast_lt, if_false]
[GOAL]
case succ.succ.intro
a n✝ : ℕ
h : DvdNotUnit (succ a) (succ n✝)
h1 : succ a ∣ succ n✝
h2 : ¬succ n✝ ∣ succ a
⊢ succ a < succ n✝
[PROOFSTEP]
refine lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h1) fun con => h2 ?_
[GOAL]
case succ.succ.intro
a n✝ : ℕ
h : DvdNotUnit (succ a) (succ n✝)
h1 : succ a ∣ succ n✝
h2 : ¬succ n✝ ∣ succ a
con : succ a = succ n✝
⊢ succ n✝ ∣ succ a
[PROOFSTEP]
rw [con]
[GOAL]
a b : ℕ
⊢ Associated (Nat.gcd a b * Nat.lcm a b) (a * b)
[PROOFSTEP]
rw [Nat.gcd_mul_lcm]
[GOAL]
a b : ℕ
⊢ Associated (a * b) (a * b)
[PROOFSTEP]
rfl
[GOAL]
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
cases' hna.lt_or_lt with ha ha
[GOAL]
case inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
cases' hnb.lt_or_lt with hb hb
[GOAL]
case inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
cases' hnb.lt_or_lt with hb hb
[GOAL]
case inl.inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : b < 0
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
simp [mul_nonneg_iff, ha.le, ha.not_le, hb.le, hb.not_le]
[GOAL]
case inl.inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : 0 < b
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
simp [mul_nonneg_iff, ha.le, ha.not_le, hb.le, hb.not_le]
[GOAL]
case inr.inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : b < 0
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
simp [mul_nonneg_iff, ha.le, ha.not_le, hb.le, hb.not_le]
[GOAL]
case inr.inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : 0 < b
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
simp [mul_nonneg_iff, ha.le, ha.not_le, hb.le, hb.not_le]
[GOAL]
u : ℤˣ
eq : u = -1
⊢ -1 < 0
[PROOFSTEP]
decide
[GOAL]
z : ℤ
h : 0 ≤ z
⊢ ↑normalize z = z
[PROOFSTEP]
rw [normalize_apply, normUnit_eq, if_pos h, Units.val_one, mul_one]
[GOAL]
z : ℤ
h : z ≤ 0
⊢ ↑normalize z = -z
[PROOFSTEP]
obtain rfl | h := h.eq_or_lt
[GOAL]
case inl
h : 0 ≤ 0
⊢ ↑normalize 0 = -0
[PROOFSTEP]
simp
[GOAL]
case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ ↑normalize z = -z
[PROOFSTEP]
rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one, mul_neg_one]
[GOAL]
z : ℤ
⊢ |z| = ↑normalize z
[PROOFSTEP]
cases le_total 0 z
[GOAL]
case inl
z : ℤ
h✝ : 0 ≤ z
⊢ |z| = ↑normalize z
[PROOFSTEP]
simp [-normalize_apply, normalize_of_nonneg, normalize_of_nonpos, *]
[GOAL]
case inr
z : ℤ
h✝ : z ≤ 0
⊢ |z| = ↑normalize z
[PROOFSTEP]
simp [-normalize_apply, normalize_of_nonneg, normalize_of_nonpos, *]
[GOAL]
z : ℤ
hz : ↑normalize z = z
⊢ |z| = z
[PROOFSTEP]
rw [abs_eq_normalize, hz]
[GOAL]
a b : ℤ
⊢ Associated ((fun a b => ↑(gcd a b)) a b * (fun a b => ↑(lcm a b)) a b) (a * b)
[PROOFSTEP]
rw [← Int.ofNat_mul, gcd_mul_lcm, coe_natAbs, abs_eq_normalize]
[GOAL]
a b : ℤ
⊢ Associated (↑normalize (a * b)) (a * b)
[PROOFSTEP]
exact normalize_associated (a * b)
[GOAL]
a : ℤ
⊢ ∃ u x, ↑(natAbs a) = u * a
[PROOFSTEP]
cases' natAbs_eq a with h h
[GOAL]
case inl
a : ℤ
h : a = ↑(natAbs a)
⊢ ∃ u x, ↑(natAbs a) = u * a
[PROOFSTEP]
use 1, isUnit_one
[GOAL]
case h
a : ℤ
h : a = ↑(natAbs a)
⊢ ↑(natAbs a) = 1 * a
[PROOFSTEP]
rw [← h, one_mul]
[GOAL]
case inr
a : ℤ
h : a = -↑(natAbs a)
⊢ ∃ u x, ↑(natAbs a) = u * a
[PROOFSTEP]
use-1, isUnit_one.neg
[GOAL]
case h
a : ℤ
h : a = -↑(natAbs a)
⊢ ↑(natAbs a) = -1 * a
[PROOFSTEP]
rw [← neg_eq_iff_eq_neg.mpr h]
[GOAL]
case h
a : ℤ
h : a = -↑(natAbs a)
⊢ -a = -1 * a
[PROOFSTEP]
simp only [neg_mul, one_mul]
[GOAL]
a b : ℤ
⊢ gcd a b = 1 ↔ IsCoprime a b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b : ℤ
⊢ gcd a b = 1 → IsCoprime a b
[PROOFSTEP]
intro hg
[GOAL]
case mp
a b : ℤ
hg : gcd a b = 1
⊢ IsCoprime a b
[PROOFSTEP]
obtain ⟨ua, -, ha⟩ := exists_unit_of_abs a
[GOAL]
case mp.intro.intro
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
⊢ IsCoprime a b
[PROOFSTEP]
obtain ⟨ub, -, hb⟩ := exists_unit_of_abs b
[GOAL]
case mp.intro.intro.intro.intro
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
ub : ℤ
hb : ↑(natAbs b) = ub * b
⊢ IsCoprime a b
[PROOFSTEP]
use Nat.gcdA (Int.natAbs a) (Int.natAbs b) * ua, Nat.gcdB (Int.natAbs a) (Int.natAbs b) * ub
[GOAL]
case h
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
ub : ℤ
hb : ↑(natAbs b) = ub * b
⊢ Nat.gcdA (natAbs a) (natAbs b) * ua * a + Nat.gcdB (natAbs a) (natAbs b) * ub * b = 1
[PROOFSTEP]
rw [mul_assoc, ← ha, mul_assoc, ← hb, mul_comm, mul_comm _ (Int.natAbs b : ℤ), ← Nat.gcd_eq_gcd_ab, ← gcd_eq_natAbs, hg,
  Int.ofNat_one]
[GOAL]
case mpr
a b : ℤ
⊢ IsCoprime a b → gcd a b = 1
[PROOFSTEP]
rintro ⟨r, s, h⟩
[GOAL]
case mpr.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
⊢ gcd a b = 1
[PROOFSTEP]
by_contra hg
[GOAL]
case mpr.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
⊢ False
[PROOFSTEP]
obtain ⟨p, ⟨hp, ha, hb⟩⟩ := Nat.Prime.not_coprime_iff_dvd.mp hg
[GOAL]
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ False
[PROOFSTEP]
apply Nat.Prime.not_dvd_one hp
[GOAL]
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ p ∣ 1
[PROOFSTEP]
rw [← coe_nat_dvd, Int.ofNat_one, ← h]
[GOAL]
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ ↑p ∣ r * a + s * b
[PROOFSTEP]
exact dvd_add ((coe_nat_dvd_left.mpr ha).mul_left _) ((coe_nat_dvd_left.mpr hb).mul_left _)
[GOAL]
a b : ℤ
⊢ IsCoprime a b ↔ Nat.coprime (natAbs a) (natAbs b)
[PROOFSTEP]
rw [← gcd_eq_one_iff_coprime, Nat.coprime_iff_gcd_eq_one, gcd_eq_natAbs]
[GOAL]
a : ℤ
m n : ℕ
⊢ gcd a (↑m * ↑n) ≠ 1 ↔ gcd a ↑m ≠ 1 ∨ gcd a ↑n ≠ 1
[PROOFSTEP]
simp only [gcd_eq_one_iff_coprime, ← not_and_or, not_iff_not, IsCoprime.mul_right_iff]
[GOAL]
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
[PROOFSTEP]
have h' : IsUnit (GCDMonoid.gcd a b) := by
  rw [← coe_gcd, h, Int.ofNat_one]
  exact isUnit_one
[GOAL]
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
⊢ IsUnit (GCDMonoid.gcd a b)
[PROOFSTEP]
rw [← coe_gcd, h, Int.ofNat_one]
[GOAL]
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
[GOAL]
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
[PROOFSTEP]
obtain ⟨d, ⟨u, hu⟩⟩ := exists_associated_pow_of_mul_eq_pow h' heq
[GOAL]
case intro.intro
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
[PROOFSTEP]
use d
[GOAL]
case h
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ a = d ^ 2 ∨ a = -d ^ 2
[PROOFSTEP]
rw [← hu]
[GOAL]
case h
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
[PROOFSTEP]
cases' Int.units_eq_one_or u with hu' hu'
[GOAL]
case h.inl
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = 1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
[PROOFSTEP]
rw [hu']
[GOAL]
case h.inl
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = 1
⊢ d ^ 2 * ↑1 = d ^ 2 ∨ d ^ 2 * ↑1 = -d ^ 2
[PROOFSTEP]
simp
[GOAL]
case h.inr
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
[PROOFSTEP]
rw [hu']
[GOAL]
case h.inr
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑(-1) = d ^ 2 ∨ d ^ 2 * ↑(-1) = -d ^ 2
[PROOFSTEP]
simp
[GOAL]
a b : ℤ
⊢ natAbs (EuclideanDomain.gcd a b) = gcd a b
[PROOFSTEP]
apply Nat.dvd_antisymm
[GOAL]
case a
a b : ℤ
⊢ natAbs (EuclideanDomain.gcd a b) ∣ gcd a b
[PROOFSTEP]
rw [← Int.coe_nat_dvd]
[GOAL]
case a
a b : ℤ
⊢ gcd a b ∣ natAbs (EuclideanDomain.gcd a b)
[PROOFSTEP]
rw [← Int.coe_nat_dvd]
[GOAL]
case a
a b : ℤ
⊢ ↑(natAbs (EuclideanDomain.gcd a b)) ∣ ↑(gcd a b)
[PROOFSTEP]
rw [Int.natAbs_dvd]
[GOAL]
case a
a b : ℤ
⊢ EuclideanDomain.gcd a b ∣ ↑(gcd a b)
[PROOFSTEP]
exact Int.dvd_gcd (EuclideanDomain.gcd_dvd_left _ _) (EuclideanDomain.gcd_dvd_right _ _)
[GOAL]
case a
a b : ℤ
⊢ ↑(gcd a b) ∣ ↑(natAbs (EuclideanDomain.gcd a b))
[PROOFSTEP]
rw [Int.dvd_natAbs]
[GOAL]
case a
a b : ℤ
⊢ ↑(gcd a b) ∣ EuclideanDomain.gcd a b
[PROOFSTEP]
exact EuclideanDomain.dvd_gcd (Int.gcd_dvd_left _ _) (Int.gcd_dvd_right _ _)
[GOAL]
⊢ Associates ℤ ≃ ℕ
[PROOFSTEP]
refine' ⟨fun z => z.out.natAbs, fun n => Associates.mk n, _, _⟩
[GOAL]
case refine'_1
⊢ Function.LeftInverse (fun n => Associates.mk ↑n) fun z => Int.natAbs (Associates.out z)
[PROOFSTEP]
refine' fun a =>
  Quotient.inductionOn a fun a => Associates.mk_eq_mk_iff_associated.2 <| Associated.symm <| ⟨normUnit a, _⟩
[GOAL]
case refine'_1
a✝ : Associates ℤ
a : ℤ
⊢ a * ↑(normUnit a) = ↑((fun z => Int.natAbs (Associates.out z)) (Quotient.mk (Associated.setoid ℤ) a))
[PROOFSTEP]
simp [Int.abs_eq_normalize]
[GOAL]
case refine'_2
⊢ Function.RightInverse (fun n => Associates.mk ↑n) fun z => Int.natAbs (Associates.out z)
[PROOFSTEP]
intro n
[GOAL]
case refine'_2
n : ℕ
⊢ (fun z => Int.natAbs (Associates.out z)) ((fun n => Associates.mk ↑n) n) = n
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2
n : ℕ
⊢ Int.natAbs (↑n * ↑(normUnit ↑n)) = n
[PROOFSTEP]
rw [← normalize_apply, ← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_ofNat]
[GOAL]
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ natAbs m ∨ p ∣ natAbs n
[PROOFSTEP]
rwa [← hp.dvd_mul, ← Int.natAbs_mul, ← Int.coe_nat_dvd_left]
[GOAL]
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ ↑p ∣ m ∨ ↑p ∣ n
[PROOFSTEP]
rw [Int.coe_nat_dvd_left, Int.coe_nat_dvd_left]
[GOAL]
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ natAbs m ∨ p ∣ natAbs n
[PROOFSTEP]
exact Int.Prime.dvd_mul hp h
[GOAL]
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ natAbs n
[PROOFSTEP]
rw [Int.coe_nat_dvd_left, Int.natAbs_pow] at h
[GOAL]
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : p ∣ natAbs n ^ k
⊢ p ∣ natAbs n
[PROOFSTEP]
exact hp.dvd_of_dvd_pow h
[GOAL]
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ ↑p ∣ n
[PROOFSTEP]
rw [Int.coe_nat_dvd_left]
[GOAL]
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ natAbs n
[PROOFSTEP]
exact Int.Prime.dvd_pow hp h
[GOAL]
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
⊢ p = 2 ∨ p ∣ Int.natAbs m
[PROOFSTEP]
cases' Int.Prime.dvd_mul hp h with hp2 hpp
[GOAL]
case inl
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2 ∨ p ∣ Int.natAbs m
[PROOFSTEP]
apply Or.intro_left
[GOAL]
case inl.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2
[PROOFSTEP]
exact le_antisymm (Nat.le_of_dvd zero_lt_two hp2) (Nat.Prime.two_le hp)
[GOAL]
case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs (m ^ 2)
⊢ p = 2 ∨ p ∣ Int.natAbs m
[PROOFSTEP]
apply Or.intro_right
[GOAL]
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs (m ^ 2)
⊢ p ∣ Int.natAbs m
[PROOFSTEP]
rw [sq, Int.natAbs_mul] at hpp
[GOAL]
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs m * Int.natAbs m
⊢ p ∣ Int.natAbs m
[PROOFSTEP]
exact (or_self_iff _).mp ((Nat.Prime.dvd_mul hp).mp hpp)
[GOAL]
n : ℤ
hn : natAbs n ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ n
[PROOFSTEP]
obtain ⟨p, pp, pd⟩ := Nat.exists_prime_and_dvd hn
[GOAL]
case intro.intro
n : ℤ
hn : natAbs n ≠ 1
p : ℕ
pp : Nat.Prime p
pd : p ∣ natAbs n
⊢ ∃ p, Prime p ∧ p ∣ n
[PROOFSTEP]
exact ⟨p, Nat.prime_iff_prime_int.mp pp, Int.coe_nat_dvd_left.mpr pd⟩
[GOAL]
n : ℕ
⊢ normalizedFactors n = ↑(factors n)
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ normalizedFactors zero = ↑(factors zero)
case succ n✝ : ℕ ⊢ normalizedFactors (succ n✝) = ↑(factors (succ n✝))
[PROOFSTEP]
case zero => simp
[GOAL]
⊢ normalizedFactors zero = ↑(factors zero)
[PROOFSTEP]
case zero => simp
[GOAL]
⊢ normalizedFactors zero = ↑(factors zero)
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
⊢ normalizedFactors (succ n✝) = ↑(factors (succ n✝))
[PROOFSTEP]
case succ n =>
  rw [← Multiset.rel_eq, ← associated_eq_eq]
  apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _
  · rw [Multiset.coe_prod, Nat.prod_factors n.succ_ne_zero]
    apply normalizedFactors_prod (Nat.succ_ne_zero _)
  · intro x hx
    rw [Nat.irreducible_iff_prime, ← Nat.prime_iff]
    exact Nat.prime_of_mem_factors hx
[GOAL]
n : ℕ
⊢ normalizedFactors (succ n) = ↑(factors (succ n))
[PROOFSTEP]
case succ n =>
  rw [← Multiset.rel_eq, ← associated_eq_eq]
  apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _
  · rw [Multiset.coe_prod, Nat.prod_factors n.succ_ne_zero]
    apply normalizedFactors_prod (Nat.succ_ne_zero _)
  · intro x hx
    rw [Nat.irreducible_iff_prime, ← Nat.prime_iff]
    exact Nat.prime_of_mem_factors hx
[GOAL]
n : ℕ
⊢ normalizedFactors (succ n) = ↑(factors (succ n))
[PROOFSTEP]
rw [← Multiset.rel_eq, ← associated_eq_eq]
[GOAL]
n : ℕ
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) (normalizedFactors (succ n)) ↑(factors (succ n))
[PROOFSTEP]
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _
[GOAL]
n : ℕ
⊢ Associated (Multiset.prod (normalizedFactors (succ n))) (Multiset.prod ↑(factors (succ n)))
[PROOFSTEP]
rw [Multiset.coe_prod, Nat.prod_factors n.succ_ne_zero]
[GOAL]
n : ℕ
⊢ Associated (Multiset.prod (normalizedFactors (succ n))) (succ n)
[PROOFSTEP]
apply normalizedFactors_prod (Nat.succ_ne_zero _)
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), x ∈ ↑(factors (succ n)) → Irreducible x
[PROOFSTEP]
intro x hx
[GOAL]
n x : ℕ
hx : x ∈ ↑(factors (succ n))
⊢ Irreducible x
[PROOFSTEP]
rw [Nat.irreducible_iff_prime, ← Nat.prime_iff]
[GOAL]
n x : ℕ
hx : x ∈ ↑(factors (succ n))
⊢ Prime x
[PROOFSTEP]
exact Nat.prime_of_mem_factors hx
[GOAL]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ normalizedFactors (Multiset.prod s) = s
[PROOFSTEP]
rw [← Multiset.rel_eq, ← associated_eq_eq]
[GOAL]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) (normalizedFactors (Multiset.prod s)) s
[PROOFSTEP]
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor h (normalizedFactors_prod _)
[GOAL]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ Multiset.prod s ≠ 0
[PROOFSTEP]
rw [Ne.def, Multiset.prod_eq_zero_iff]
[GOAL]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ ¬0 ∈ s
[PROOFSTEP]
intro con
[GOAL]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
con : 0 ∈ s
⊢ False
[PROOFSTEP]
exact not_irreducible_zero (h 0 con)
[GOAL]
a b : ℤ
⊢ Finite a b ↔ Finite (_root_.Int.natAbs a) (_root_.Int.natAbs b)
[PROOFSTEP]
simp only [finite_def, ← Int.natAbs_dvd_natAbs, Int.natAbs_pow]
[GOAL]
a b : ℤ
⊢ Finite a b ↔ _root_.Int.natAbs a ≠ 1 ∧ b ≠ 0
[PROOFSTEP]
rw [finite_int_iff_natAbs_finite, finite_nat_iff, pos_iff_ne_zero, Int.natAbs_ne_zero]
[GOAL]
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ P n
[PROOFSTEP]
apply UniqueFactorizationMonoid.induction_on_prime
[GOAL]
case h₁
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ P 0
[PROOFSTEP]
exact h₀
[GOAL]
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ ∀ (x : ℕ), IsUnit x → P x
[PROOFSTEP]
intro n h
[GOAL]
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h✝ : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n✝ n : ℕ
h : IsUnit n
⊢ P n
[PROOFSTEP]
rw [Nat.isUnit_iff.1 h]
[GOAL]
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h✝ : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n✝ n : ℕ
h : IsUnit n
⊢ P 1
[PROOFSTEP]
exact h₁
[GOAL]
case h₃
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ ∀ (a p : ℕ), a ≠ 0 → Prime p → P a → P (p * a)
[PROOFSTEP]
intro a p _ hp ha
[GOAL]
case h₃
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n a p : ℕ
a✝ : a ≠ 0
hp : Prime p
ha : P a
⊢ P (p * a)
[PROOFSTEP]
exact h p a hp.nat_prime ha
[GOAL]
a b : ℤ
⊢ Associated a b ↔ natAbs a = natAbs b
[PROOFSTEP]
rw [← dvd_dvd_iff_associated, ← Int.natAbs_dvd_natAbs, ← Int.natAbs_dvd_natAbs, dvd_dvd_iff_associated]
[GOAL]
a b : ℤ
⊢ Associated (natAbs a) (natAbs b) ↔ natAbs a = natAbs b
[PROOFSTEP]
exact associated_iff_eq
[GOAL]
a b : ℤ
⊢ Associated a b ↔ a = b ∨ a = -b
[PROOFSTEP]
rw [Int.associated_iff_natAbs]
[GOAL]
a b : ℤ
⊢ natAbs a = natAbs b ↔ a = b ∨ a = -b
[PROOFSTEP]
exact Int.natAbs_eq_natAbs_iff
[GOAL]
a : ℤ
⊢ Ideal.span {↑(natAbs a)} = Ideal.span {a}
[PROOFSTEP]
rw [Ideal.span_singleton_eq_span_singleton]
[GOAL]
a : ℤ
⊢ Associated (↑(natAbs a)) a
[PROOFSTEP]
exact (associated_natAbs _).symm
[GOAL]
a b c : ℤ
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ bit1 k
⊢ ∃ d, a = d ^ bit1 k
[PROOFSTEP]
obtain ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow' hab h
[GOAL]
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ bit1 k
d : ℤ
hd : Associated (d ^ bit1 k) a
⊢ ∃ d, a = d ^ bit1 k
[PROOFSTEP]
replace hd := hd.symm
[GOAL]
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ bit1 k
d : ℤ
hd : Associated a (d ^ bit1 k)
⊢ ∃ d, a = d ^ bit1 k
[PROOFSTEP]
rw [associated_iff_natAbs, natAbs_eq_natAbs_iff, ← neg_pow_bit1] at hd
[GOAL]
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ bit1 k
d : ℤ
hd : a = d ^ bit1 k ∨ a = (-d) ^ bit1 k
⊢ ∃ d, a = d ^ bit1 k
[PROOFSTEP]
obtain rfl | rfl := hd
[GOAL]
case intro.inl
b c : ℤ
k : ℕ
d : ℤ
hab : IsCoprime (d ^ bit1 k) b
h : d ^ bit1 k * b = c ^ bit1 k
⊢ ∃ d_1, d ^ bit1 k = d_1 ^ bit1 k
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
case intro.inr
b c : ℤ
k : ℕ
d : ℤ
hab : IsCoprime ((-d) ^ bit1 k) b
h : (-d) ^ bit1 k * b = c ^ bit1 k
⊢ ∃ d_1, (-d) ^ bit1 k = d_1 ^ bit1 k
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
a b c : ℤ
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ bit1 k
⊢ b * a = ?m.195121 hab h ^ bit1 k
[PROOFSTEP]
rwa [mul_comm] at h