[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsDomain R
inst✝¹¹ : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Field L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ minpoly K (↑(algebraMap S L) s) = map (algebraMap R K) (minpoly R s)
[PROOFSTEP]
refine' (eq_of_irreducible_of_monic _ _ _).symm
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsDomain R
inst✝¹¹ : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Field L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ Irreducible (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
exact (Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map (monic hs)).1 (irreducible hs)
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsDomain R
inst✝¹¹ : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Field L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ ↑(Polynomial.aeval (↑(algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0
[PROOFSTEP]
rw [aeval_map_algebraMap, aeval_algebraMap_apply, aeval, map_zero]
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsDomain R
inst✝¹¹ : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Field L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
exact (monic hs).map _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : IsDomain R
inst✝¹³ : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
inst✝¹⁰ : IsFractionRing R K
inst✝⁹ : Field L
inst✝⁸ : Algebra R L
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : IsScalarTower R K L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
⊢ minpoly K s = map (algebraMap R K) (minpoly R s)
[PROOFSTEP]
let L := FractionRing S
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : IsDomain R
inst✝¹³ : Algebra R S
K : Type u_3
L✝ : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
inst✝¹⁰ : IsFractionRing R K
inst✝⁹ : Field L✝
inst✝⁸ : Algebra R L✝
inst✝⁷ : Algebra S L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : IsScalarTower R K L✝
inst✝⁴ : IsScalarTower R S L✝
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
L : Type u_2 := FractionRing S
⊢ minpoly K s = map (algebraMap R K) (minpoly R s)
[PROOFSTEP]
rw [← isIntegrallyClosed_eq_field_fractions K L hs]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : IsDomain R
inst✝¹³ : Algebra R S
K : Type u_3
L✝ : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
inst✝¹⁰ : IsFractionRing R K
inst✝⁹ : Field L✝
inst✝⁸ : Algebra R L✝
inst✝⁷ : Algebra S L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : IsScalarTower R K L✝
inst✝⁴ : IsScalarTower R S L✝
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
L : Type u_2 := FractionRing S
⊢ minpoly K s = minpoly K (↑(algebraMap S L) s)
[PROOFSTEP]
refine' minpoly.eq_of_algebraMap_eq (IsFractionRing.injective S L) (isIntegral_of_isScalarTower hs) rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
⊢ minpoly R s ∣ p
[PROOFSTEP]
let K := FractionRing R
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
⊢ minpoly R s ∣ p
[PROOFSTEP]
let L := FractionRing S
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly R s ∣ p
[PROOFSTEP]
have : minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (p %ₘ minpoly R s) :=
  by
  rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]
  refine' dvd_sub (minpoly.dvd K (algebraMap S L s) _) _
  rw [← map_aeval_eq_aeval_map, hp, map_zero]
  rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
  apply dvd_mul_of_dvd_left
  rw [isIntegrallyClosed_eq_field_fractions K L hs]
  exact Monic.map _ (minpoly.monic hs)
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
[PROOFSTEP]
rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣
    map (algebraMap R K) p -
      map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
refine' dvd_sub (minpoly.dvd K (algebraMap S L s) _) _
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ ↑(Polynomial.aeval (↑(algebraMap S L) s)) (map (algebraMap R K) p) = 0
case refine'_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣
    map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
rw [← map_aeval_eq_aeval_map, hp, map_zero]
[GOAL]
case refine'_1.h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ RingHom.comp (algebraMap K ((fun x => L) s)) (algebraMap R K) = RingHom.comp (algebraMap S L) (algebraMap R S)
case refine'_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣
    map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣
    map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
apply dvd_mul_of_dvd_left
[GOAL]
case refine'_2.h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (minpoly R s)
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
rw [isIntegrallyClosed_eq_field_fractions K L hs]
[GOAL]
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
exact Monic.map _ (minpoly.monic hs)
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
⊢ minpoly R s ∣ p
[PROOFSTEP]
rw [isIntegrallyClosed_eq_field_fractions _ _ hs,
  map_dvd_map (algebraMap R K) (IsFractionRing.injective R K) (minpoly.monic hs)] at this
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this✝ : minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
this : minpoly R s ∣ p %ₘ minpoly R s
⊢ minpoly R s ∣ p
[PROOFSTEP]
rw [← dvd_iff_modByMonic_eq_zero (minpoly.monic hs)]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this✝ : minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
this : minpoly R s ∣ p %ₘ minpoly R s
⊢ p %ₘ minpoly R s = 0
[PROOFSTEP]
refine' Polynomial.eq_zero_of_dvd_of_degree_lt this (degree_modByMonic_lt p <| minpoly.monic hs)
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : minpoly R s ∣ p
⊢ ↑(Polynomial.aeval s) p = 0
[PROOFSTEP]
simpa only [RingHom.mem_ker, RingHom.coe_comp, coe_evalRingHom, coe_mapRingHom, Function.comp_apply, eval_map, ←
  aeval_def] using aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s)
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
⊢ RingHom.ker ↑(Polynomial.aeval s) = Ideal.span {minpoly R s}
[PROOFSTEP]
ext p
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
⊢ p ∈ RingHom.ker ↑(Polynomial.aeval s) ↔ p ∈ Ideal.span {minpoly R s}
[PROOFSTEP]
simp_rw [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, isIntegrallyClosed_dvd_iff hs, ←
  Ideal.mem_span_singleton]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : ↑(Polynomial.aeval s) p = 0
⊢ degree (minpoly R s) ≤ degree p
[PROOFSTEP]
rw [degree_eq_natDegree (minpoly.ne_zero hs), degree_eq_natDegree hp0]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : ↑(Polynomial.aeval s) p = 0
⊢ ↑(natDegree (minpoly R s)) ≤ ↑(natDegree p)
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : ↑(Polynomial.aeval s) p = 0
⊢ natDegree (minpoly R s) ≤ natDegree p
[PROOFSTEP]
exact natDegree_le_of_dvd ((isIntegrallyClosed_dvd_iff hs _).mp hp) hp0
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
⊢ P = minpoly R s
[PROOFSTEP]
have hs : IsIntegral R s := ⟨P, hmo, hP⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
⊢ P = minpoly R s
[PROOFSTEP]
symm
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
⊢ minpoly R s = P
[PROOFSTEP]
apply eq_of_sub_eq_zero
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
⊢ minpoly R s - P = 0
[PROOFSTEP]
by_contra hnz
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ False
[PROOFSTEP]
have := IsIntegrallyClosed.degree_le_of_ne_zero hs hnz (by simp [hP])
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ ↑(Polynomial.aeval s) (minpoly R s - P) = 0
[PROOFSTEP]
simp [hP]
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
this : degree (minpoly R s) ≤ degree (minpoly R s - P)
⊢ False
[PROOFSTEP]
contrapose! this
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
this : ¬False
⊢ degree (minpoly R s - P) < degree (minpoly R s)
[PROOFSTEP]
refine' degree_sub_lt _ (ne_zero hs) _
[GOAL]
case h.refine'_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
this : ¬False
⊢ degree (minpoly R s) = degree P
[PROOFSTEP]
exact le_antisymm (min R s hmo hP) (Pmin (minpoly R s) (monic hs) (aeval R s))
[GOAL]
case h.refine'_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
this : ¬False
⊢ leadingCoeff (minpoly R s) = leadingCoeff P
[PROOFSTEP]
rw [(monic hs).leadingCoeff, hmo.leadingCoeff]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
⊢ Prime (minpoly R x)
[PROOFSTEP]
refine'
  ⟨(minpoly.monic hx).ne_zero,
    ⟨fun h_contra => (ne_of_lt (minpoly.degree_pos hx)) (degree_eq_zero_of_isUnit h_contra).symm, fun a b h =>
      or_iff_not_imp_left.mpr fun h' => _⟩⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : minpoly R x ∣ a * b
h' : ¬minpoly R x ∣ a
⊢ minpoly R x ∣ b
[PROOFSTEP]
rw [← minpoly.isIntegrallyClosed_dvd_iff hx] at h' h ⊢
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : ↑(Polynomial.aeval x) (a * b) = 0
h' : ¬↑(Polynomial.aeval x) a = 0
⊢ ↑(Polynomial.aeval x) b = 0
[PROOFSTEP]
rw [aeval_mul] at h
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : ↑(Polynomial.aeval x) a * ↑(Polynomial.aeval x) b = 0
h' : ¬↑(Polynomial.aeval x) a = 0
⊢ ↑(Polynomial.aeval x) b = 0
[PROOFSTEP]
exact eq_zero_of_ne_zero_of_mul_left_eq_zero h' h
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
⊢ Injective ↑(Minpoly.toAdjoin R x)
[PROOFSTEP]
refine' (injective_iff_map_eq_zero _).2 fun P₁ hP₁ => _
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : ↑(Minpoly.toAdjoin R x) P₁ = 0
⊢ P₁ = 0
[PROOFSTEP]
obtain ⟨P, hP⟩ := mk_surjective (minpoly.monic hx) P₁
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : ↑(Minpoly.toAdjoin R x) P₁ = 0
P : R[X]
hP : ↑(AdjoinRoot.mk (minpoly R x)) P = P₁
⊢ P₁ = 0
[PROOFSTEP]
by_cases hPzero : P = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : ↑(Minpoly.toAdjoin R x) P₁ = 0
P : R[X]
hP : ↑(AdjoinRoot.mk (minpoly R x)) P = P₁
hPzero : P = 0
⊢ P₁ = 0
[PROOFSTEP]
simpa [hPzero] using hP.symm
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : ↑(Minpoly.toAdjoin R x) P₁ = 0
P : R[X]
hP : ↑(AdjoinRoot.mk (minpoly R x)) P = P₁
hPzero : ¬P = 0
⊢ P₁ = 0
[PROOFSTEP]
rw [← hP, Minpoly.toAdjoin_apply', liftHom_mk, ← Subalgebra.coe_eq_zero, aeval_subalgebra_coe,
  isIntegrallyClosed_dvd_iff hx] at hP₁
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
P : R[X]
hP₁ : minpoly R x ∣ P
hP : ↑(AdjoinRoot.mk (minpoly R x)) P = P₁
hPzero : ¬P = 0
⊢ P₁ = 0
[PROOFSTEP]
obtain ⟨Q, hQ⟩ := hP₁
[GOAL]
case neg.intro
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
P : R[X]
hP : ↑(AdjoinRoot.mk (minpoly R x)) P = P₁
hPzero : ¬P = 0
Q : R[X]
hQ : P = minpoly R x * Q
⊢ P₁ = 0
[PROOFSTEP]
rw [← hP, hQ, RingHom.map_mul, mk_self, zero_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
⊢ (adjoin.powerBasis' hx).gen = { val := x, property := (_ : x ∈ adjoin R {x}) }
[PROOFSTEP]
rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin, AlgEquiv.ofBijective_apply,
  Minpoly.toAdjoin, liftHom_root]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
B : PowerBasis R S
hint : IsIntegral R x
hx : B.gen ∈ adjoin R {x}
⊢ (PowerBasis.ofGenMemAdjoin' B hint hx).gen = x
[PROOFSTEP]
simp [PowerBasis.ofGenMemAdjoin']


[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
p✝ q✝ : α✝ → Prop
α β : Sort u_4
p : α → Prop
q : β → Prop
a : { x // p x }
b : { y // q y }
h : α = β
h' : HEq p q
⊢ HEq a b ↔ HEq ↑a ↑b
[PROOFSTEP]
subst h
[GOAL]
α✝ : Sort u_1
β : Sort u_2
γ : Sort u_3
p✝ q✝ : α✝ → Prop
α : Sort u_4
p : α → Prop
a : { x // p x }
q : α → Prop
b : { y // q y }
h' : HEq p q
⊢ HEq a b ↔ HEq ↑a ↑b
[PROOFSTEP]
subst h'
[GOAL]
α✝ : Sort u_1
β : Sort u_2
γ : Sort u_3
p✝ q : α✝ → Prop
α : Sort u_4
p : α → Prop
a b : { y // p y }
⊢ HEq a b ↔ HEq ↑a ↑b
[PROOFSTEP]
rw [heq_iff_eq, heq_iff_eq, ext_iff]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
p q : α → Prop
a : Subtype p
b : α
⊢ (∃ h, { val := b, property := h } = a) ↔ b = ↑a
[PROOFSTEP]
simp only [@eq_comm _ b, exists_eq_subtype_mk_iff, @eq_comm _ _ a]
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
p✝ q : α✝ → Prop
α : Sort u_5
β : α → Type u_4
f : (x : α) → β x
p : α → Prop
x : Subtype p
⊢ restrict p f x = f ↑x
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
p✝ q : α✝ → Prop
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
⊢ Surjective fun f => restrict p f
[PROOFSTEP]
letI := Classical.decPred p
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
p✝ q : α✝ → Prop
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
⊢ Surjective fun f => restrict p f
[PROOFSTEP]
refine' fun f ↦ ⟨fun x ↦ if h : p x then f ⟨x, h⟩ else Nonempty.some (ne x), funext <| _⟩
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
p✝ q : α✝ → Prop
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
f : (x : Subtype p) → β ↑x
⊢ ∀ (x : Subtype p),
    (fun f => restrict p f)
        (fun x => if h : p x then f { val := x, property := h } else Nonempty.some (_ : Nonempty (β x))) x =
      f x
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
p✝ q : α✝ → Prop
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
f : (x : Subtype p) → β ↑x
x : α
hx : p x
⊢ (fun f => restrict p f)
      (fun x => if h : p x then f { val := x, property := h } else Nonempty.some (_ : Nonempty (β x)))
      { val := x, property := hx } =
    f { val := x, property := hx }
[PROOFSTEP]
exact dif_pos hx
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
p✝ q : α✝ → Prop
α : Sort u_4
β : Sort u_5
f : α → β
p : β → Prop
h : ∀ (a : α), p (f a)
hf : Injective f
x y : α
hxy : coind f h x = coind f h y
⊢ f x = f y
[PROOFSTEP]
apply congr_arg Subtype.val hxy


[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
⊢ ↑i ≤ 2 * ↑i
[PROOFSTEP]
rw [Nat.succ_mul, Nat.one_mul]
[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
⊢ ↑i ≤ ↑i + ↑i
[PROOFSTEP]
exact Nat.le_add_left i i
[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
left_le : ↑i ≤ left
right_le : ↑i ≤ right
i_le : i ≤ i
j✝ j : { j // i ≤ j }
h : ¬↑i = ↑↑j
a' : Array α := Array.swap a i ↑j
⊢ ↑↑j < Array.size a'
[PROOFSTEP]
rw [a.size_swap i j]
[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
left_le : ↑i ≤ left
right_le : ↑i ≤ right
i_le : i ≤ i
j✝ j : { j // i ≤ j }
h : ¬↑i = ↑↑j
a' : Array α := Array.swap a i ↑j
⊢ ↑↑j < Array.size a
[PROOFSTEP]
exact j.1.2
[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
left_le : ↑i ≤ left
right_le : ↑i ≤ right
i_le : i ≤ i
j✝ j : { j // i ≤ j }
h : ¬↑i = ↑↑j
a' : Array α := Array.swap a i ↑j
j' : Fin (Array.size a') := { val := ↑↑j, isLt := ?m.5009 }
⊢ Array.size a' - ↑↑j < Array.size a - ↑i
[PROOFSTEP]
rw [a.size_swap i j]
[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
left_le : ↑i ≤ left
right_le : ↑i ≤ right
i_le : i ≤ i
j✝ j : { j // i ≤ j }
h : ¬↑i = ↑↑j
a' : Array α := Array.swap a i ↑j
j' : Fin (Array.size a') := { val := ↑↑j, isLt := ?m.5009 }
⊢ Array.size a - ↑↑j < Array.size a - ↑i
[PROOFSTEP]
exact Nat.sub_lt_sub_left i.2 <| Nat.lt_of_le_of_ne j.2 h
[GOAL]
α : Type u_1
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
left_le : ↑i ≤ left
right_le : ↑i ≤ right
i_le : i ≤ i
j : { j // i ≤ j }
h : ¬↑i = ↑↑j
a' : Array α := Array.swap a i ↑j
j' : Fin (Array.size a') := { val := ↑↑j, isLt := (_ : ↑↑j < Array.size a') }
this : Array.size a' - ↑↑j < Array.size a - ↑i
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => Array.size a - ↑snd) instWellFoundedRelation).1
    { fst := a', snd := j' } { fst := a, snd := i }
[PROOFSTEP]
assumption
[GOAL]
α : Type ?u.8277
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
i0 : ¬↑i = 0
this : (↑i - 1) / 2 < ↑i
j : Fin (Array.size a) := { val := (↑i - 1) / 2, isLt := (_ : (↑i - 1) / 2 < Array.size a) }
a' : Array α := Array.swap a i j
⊢ ↑j < Array.size a'
[PROOFSTEP]
rw [a.size_swap i j]
[GOAL]
α : Type ?u.8277
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
i0 : ¬↑i = 0
this : (↑i - 1) / 2 < ↑i
j : Fin (Array.size a) := { val := (↑i - 1) / 2, isLt := (_ : (↑i - 1) / 2 < Array.size a) }
a' : Array α := Array.swap a i j
⊢ ↑j < Array.size a
[PROOFSTEP]
exact j.2
[GOAL]
α : Type u_1
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
i0 : ¬↑i = 0
this : (↑i - 1) / 2 < ↑i
j : Fin (Array.size a) := { val := (↑i - 1) / 2, isLt := (_ : (↑i - 1) / 2 < Array.size a) }
h✝ : lt (Array.get a j) (Array.get a i) = true
a' : Array α := Array.swap a i j
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => ↑snd) instWellFoundedRelation).1
    { fst := a', snd := { val := ↑j, isLt := (_ : ↑j < Array.size a') } } { fst := a, snd := i }
[PROOFSTEP]
assumption
[GOAL]
α : Type ?u.10435
lt : α → α → Bool
self : BinaryHeap α lt
x : α
n : ℕ := size self
⊢ n < Array.size (Array.push self.arr x)
[PROOFSTEP]
rw [Array.size_push]
[GOAL]
α : Type ?u.10435
lt : α → α → Bool
self : BinaryHeap α lt
x : α
n : ℕ := size self
⊢ n < Array.size self.arr + 1
[PROOFSTEP]
apply Nat.lt_succ_self
[GOAL]
α : Type u_1
lt : α → α → Bool
self : BinaryHeap α lt
x : α
⊢ size (insert self x) = size self + 1
[PROOFSTEP]
simp [insert, size, size_heapifyUp]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
e : Array.size self.arr = 0
⊢ size self = size self - 1
[PROOFSTEP]
simp [size, e]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
⊢ 0 < Array.size self.arr
[PROOFSTEP]
rw [e]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
⊢ 0 < Nat.succ n
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
h0 : 0 < Array.size self.arr
⊢ n < Array.size self.arr
[PROOFSTEP]
rw [e]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
h0 : 0 < Array.size self.arr
⊢ n < Nat.succ n
[PROOFSTEP]
apply Nat.lt_succ_self
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
h0 : 0 < Array.size self.arr
hn : n < Array.size self.arr
hn0 : 0 < n
a : Array α := Array.pop (Array.swap self.arr { val := 0, isLt := h0 } { val := n, isLt := hn })
⊢ 0 < Array.size a
[PROOFSTEP]
rwa [Array.size_pop, Array.size_swap, e]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
h0 : 0 < Array.size self.arr
hn : n < Array.size self.arr
hn0 : 0 < n
a : Array α := Array.pop (Array.swap self.arr { val := 0, isLt := h0 } { val := n, isLt := hn })
⊢ size { arr := ↑(heapifyDown lt a { val := 0, isLt := (_ : 0 < Array.size a) }) } = size self - 1
[PROOFSTEP]
simp [size]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
h0 : 0 < Array.size self.arr
hn : n < Array.size self.arr
hn0 : ¬0 < n
⊢ size { arr := Array.pop self.arr } = size self - 1
[PROOFSTEP]
simp [size]
[GOAL]
α : Type u_1
x : α
lt : α → α → Bool
self : BinaryHeap α lt
e : max self = some x
h : ¬0 < Array.size self.arr
⊢ False
[PROOFSTEP]
simp [BinaryHeap.max, Array.get?, h] at e
[GOAL]
α : Type ?u.16836
lt : α → α → Bool
self : BinaryHeap α lt
x m : α
e : max self = some m
a : Array α := Array.set self.arr { val := 0, isLt := (_ : 0 < size self) } x
⊢ 0 < Array.size a
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.16836
lt : α → α → Bool
self : BinaryHeap α lt
x m : α
e : max self = some m
a : Array α := Array.set self.arr { val := 0, isLt := (_ : 0 < size self) } x
⊢ 0 < Array.size self.arr
[PROOFSTEP]
exact size_pos_of_max e
[GOAL]
α : Type ?u.18030
lt : α → α → Bool
self : BinaryHeap α lt
x m : α
e : max self = some m
a : Array α := Array.set self.arr { val := 0, isLt := (_ : 0 < size self) } x
⊢ 0 < Array.size a
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.18030
lt : α → α → Bool
self : BinaryHeap α lt
x m : α
e : max self = some m
a : Array α := Array.set self.arr { val := 0, isLt := (_ : 0 < size self) } x
⊢ 0 < Array.size self.arr
[PROOFSTEP]
exact size_pos_of_max e
[GOAL]
α : Type ?u.19048
lt : α → α → Bool
self : BinaryHeap α lt
i : Fin (size self)
x : α
⊢ ↑i < Array.size (Array.set self.arr i x)
[PROOFSTEP]
rw [self.1.size_set]
[GOAL]
α : Type ?u.19048
lt : α → α → Bool
self : BinaryHeap α lt
i : Fin (size self)
x : α
⊢ ↑i < Array.size self.arr
[PROOFSTEP]
exact i.2
[GOAL]
α : Type ?u.19626
lt : α → α → Bool
self : BinaryHeap α lt
i : Fin (size self)
x : α
⊢ ↑i < Array.size (Array.set self.arr i x)
[PROOFSTEP]
rw [self.1.size_set]
[GOAL]
α : Type ?u.19626
lt : α → α → Bool
self : BinaryHeap α lt
i : Fin (size self)
x : α
⊢ ↑i < Array.size self.arr
[PROOFSTEP]
exact i.2
[GOAL]
α : Type ?u.20451
a✝ : Array α
lt : α → α → Bool
gt : α → α → Bool := fun y x => lt x y
a : BinaryHeap α gt
out : Array α
x : α
e : BinaryHeap.max a = some x
⊢ BinaryHeap.size (BinaryHeap.popMax a) < BinaryHeap.size a
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.20451
a✝ : Array α
lt : α → α → Bool
gt : α → α → Bool := fun y x => lt x y
a : BinaryHeap α gt
out : Array α
x : α
e : BinaryHeap.max a = some x
⊢ BinaryHeap.size a - 1 < BinaryHeap.size a
[PROOFSTEP]
exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
[GOAL]
α : Type u_1
lt : α → α → Bool
a : BinaryHeap α fun y x => lt x y
out : Array α
gt : α → α → Bool := fun y x => lt x y
x : α
e : BinaryHeap.max a = some x
this : BinaryHeap.size (BinaryHeap.popMax a) < BinaryHeap.size a
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => BinaryHeap.size a) instWellFoundedRelation).1
    { fst := BinaryHeap.popMax a, snd := push out x } { fst := a, snd := out }
[PROOFSTEP]
assumption


[GOAL]
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (succ n)
⊢ α
[PROOFSTEP]
refine' i.cases' _ _
[GOAL]
case refine'_1
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (succ n)
⊢ α
case refine'_2 α : Type u_1 m n : ℕ a : α v : Vector3 α n i : Fin2 (succ n) ⊢ Fin2 n → α
[PROOFSTEP]
exact a
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (succ n)
⊢ Fin2 n → α
[PROOFSTEP]
exact v
[GOAL]
α : Type u_1
m n : ℕ
C : Vector3 α 0 → Sort u
H : C []
v : Vector3 α 0
⊢ C v
[PROOFSTEP]
rw [eq_nil v]
[GOAL]
α : Type u_1
m n : ℕ
C : Vector3 α 0 → Sort u
H : C []
v : Vector3 α 0
⊢ C []
[PROOFSTEP]
apply H
[GOAL]
α : Type u_1
m n : ℕ
C : Vector3 α (succ n) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (succ n)
⊢ C v
[PROOFSTEP]
rw [← cons_head_tail v]
[GOAL]
α : Type u_1
m n : ℕ
C : Vector3 α (succ n) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (succ n)
⊢ C (head v :: tail v)
[PROOFSTEP]
apply H
[GOAL]
α : Type u_1
m✝ n✝ m : ℕ
v : Vector3 α (succ m)
n : ℕ
w : Vector3 α n
a : α
_t : Vector3 α m
⊢ ((a :: _t) +-+ w) (left n fz) = (a :: _t) fz
[PROOFSTEP]
simp [*, left]
[GOAL]
α : Type u_1
m✝ n✝ m : ℕ
i : Fin2 m
v : Vector3 α (succ m)
n : ℕ
w : Vector3 α n
_a : α
t : Vector3 α m
⊢ ((_a :: t) +-+ w) (left n (fs i)) = (_a :: t) (fs i)
[PROOFSTEP]
simp [append_left, left]
[GOAL]
α : Type u_1
m✝ n✝ m : ℕ
v : Vector3 α (succ m)
n : ℕ
w : Vector3 α n
i : Fin2 n
_a : α
t : Vector3 α m
⊢ ((_a :: t) +-+ w) (add i (succ m)) = w i
[PROOFSTEP]
simp [append_add, add]
[GOAL]
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
⊢ insert a v fz = a :: v
[PROOFSTEP]
refine' funext fun j => j.cases' _ _
[GOAL]
case refine'_1
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
j : Fin2 (succ n)
⊢ insert a v fz fz = (a :: v) fz
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
j : Fin2 (succ n)
⊢ ∀ (n_1 : Fin2 n), insert a v fz (fs n_1) = (a :: v) (fs n_1)
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
j : Fin2 (succ n)
⊢ insert a v fz fz = (a :: v) fz
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
j : Fin2 (succ n)
n✝ : Fin2 n
⊢ insert a v fz (fs n✝) = (a :: v) (fs n✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
m n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (succ n)
j : Fin2 (succ (succ n))
⊢ insert a (b :: v) (fs i) j = (b :: insert a v i) j
[PROOFSTEP]
refine' j.cases' _ fun j => _
[GOAL]
case refine'_1
α : Type u_1
m n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (succ n)
j : Fin2 (succ (succ n))
⊢ insert a (b :: v) (fs i) fz = (b :: insert a v i) fz
[PROOFSTEP]
simp [insert, insertPerm]
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (succ n)
j✝ : Fin2 (succ (succ n))
j : Fin2 (n + 1)
⊢ insert a (b :: v) (fs i) (fs j) = (b :: insert a v i) (fs j)
[PROOFSTEP]
simp [insert, insertPerm]
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (succ n)
j✝ : Fin2 (succ (succ n))
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match insertPerm i j with
      | fz => fz
      | fs k => fs (fs k)) =
    (a :: v) (insertPerm i j)
[PROOFSTEP]
refine' Fin2.cases' _ _ (insertPerm i j)
[GOAL]
case refine'_2.refine'_1
α : Type u_1
m n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (succ n)
j✝ : Fin2 (succ (succ n))
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match fz with
      | fz => fz
      | fs k => fs (fs k)) =
    (a :: v) fz
[PROOFSTEP]
simp [insertPerm]
[GOAL]
case refine'_2.refine'_2
α : Type u_1
m n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (succ n)
j✝ : Fin2 (succ (succ n))
j : Fin2 (n + 1)
⊢ ∀ (n_1 : Fin2 n),
    (a :: b :: v)
        (match fs n_1 with
        | fz => fz
        | fs k => fs (fs k)) =
      (a :: v) (fs n_1)
[PROOFSTEP]
simp [insertPerm]
[GOAL]
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
⊢ insert a (t +-+ v) (Eq.recOn e (add i m)) = Eq.recOn e (t +-+ insert a v i)
[PROOFSTEP]
refine' Vector3.recOn t (fun e => _) (@fun k b t IH _ => _) e
[GOAL]
case refine'_1
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e✝ : succ n + m = succ (n + m)
e : succ n + 0 = succ (n + 0)
⊢ insert a ([] +-+ v) (Eq.recOn e (add i 0)) = Eq.recOn e ([] +-+ insert a v i)
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (add i (succ k))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (add i (succ k))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
[PROOFSTEP]
have e' := succ_add n k
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (add i (succ k))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
[PROOFSTEP]
change
  insert a (b :: t +-+ v) (Eq.recOn (congr_arg succ e') (fs (add i k))) =
    Eq.recOn (congr_arg succ e') (b :: t +-+ insert a v i)
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ insert a (b :: t +-+ v) (Eq.recOn (_ : succ (succ n + k) = succ (succ (n + k))) (fs (add i k))) =
    Eq.recOn (_ : succ (succ n + k) = succ (succ (n + k))) (b :: t +-+ insert a v i)
[PROOFSTEP]
rw [←
  (Eq.recOn e' rfl : fs (Eq.recOn e' (i.add k) : Fin2 (succ (n + k))) = Eq.recOn (congr_arg succ e') (fs (i.add k)))]
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ insert a (b :: t +-+ v) (fs (Eq.recOn e' (add i k))) =
    Eq.recOn (_ : succ (succ n + k) = succ (succ (n + k))) (b :: t +-+ insert a v i)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ (b :: insert a (t +-+ v) (e' ▸ add i k)) = (_ : succ (succ n + k) = succ (succ (n + k))) ▸ b :: t +-+ insert a v i
[PROOFSTEP]
rw [IH]
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (succ n)
e : succ n + m = succ (n + m)
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : succ n + k = succ (n + k)), insert a (t +-+ v) (Eq.recOn x (add i k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : succ n + succ k = succ (n + succ k)
e' : succ n + k = succ (n + k)
⊢ (b :: Eq.recOn e' (t +-+ insert a v i)) = (_ : succ (succ n + k) = succ (succ (n + k))) ▸ b :: t +-+ insert a v i
[PROOFSTEP]
exact Eq.recOn e' rfl
[GOAL]
α : Type u_1
m n : ℕ
f : Vector3 α 0 → Prop
x✝ : Exists f
v : Vector3 α 0
fv : f v
⊢ f []
[PROOFSTEP]
rw [← eq_nil v]
[GOAL]
α : Type u_1
m n : ℕ
f : Vector3 α 0 → Prop
x✝ : Exists f
v : Vector3 α 0
fv : f v
⊢ f v
[PROOFSTEP]
exact fv
[GOAL]
α : Type u_1
m n : ℕ
f : Vector3 α (succ n) → Prop
x✝ : Exists f
v : Vector3 α (succ n)
fv : f v
⊢ f (?m.40396 f x✝ v fv :: ?m.40397 f x✝ v fv)
[PROOFSTEP]
rw [cons_head_tail v]
[GOAL]
α : Type u_1
m n : ℕ
f : Vector3 α (succ n) → Prop
x✝ : Exists f
v : Vector3 α (succ n)
fv : f v
⊢ f v
[PROOFSTEP]
exact fv
[GOAL]
α : Type u_1
m n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
[PROOFSTEP]
refine' v.recOn _ _
[GOAL]
case refine'_1
α : Type u_1
m n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p [] ↔ ∀ (i : Fin2 0), p []
[PROOFSTEP]
exact ⟨fun _ => Fin2.elim0, fun _ => trivial⟩
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (VectorAllP p (a :: w) ↔ ∀ (i : Fin2 (succ n)), p ((a :: w) i))
[PROOFSTEP]
simp only [vectorAllP_cons]
[GOAL]
case refine'_2
α : Type u_1
m n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (p a ∧ VectorAllP p w ↔ ∀ (i : Fin2 (succ n)), p ((a :: w) i))
[PROOFSTEP]
refine' fun {n} a v IH =>
  (and_congr_right fun _ => IH).trans
    ⟨fun ⟨pa, h⟩ i => by
      refine' i.cases' _ _
      exacts [pa, h], fun h => ⟨_, fun i => _⟩⟩
[GOAL]
α : Type u_1
m n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (succ n)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) i)
[PROOFSTEP]
refine' i.cases' _ _
[GOAL]
case refine'_1
α : Type u_1
m n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (succ n)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) fz)
case refine'_2
α : Type u_1
m n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (succ n)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ ∀ (n_1 : Fin2 n), p ((a :: v) (fs n_1))
[PROOFSTEP]
exacts [pa, h]
[GOAL]
case refine'_2.refine'_1
α : Type u_1
m n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (succ n)), p ((a :: v) i)
⊢ p a
[PROOFSTEP]
simpa using h fz
[GOAL]
case refine'_2.refine'_2
α : Type u_1
m n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (succ n)), p ((a :: v) i)
i : Fin2 n
⊢ p (v i)
[PROOFSTEP]
simpa using h (fs i)