[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → ↑x j ≤ ↑y j ∧ ↑y j ≤ ↑x j) ∧ ↑x i < ↑y i
[PROOFSTEP]
obtain ⟨hle, j, hlt⟩ := Pi.lt_def.1 hlt
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : (fun i => ↑x i) ≤ fun i => ↑y i
j : ι
hlt : ↑x j < ↑y j
⊢ ∃ i, (∀ (j : ι), r j i → ↑x j ≤ ↑y j ∧ ↑y j ≤ ↑x j) ∧ ↑x i < ↑y i
[PROOFSTEP]
classical
have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
obtain ⟨i, hi, hl⟩ := this.has_min {i | x i < y i} ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
refine' ⟨i, fun k hk ↦ ⟨hle k, _⟩, hi⟩
exact of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_le h) hk
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : (fun i => ↑x i) ≤ fun i => ↑y i
j : ι
hlt : ↑x j < ↑y j
⊢ ∃ i, (∀ (j : ι), r j i → ↑x j ≤ ↑y j ∧ ↑y j ≤ ↑x j) ∧ ↑x i < ↑y i
[PROOFSTEP]
have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : (fun i => ↑x i) ≤ fun i => ↑y i
j : ι
hlt : ↑x j < ↑y j
this : Set.WellFoundedOn (↑(neLocus x y)) r
⊢ ∃ i, (∀ (j : ι), r j i → ↑x j ≤ ↑y j ∧ ↑y j ≤ ↑x j) ∧ ↑x i < ↑y i
[PROOFSTEP]
obtain ⟨i, hi, hl⟩ := this.has_min {i | x i < y i} ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : (fun i => ↑x i) ≤ fun i => ↑y i
j : ι
hlt : ↑x j < ↑y j
this : Set.WellFoundedOn (↑(neLocus x y)) r
i : ↑↑(neLocus x y)
hi : i ∈ {i | ↑x ↑i < ↑y ↑i}
hl : ∀ (x_1 : ↑↑(neLocus x y)), x_1 ∈ {i | ↑x ↑i < ↑y ↑i} → ¬r ↑x_1 ↑i
⊢ ∃ i, (∀ (j : ι), r j i → ↑x j ≤ ↑y j ∧ ↑y j ≤ ↑x j) ∧ ↑x i < ↑y i
[PROOFSTEP]
refine' ⟨i, fun k hk ↦ ⟨hle k, _⟩, hi⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : (fun i => ↑x i) ≤ fun i => ↑y i
j : ι
hlt : ↑x j < ↑y j
this : Set.WellFoundedOn (↑(neLocus x y)) r
i : ↑↑(neLocus x y)
hi : i ∈ {i | ↑x ↑i < ↑y ↑i}
hl : ∀ (x_1 : ↑↑(neLocus x y)), x_1 ∈ {i | ↑x ↑i < ↑y ↑i} → ¬r ↑x_1 ↑i
k : ι
hk : r k ↑i
⊢ ↑y k ≤ ↑x k
[PROOFSTEP]
exact of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_le h) hk
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ Pi.Lex r (fun {i} x x_1 => x < x_1) ↑x ↑y
[PROOFSTEP]
simp_rw [Pi.Lex, le_antisymm_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → ↑x j ≤ ↑y j ∧ ↑y j ≤ ↑x j) ∧ ↑x i < ↑y i
[PROOFSTEP]
exact lex_lt_of_lt_of_preorder r hlt
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
⊢ P (↑toLex f) (↑toLex g)
[PROOFSTEP]
apply (mem_neLocus.mp <| Finset.mem_of_min h).lt_or_lt.by_cases
[GOAL]
case h₁
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
⊢ ↑f wit < ↑g wit → P (↑toLex f) (↑toLex g)
[PROOFSTEP]
intro hwit
[GOAL]
case h₂
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
⊢ ↑g wit < ↑f wit → P (↑toLex f) (↑toLex g)
[PROOFSTEP]
intro hwit
[GOAL]
case h₁
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
hwit : ↑f wit < ↑g wit
⊢ P (↑toLex f) (↑toLex g)
[PROOFSTEP]
exact h_lt ⟨wit, fun j hj ↦ not_mem_neLocus.mp (Finset.not_mem_of_lt_min hj h), hwit⟩
[GOAL]
case h₂
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
hwit : ↑g wit < ↑f wit
⊢ P (↑toLex f) (↑toLex g)
[PROOFSTEP]
exact h_gt ⟨wit, fun j hj ↦ not_mem_neLocus.mp (Finset.not_mem_of_lt_min hj <| by rwa [neLocus_comm]), hwit⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
hwit : ↑g wit < ↑f wit
j : ι
hj : (fun x x_1 => x < x_1) j wit
⊢ Finset.min (neLocus (↑ofLex (↑toLex g)) (↑ofLex (↑toLex f))) = ↑wit
[PROOFSTEP]
rwa [neLocus_comm]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
⊢ Monotone ↑toLex
[PROOFSTEP]
intro a b h
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
⊢ ↑toLex a ≤ ↑toLex b
[PROOFSTEP]
refine' le_of_lt_or_eq (or_iff_not_imp_right.2 fun hne ↦ _)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬↑toLex a = ↑toLex b
⊢ ↑toLex a < ↑toLex b
[PROOFSTEP]
classical exact
  ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne), fun j hj ↦ not_mem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_lt hj,
    (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬↑toLex a = ↑toLex b
⊢ ↑toLex a < ↑toLex b
[PROOFSTEP]
exact
  ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne), fun j hj ↦ not_mem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_lt hj,
    (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩


[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ Irreducible (factor f)
[PROOFSTEP]
rw [factor]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ Irreducible (if H : ∃ g, Irreducible g ∧ g ∣ f then Classical.choose H else X)
[PROOFSTEP]
split_ifs with H
[GOAL]
case pos
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
H : ∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible (Classical.choose H)
[PROOFSTEP]
exact (Classical.choose_spec H).1
[GOAL]
case neg
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
H : ¬∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible X
[PROOFSTEP]
exact irreducible_X
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf1 : ¬IsUnit f
⊢ factor f ∣ f
[PROOFSTEP]
by_cases hf2 : f = 0
[GOAL]
case pos
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ factor f ∣ f
[PROOFSTEP]
rw [hf2]
[GOAL]
case pos
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ factor 0 ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
case neg
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ factor f ∣ f
[PROOFSTEP]
rw [factor, dif_pos (WfDvdMonoid.exists_irreducible_factor hf1 hf2)]
[GOAL]
case neg
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ Classical.choose (_ : ∃ i, Irreducible i ∧ i ∣ f) ∣ f
[PROOFSTEP]
exact (Classical.choose_spec <| WfDvdMonoid.exists_irreducible_factor hf1 hf2).2
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf : natDegree f ≠ 0
⊢ (X - ↑C (AdjoinRoot.root (factor f))) * removeFactor f = map (AdjoinRoot.of (factor f)) f
[PROOFSTEP]
let ⟨g, hg⟩ := factor_dvd_of_natDegree_ne_zero hf
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf : natDegree f ≠ 0
g : K[X]
hg : f = factor f * g
⊢ (X - ↑C (AdjoinRoot.root (factor f))) * removeFactor f = map (AdjoinRoot.of (factor f)) f
[PROOFSTEP]
apply (mul_divByMonic_eq_iff_isRoot (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor)).mpr
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf : natDegree f ≠ 0
g : K[X]
hg : f = factor f * g
⊢ IsRoot (map (AdjoinRoot.of (factor f)) f) (AdjoinRoot.root (factor f))
[PROOFSTEP]
rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ natDegree (removeFactor f) = natDegree f - 1
[PROOFSTEP]
rw [removeFactor, natDegree_divByMonic (map (AdjoinRoot.of f.factor) f) (monic_X_sub_C _), natDegree_map,
  natDegree_X_sub_C]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
n : ℕ
hfn : natDegree f = n + 1
⊢ natDegree (removeFactor f) = n
[PROOFSTEP]
rw [natDegree_removeFactor, hfn, n.add_sub_cancel]
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), natDegree f = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : natDegree f = Nat.succ n
⊢ Splits (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f
[PROOFSTEP]
rw [← splits_id_iff_splits, algebraMap_succ, ← map_map, splits_id_iff_splits, ←
  X_sub_C_mul_removeFactor f fun h => by rw [h] at hf ; cases hf]
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), natDegree f = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : natDegree f = Nat.succ n
h : natDegree f = 0
⊢ False
[PROOFSTEP]
rw [h] at hf
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), natDegree f = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : 0 = Nat.succ n
h : natDegree f = 0
⊢ False
[PROOFSTEP]
cases hf
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), natDegree f = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : natDegree f = Nat.succ n
⊢ Splits (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
    ((X - ↑C (AdjoinRoot.root (factor f))) * removeFactor f)
[PROOFSTEP]
exact splits_mul _ (splits_X_sub_C _) (ih _ (natDegree_removeFactor' hf))
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
⊢ Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f))) = ⊤
[PROOFSTEP]
have hndf : f.natDegree ≠ 0 := by intro h; rw [h] at hfn ; cases hfn
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
⊢ natDegree f ≠ 0
[PROOFSTEP]
intro h
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
h : natDegree f = 0
⊢ False
[PROOFSTEP]
rw [h] at hfn
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : 0 = Nat.succ n
h : natDegree f = 0
⊢ False
[PROOFSTEP]
cases hfn
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
⊢ Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f))) = ⊤
[PROOFSTEP]
have hfn0 : f ≠ 0 := by intro h; rw [h] at hndf ; exact hndf rfl
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
⊢ f ≠ 0
[PROOFSTEP]
intro h
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
h : f = 0
⊢ False
[PROOFSTEP]
rw [h] at hndf
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree 0 ≠ 0
h : f = 0
⊢ False
[PROOFSTEP]
exact hndf rfl
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
⊢ Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f))) = ⊤
[PROOFSTEP]
have hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0 := map_ne_zero hfn0
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
hmf0 : map (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f ≠ 0
⊢ Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f))) = ⊤
[PROOFSTEP]
rw [algebraMap_succ, ← map_map, ← X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
        (X - ↑C (AdjoinRoot.root (factor f))) *
      map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f) ≠
    0
⊢ Algebra.adjoin K
      ↑(Multiset.toFinset
          (roots
            (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
                (X - ↑C (AdjoinRoot.root (factor f))) *
              map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f)))) =
    ⊤
[PROOFSTEP]
rw [roots_mul hmf0, Polynomial.map_sub, map_X, map_C, roots_X_sub_C, Multiset.toFinset_add, Finset.coe_union,
  Multiset.toFinset_singleton, Finset.coe_singleton, Algebra.adjoin_union_eq_adjoin_adjoin, ← Set.image_singleton,
  Algebra.adjoin_algebraMap K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor), AdjoinRoot.adjoinRoot_eq_top,
  Algebra.map_top]
  /- Porting note: was `rw [IsScalarTower.adjoin_range_toAlgHom K (AdjoinRoot f.factor)
          (SplittingFieldAux n f.removeFactor)]` -/
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
        (X - ↑C (AdjoinRoot.root (factor f))) *
      map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f) ≠
    0
⊢ Subalgebra.restrictScalars K
      (Algebra.adjoin
        { x //
          x ∈ AlgHom.range (IsScalarTower.toAlgHom K (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) }
        ↑(Multiset.toFinset
            (roots
              (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f))))) =
    ⊤
[PROOFSTEP]
have :=
  IsScalarTower.adjoin_range_toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)
    (↑(f.removeFactor.map <| algebraMap (AdjoinRoot f.factor) <| SplittingFieldAux n f.removeFactor).roots.toFinset :
      Set (SplittingFieldAux n f.removeFactor))
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
        (X - ↑C (AdjoinRoot.root (factor f))) *
      map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f) ≠
    0
this :
  Subalgebra.restrictScalars K
      (Algebra.adjoin
        { x //
          x ∈ AlgHom.range (IsScalarTower.toAlgHom K (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) }
        ↑(Multiset.toFinset
            (roots
              (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f))))) =
    Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot (factor f))
        ↑(Multiset.toFinset
            (roots (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f)))))
⊢ Subalgebra.restrictScalars K
      (Algebra.adjoin
        { x //
          x ∈ AlgHom.range (IsScalarTower.toAlgHom K (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) }
        ↑(Multiset.toFinset
            (roots
              (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f))))) =
    ⊤
[PROOFSTEP]
refine this.trans ?_
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
        (X - ↑C (AdjoinRoot.root (factor f))) *
      map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f) ≠
    0
this :
  Subalgebra.restrictScalars K
      (Algebra.adjoin
        { x //
          x ∈ AlgHom.range (IsScalarTower.toAlgHom K (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) }
        ↑(Multiset.toFinset
            (roots
              (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f))))) =
    Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot (factor f))
        ↑(Multiset.toFinset
            (roots (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f)))))
⊢ Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot (factor f))
        ↑(Multiset.toFinset
            (roots
              (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f))))) =
    ⊤
[PROOFSTEP]
rw [ih _ (natDegree_removeFactor' hfn), Subalgebra.restrictScalars_top]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ Function.Surjective ↑(ofMvPolynomial f)
[PROOFSTEP]
suffices AlgHom.range (ofMvPolynomial f) = ⊤ by rw [← Set.range_iff_surjective]; rwa [SetLike.ext'_iff] at this
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
this : AlgHom.range (ofMvPolynomial f) = ⊤
⊢ Function.Surjective ↑(ofMvPolynomial f)
[PROOFSTEP]
rw [← Set.range_iff_surjective]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
this : AlgHom.range (ofMvPolynomial f) = ⊤
⊢ Set.range ↑(ofMvPolynomial f) = Set.univ
[PROOFSTEP]
rwa [SetLike.ext'_iff] at this
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ AlgHom.range (ofMvPolynomial f) = ⊤
[PROOFSTEP]
rw [ofMvPolynomial, ← Algebra.adjoin_range_eq_range_aeval K, eq_top_iff, ← adjoin_rootSet _ _ rfl]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ Algebra.adjoin K (rootSet f (SplittingFieldAux (natDegree f) f)) ≤ Algebra.adjoin K (Set.range fun i => ↑i)
[PROOFSTEP]
apply Algebra.adjoin_le
[GOAL]
case H
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ rootSet f (SplittingFieldAux (natDegree f) f) ⊆ ↑(Algebra.adjoin K (Set.range fun i => ↑i))
[PROOFSTEP]
intro α hα
[GOAL]
case H
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
α : SplittingFieldAux (natDegree f) f
hα : α ∈ rootSet f (SplittingFieldAux (natDegree f) f)
⊢ α ∈ ↑(Algebra.adjoin K (Set.range fun i => ↑i))
[PROOFSTEP]
apply Algebra.subset_adjoin
[GOAL]
case H.a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
α : SplittingFieldAux (natDegree f) f
hα : α ∈ rootSet f (SplittingFieldAux (natDegree f) f)
⊢ α ∈ Set.range fun i => ↑i
[PROOFSTEP]
exact ⟨⟨α, hα⟩, rfl⟩
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
apply_fun e
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
⊢ ↑e (a * a⁻¹) = ↑e 1
[PROOFSTEP]
have : e a ≠ 0 := fun w' => by
  apply w
  simp at w'
  exact w'
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
w' : ↑e a = 0
⊢ False
[PROOFSTEP]
apply w
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
w' : ↑e a = 0
⊢ a = 0
[PROOFSTEP]
simp at w'
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
w' : a = 0
⊢ a = 0
[PROOFSTEP]
exact w'
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
this : ↑e a ≠ 0
⊢ ↑e (a * a⁻¹) = ↑e 1
[PROOFSTEP]
simp only [map_mul, AlgEquiv.apply_symm_apply, ne_eq, AddEquivClass.map_eq_zero_iff, map_one]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
this : ↑e a ≠ 0
⊢ ↑(algEquivSplittingFieldAux f) a * (↑(algEquivSplittingFieldAux f) a)⁻¹ = 1
[PROOFSTEP]
rw [mul_inv_cancel]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
this : ↑e a ≠ 0
⊢ ↑(algEquivSplittingFieldAux f) a ≠ 0
[PROOFSTEP]
assumption
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
⊢ 0⁻¹ = 0
[PROOFSTEP]
simp
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
[PROOFSTEP]
apply_fun e
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑e ↑(Rat.mk' a b) = ↑e (↑a * (↑b)⁻¹)
[PROOFSTEP]
change e (algebraMap K _ _) = _
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑e (↑(algebraMap K (SplittingField f)) ↑(Rat.mk' a b)) = ↑e (↑a * (↑b)⁻¹)
[PROOFSTEP]
simp only [map_ratCast, map_natCast, map_mul, map_intCast, AlgEquiv.commutes, AlgEquiv.apply_symm_apply]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
[PROOFSTEP]
apply Field.ratCast_mk
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℚ
x : SplittingField f
p : MvPolynomial (↑(rootSet f (SplittingFieldAux (natDegree f) f))) K
⊢ (fun x x_1 => x • x_1) a p =
    (fun x x_1 => x * x_1) (↑(algebraMap K (MvPolynomial (↑(rootSet f (SplittingFieldAux (natDegree f) f))) K)) ↑a) p
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℚ
x : SplittingField f
p : MvPolynomial (↑(rootSet f (SplittingFieldAux (natDegree f) f))) K
m✝ : ↑(rootSet f (SplittingFieldAux (natDegree f) f)) →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((fun x x_1 => x • x_1) a p) =
    MvPolynomial.coeff m✝
      ((fun x x_1 => x * x_1) (↑(algebraMap K (MvPolynomial (↑(rootSet f (SplittingFieldAux (natDegree f) f))) K)) ↑a)
        p)
[PROOFSTEP]
simp [MvPolynomial.algebraMap_eq, Rat.smul_def]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
⊢ L ≃ₐ[K] SplittingField f
[PROOFSTEP]
refine'
  AlgEquiv.ofBijective (lift L f <| splits (SplittingField f) f)
    ⟨RingHom.injective (lift L f <| splits (SplittingField f) f).toRingHom, _⟩
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
⊢ Function.Surjective ↑(lift L f (_ : Splits (algebraMap K (SplittingField f)) f))
[PROOFSTEP]
haveI := finiteDimensional (SplittingField f) f
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
this : FiniteDimensional K (SplittingField f)
⊢ Function.Surjective ↑(lift L f (_ : Splits (algebraMap K (SplittingField f)) f))
[PROOFSTEP]
haveI := finiteDimensional L f
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
this✝ : FiniteDimensional K (SplittingField f)
this : FiniteDimensional K L
⊢ Function.Surjective ↑(lift L f (_ : Splits (algebraMap K (SplittingField f)) f))
[PROOFSTEP]
have : FiniteDimensional.finrank K L = FiniteDimensional.finrank K (SplittingField f) :=
  le_antisymm
    (LinearMap.finrank_le_finrank_of_injective
      (show Function.Injective (lift L f <| splits (SplittingField f) f).toLinearMap from
        RingHom.injective (lift L f <| splits (SplittingField f) f : L →+* f.SplittingField)))
    (LinearMap.finrank_le_finrank_of_injective
      (show Function.Injective (lift (SplittingField f) f <| splits L f).toLinearMap from
        RingHom.injective (lift (SplittingField f) f <| splits L f : f.SplittingField →+* L)))
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
this✝¹ : FiniteDimensional K (SplittingField f)
this✝ : FiniteDimensional K L
this : FiniteDimensional.finrank K L = FiniteDimensional.finrank K (SplittingField f)
⊢ Function.Surjective ↑(lift L f (_ : Splits (algebraMap K (SplittingField f)) f))
[PROOFSTEP]
change Function.Surjective (lift L f <| splits (SplittingField f) f).toLinearMap
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
this✝¹ : FiniteDimensional K (SplittingField f)
this✝ : FiniteDimensional K L
this : FiniteDimensional.finrank K L = FiniteDimensional.finrank K (SplittingField f)
⊢ Function.Surjective ↑(AlgHom.toLinearMap (lift L f (_ : Splits (algebraMap K (SplittingField f)) f)))
[PROOFSTEP]
refine' (LinearMap.injective_iff_surjective_of_finrank_eq_finrank this).1 _
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
this✝¹ : FiniteDimensional K (SplittingField f)
this✝ : FiniteDimensional K L
this : FiniteDimensional.finrank K L = FiniteDimensional.finrank K (SplittingField f)
⊢ Function.Injective ↑(AlgHom.toLinearMap (lift L f (_ : Splits (algebraMap K (SplittingField f)) f)))
[PROOFSTEP]
exact RingHom.injective (lift L f <| splits (SplittingField f) f : L →+* f.SplittingField)


[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LE (α i)
⊢ ∀ {a b : Π₀ (i : ι), α i},
    ↑{ toFun := FunLike.coe, inj' := (_ : Function.Injective fun f => ↑f) } a ≤
        ↑{ toFun := FunLike.coe, inj' := (_ : Function.Injective fun f => ↑f) } b ↔
      a ≤ b
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (↑(support (f ⊓ g) ∪ support (f ⊔ g)))ᶜ = (↑(support f ∪ support g))ᶜ
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x✝ : ι
⊢ x✝ ∈ (↑(support (f ⊓ g) ∪ support (f ⊔ g)))ᶜ ↔ x✝ ∈ (↑(support f ∪ support g))ᶜ
[PROOFSTEP]
simp [inf_eq_and_sup_eq_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
⊢ ∀ (a : Π₀ (i : ι), α i), ⊥ ≤ a
[PROOFSTEP]
simp only [le_def, coe_zero, Pi.zero_apply, imp_true_iff, zero_le]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
f g : Π₀ (i : ι), α i
⊢ f + g = 0 ↔ f = 0 ∧ g = 0
[PROOFSTEP]
simp [FunLike.ext_iff, forall_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
s : Finset ι
i : ι
a : α i
⊢ (∀ (i_1 : ι), i_1 ∈ {i} → ↑(single i a) i_1 ≤ ↑f i_1) ↔ a ≤ ↑f i
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i : ι
a b : α i
f g : Π₀ (i : ι), α i
⊢ ↑(f - g) = ↑f - ↑g
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a b : α i✝
f g : Π₀ (i : ι), α i
i : ι
⊢ ↑(f - g) i = (↑f - ↑g) i
[PROOFSTEP]
exact tsub_apply f g i
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
src✝¹ : OrderBot (DFinsupp α) := inferInstance
src✝ : OrderedAddCommMonoid (DFinsupp α) := inferInstance
⊢ ∀ {a b : Π₀ (i : ι), α i}, a ≤ b → ∃ c, b = a + c
[PROOFSTEP]
intro f g h
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i : ι
a b : α i
src✝¹ : OrderBot (DFinsupp α) := inferInstance
src✝ : OrderedAddCommMonoid (DFinsupp α) := inferInstance
f g : Π₀ (i : ι), α i
h : f ≤ g
⊢ ∃ c, g = f + c
[PROOFSTEP]
exists g - f
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i : ι
a b : α i
src✝¹ : OrderBot (DFinsupp α) := inferInstance
src✝ : OrderedAddCommMonoid (DFinsupp α) := inferInstance
f g : Π₀ (i : ι), α i
h : f ≤ g
⊢ g = f + (g - f)
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a b : α i✝
src✝¹ : OrderBot (DFinsupp α) := inferInstance
src✝ : OrderedAddCommMonoid (DFinsupp α) := inferInstance
f g : Π₀ (i : ι), α i
h : f ≤ g
i : ι
⊢ ↑g i = ↑(f + (g - f)) i
[PROOFSTEP]
exact (add_tsub_cancel_of_le <| h i).symm
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
⊢ single i (a - b) = single i a - single i b
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
[PROOFSTEP]
obtain rfl | h := eq_or_ne i j
[GOAL]
case h.inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
⊢ ↑(single i (a - b)) i = ↑(single i a - single i b) i
[PROOFSTEP]
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
[GOAL]
case h.inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
h : i ≠ j
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
[PROOFSTEP]
rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝³ : (i : ι) → Sub (α i)
inst✝² : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ support (f - g) ⊆ support f
[PROOFSTEP]
simp (config := { contextual := true }) only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff, Ne.def, coe_tsub,
  Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝³ : (i : ι) → Sub (α i)
inst✝² : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ support f \ support g ⊆ support (f - g)
[PROOFSTEP]
simp (config := { contextual := true }) [subset_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ support (f ⊓ g) = support f ∩ support g
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ support (f ⊓ g) ↔ a✝ ∈ support f ∩ support g
[PROOFSTEP]
simp only [inf_apply, mem_support_iff, Ne.def, Finset.mem_inter]
[GOAL]
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ ¬↑f a✝ ⊓ ↑g a✝ = 0 ↔ ¬↑f a✝ = 0 ∧ ¬↑g a✝ = 0
[PROOFSTEP]
simp only [inf_eq_min, ← nonpos_iff_eq_zero, min_le_iff, not_or]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ support (f ⊔ g) = support f ∪ support g
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ support (f ⊔ g) ↔ a✝ ∈ support f ∪ support g
[PROOFSTEP]
simp only [Finset.mem_union, mem_support_iff, sup_apply, Ne.def, ← bot_eq_zero]
[GOAL]
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ ¬↑f a✝ ⊔ ↑g a✝ = ⊥ ↔ ¬↑f a✝ = ⊥ ∨ ¬↑g a✝ = ⊥
[PROOFSTEP]
rw [_root_.sup_eq_bot_iff, not_and_or]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ Disjoint f g ↔ Disjoint (support f) (support g)
[PROOFSTEP]
rw [disjoint_iff, disjoint_iff, DFinsupp.bot_eq_zero, ← DFinsupp.support_eq_empty, DFinsupp.support_inf]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ support f ∩ support g = ∅ ↔ support f ⊓ support g = ⊥
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
a : α
n : ℕ
⊢ ↑toDFinsupp (replicate n a) = DFinsupp.single a n
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
a : α
n : ℕ
i : α
⊢ ↑(↑toDFinsupp (replicate n a)) i = ↑(DFinsupp.single a n) i
[PROOFSTEP]
dsimp [toDFinsupp]
[GOAL]
case h
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
a : α
n : ℕ
i : α
⊢ count i (replicate n a) = ↑(DFinsupp.single a n) i
[PROOFSTEP]
simp [count_replicate, eq_comm]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ ↑toDFinsupp {a} = DFinsupp.single a 1
[PROOFSTEP]
rw [← replicate_one, toDFinsupp_replicate]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
⊢ AddMonoidHom.comp DFinsupp.toMultiset toDFinsupp = AddMonoidHom.id (Multiset α)
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
x✝ a✝ : α
⊢ count a✝ (↑(AddMonoidHom.comp DFinsupp.toMultiset toDFinsupp) {x✝}) = count a✝ (↑(AddMonoidHom.id (Multiset α)) {x✝})
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
⊢ AddMonoidHom.comp toDFinsupp DFinsupp.toMultiset = AddMonoidHom.id (Π₀ (x : α), ℕ)
[PROOFSTEP]
ext
[GOAL]
case H.a.h
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
x✝ i✝ : α
⊢ ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp toDFinsupp DFinsupp.toMultiset) (DFinsupp.singleAddHom (fun i => ℕ) x✝)) 1)
      i✝ =
    ↑(↑(AddMonoidHom.comp (AddMonoidHom.id (Π₀ (x : α), ℕ)) (DFinsupp.singleAddHom (fun i => ℕ) x✝)) 1) i✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
⊢ ↑toDFinsupp s ≤ ↑toDFinsupp t ↔ s ≤ t
[PROOFSTEP]
simp [Multiset.le_iff_count, DFinsupp.le_def]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
⊢ ↑toDFinsupp (s ∩ t) = ↑toDFinsupp s ⊓ ↑toDFinsupp t
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
i : α
⊢ ↑(↑toDFinsupp (s ∩ t)) i = ↑(↑toDFinsupp s ⊓ ↑toDFinsupp t) i
[PROOFSTEP]
simp [inf_eq_min]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
⊢ ↑toDFinsupp (s ∪ t) = ↑toDFinsupp s ⊔ ↑toDFinsupp t
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
i : α
⊢ ↑(↑toDFinsupp (s ∪ t)) i = ↑(↑toDFinsupp s ⊔ ↑toDFinsupp t) i
[PROOFSTEP]
simp [sup_eq_max]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ ↑toMultiset f ≤ ↑toMultiset g ↔ f ≤ g
[PROOFSTEP]
simp_rw [← Multiset.toDFinsupp_le_toDFinsupp, toMultiset_toDFinsupp]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ ↑toMultiset f < ↑toMultiset g ↔ f < g
[PROOFSTEP]
simp_rw [← Multiset.toDFinsupp_lt_toDFinsupp, toMultiset_toDFinsupp]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ ↑Multiset.toDFinsupp (↑toMultiset (f ⊓ g)) = ↑Multiset.toDFinsupp (↑toMultiset f ∩ ↑toMultiset g)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ ↑Multiset.toDFinsupp (↑toMultiset (f ⊔ g)) = ↑Multiset.toDFinsupp (↑toMultiset f ∪ ↑toMultiset g)
[PROOFSTEP]
simp


[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ↑σ) j < (f ∘ ↑σ) i → P (f ∘ ↑σ) → P (f ∘ ↑σ ∘ ↑(Equiv.swap i j))
⊢ P (f ∘ ↑(sort f))
[PROOFSTEP]
letI := @Preorder.lift _ (Lex (Fin n → α)) _ fun σ : Equiv.Perm (Fin n) => toLex (f ∘ σ)
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ↑σ) j < (f ∘ ↑σ) i → P (f ∘ ↑σ) → P (f ∘ ↑σ ∘ ↑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => ↑toLex (f ∘ ↑σ)
⊢ P (f ∘ ↑(sort f))
[PROOFSTEP]
refine'
  @WellFounded.induction_bot' _ _ _ (IsWellFounded.wf : WellFounded (· < ·)) (Equiv.refl _) (sort f) P (fun σ => f ∘ σ)
    (fun σ hσ hfσ => _) hf
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ↑σ) j < (f ∘ ↑σ) i → P (f ∘ ↑σ) → P (f ∘ ↑σ ∘ ↑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => ↑toLex (f ∘ ↑σ)
σ : Fin n ≃ Fin n
hσ : (fun σ => f ∘ ↑σ) σ ≠ (fun σ => f ∘ ↑σ) (sort f)
hfσ : P ((fun σ => f ∘ ↑σ) σ)
⊢ ∃ c, c < σ ∧ P ((fun σ => f ∘ ↑σ) c)
[PROOFSTEP]
obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ
[GOAL]
case intro.intro.intro
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ↑σ) j < (f ∘ ↑σ) i → P (f ∘ ↑σ) → P (f ∘ ↑σ ∘ ↑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => ↑toLex (f ∘ ↑σ)
σ : Fin n ≃ Fin n
hσ : (fun σ => f ∘ ↑σ) σ ≠ (fun σ => f ∘ ↑σ) (sort f)
hfσ : P ((fun σ => f ∘ ↑σ) σ)
i j : Fin n
hij₁ : i < j
hij₂ : (f ∘ ↑σ) j < (f ∘ ↑σ) i
⊢ ∃ c, c < σ ∧ P ((fun σ => f ∘ ↑σ) c)
[PROOFSTEP]
exact ⟨σ * Equiv.swap i j, Pi.lex_desc hij₁.le hij₂, h σ i j hij₁ hij₂ hfσ⟩


[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Icc a b) = Icc ↑a ↑b
[PROOFSTEP]
simp [Icc_eq_finset_subtype, Finset.fin, Finset.map_map, Icc_filter_lt_of_lt_right]
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ico a b) = Ico ↑a ↑b
[PROOFSTEP]
simp [Ico_eq_finset_subtype, Finset.fin, Finset.map_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioc a b) = Ioc ↑a ↑b
[PROOFSTEP]
simp [Ioc_eq_finset_subtype, Finset.fin, Finset.map_map, Ioc_filter_lt_of_lt_right]
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioo a b) = Ioo ↑a ↑b
[PROOFSTEP]
simp [Ioo_eq_finset_subtype, Finset.fin, Finset.map_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Icc a b) = ↑b + 1 - ↑a
[PROOFSTEP]
rw [← Nat.card_Icc, ← map_valEmbedding_Icc, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Ico a b) = ↑b - ↑a
[PROOFSTEP]
rw [← Nat.card_Ico, ← map_valEmbedding_Ico, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Ioc a b) = ↑b - ↑a
[PROOFSTEP]
rw [← Nat.card_Ioc, ← map_valEmbedding_Ioc, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Ioo a b) = ↑b - ↑a - 1
[PROOFSTEP]
rw [← Nat.card_Ioo, ← map_valEmbedding_Ioo, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (uIcc a b) = Int.natAbs (↑↑b - ↑↑a) + 1
[PROOFSTEP]
rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
[PROOFSTEP]
rw [← card_Icc, Fintype.card_ofFinset]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
[PROOFSTEP]
rw [← card_Ico, Fintype.card_ofFinset]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
[PROOFSTEP]
rw [← card_Ioc, Fintype.card_ofFinset]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
[PROOFSTEP]
rw [← card_Ioo, Fintype.card_ofFinset]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.uIcc a b) = Int.natAbs (↑↑b - ↑↑a) + 1
[PROOFSTEP]
rw [← card_uIcc, Fintype.card_ofFinset]
[GOAL]
n : ℕ
a b : Fin n
⊢ Ici a = Finset.fin n (Icc (↑a) n)
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
a b a✝ : Fin n
⊢ a✝ ∈ Ici a ↔ a✝ ∈ Finset.fin n (Icc (↑a) n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
a b : Fin n
⊢ Ioi a = Finset.fin n (Ioc (↑a) n)
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
a b a✝ : Fin n
⊢ a✝ ∈ Ioi a ↔ a✝ ∈ Finset.fin n (Ioc (↑a) n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ici a) = Icc (↑a) (n - 1)
[PROOFSTEP]
clear b
[GOAL]
n : ℕ
a : Fin n
⊢ map valEmbedding (Ici a) = Icc (↑a) (n - 1)
[PROOFSTEP]
ext x
[GOAL]
case a
n : ℕ
a : Fin n
x : ℕ
⊢ x ∈ map valEmbedding (Ici a) ↔ x ∈ Icc (↑a) (n - 1)
[PROOFSTEP]
simp only [exists_prop, Embedding.coe_subtype, mem_Ici, mem_map, mem_Icc]
[GOAL]
case a
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a ≤ a_1 ∧ ↑valEmbedding a_1 = x) ↔ ↑a ≤ x ∧ x ≤ n - 1
[PROOFSTEP]
constructor
[GOAL]
case a.mp
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a ≤ a_1 ∧ ↑valEmbedding a_1 = x) → ↑a ≤ x ∧ x ≤ n - 1
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case a.mp.intro.intro
n : ℕ
a x : Fin n
hx : a ≤ x
⊢ ↑a ≤ ↑valEmbedding x ∧ ↑valEmbedding x ≤ n - 1
[PROOFSTEP]
exact ⟨hx, le_tsub_of_add_le_right <| x.2⟩
[GOAL]
case a.mpr
n : ℕ
a : Fin n
x : ℕ
⊢ ↑a ≤ x ∧ x ≤ n - 1 → ∃ a_2, a ≤ a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
cases n
[GOAL]
case a.mpr.zero
x : ℕ
a : Fin Nat.zero
⊢ ↑a ≤ x ∧ x ≤ Nat.zero - 1 → ∃ a_2, a ≤ a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
exact Fin.elim0 a
[GOAL]
case a.mpr.succ
x n✝ : ℕ
a : Fin (Nat.succ n✝)
⊢ ↑a ≤ x ∧ x ≤ Nat.succ n✝ - 1 → ∃ a_2, a ≤ a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
exact fun hx => ⟨⟨x, Nat.lt_succ_iff.2 hx.2⟩, hx.1, rfl⟩
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioi a) = Ioc (↑a) (n - 1)
[PROOFSTEP]
clear b
[GOAL]
n : ℕ
a : Fin n
⊢ map valEmbedding (Ioi a) = Ioc (↑a) (n - 1)
[PROOFSTEP]
ext x
[GOAL]
case a
n : ℕ
a : Fin n
x : ℕ
⊢ x ∈ map valEmbedding (Ioi a) ↔ x ∈ Ioc (↑a) (n - 1)
[PROOFSTEP]
simp only [exists_prop, Embedding.coe_subtype, mem_Ioi, mem_map, mem_Ioc]
[GOAL]
case a
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ ↑valEmbedding a_1 = x) ↔ ↑a < x ∧ x ≤ n - 1
[PROOFSTEP]
constructor
[GOAL]
case a.mp
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ ↑valEmbedding a_1 = x) → ↑a < x ∧ x ≤ n - 1
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case a.mp.intro.intro
n : ℕ
a x : Fin n
hx : a < x
⊢ ↑a < ↑valEmbedding x ∧ ↑valEmbedding x ≤ n - 1
[PROOFSTEP]
exact ⟨hx, le_tsub_of_add_le_right <| x.2⟩
[GOAL]
case a.mpr
n : ℕ
a : Fin n
x : ℕ
⊢ ↑a < x ∧ x ≤ n - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
cases n
[GOAL]
case a.mpr.zero
x : ℕ
a : Fin Nat.zero
⊢ ↑a < x ∧ x ≤ Nat.zero - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
exact Fin.elim0 a
[GOAL]
case a.mpr.succ
x n✝ : ℕ
a : Fin (Nat.succ n✝)
⊢ ↑a < x ∧ x ≤ Nat.succ n✝ - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
exact fun hx => ⟨⟨x, Nat.lt_succ_iff.2 hx.2⟩, hx.1, rfl⟩
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Iic b) = Iic ↑b
[PROOFSTEP]
simp [Iic_eq_finset_subtype, Finset.fin, Finset.map_map, Iic_filter_lt_of_lt_right]
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Iio b) = Iio ↑b
[PROOFSTEP]
simp [Iio_eq_finset_subtype, Finset.fin, Finset.map_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Ici a) = n - ↑a
[PROOFSTEP]
clear b
[GOAL]
n : ℕ
a : Fin n
⊢ card (Ici a) = n - ↑a
[PROOFSTEP]
cases n with
| zero => exact Fin.elim0 a
| succ => rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.succ_sub_one]
[GOAL]
n : ℕ
a : Fin n
⊢ card (Ici a) = n - ↑a
[PROOFSTEP]
cases n with
| zero => exact Fin.elim0 a
| succ => rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.succ_sub_one]
[GOAL]
case zero
a : Fin Nat.zero
⊢ card (Ici a) = Nat.zero - ↑a
[PROOFSTEP]

| zero => exact Fin.elim0 a
[GOAL]
case zero
a : Fin Nat.zero
⊢ card (Ici a) = Nat.zero - ↑a
[PROOFSTEP]
exact Fin.elim0 a
[GOAL]
case succ
n✝ : ℕ
a : Fin (Nat.succ n✝)
⊢ card (Ici a) = Nat.succ n✝ - ↑a
[PROOFSTEP]

| succ => rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.succ_sub_one]
[GOAL]
case succ
n✝ : ℕ
a : Fin (Nat.succ n✝)
⊢ card (Ici a) = Nat.succ n✝ - ↑a
[PROOFSTEP]
rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.succ_sub_one]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Ioi a) = n - 1 - ↑a
[PROOFSTEP]
rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioc]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Iic b) = ↑b + 1
[PROOFSTEP]
rw [← Nat.card_Iic b, ← map_valEmbedding_Iic, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Iio b) = ↑b
[PROOFSTEP]
rw [← Nat.card_Iio b, ← map_valEmbedding_Iio, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ici a) = n - ↑a
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Ici]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ioi a) = n - 1 - ↑a
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Ioi]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Iic b) = ↑b + 1
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Iic]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Iio b) = ↑b
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Iio]


[GOAL]
α : Type u_1
n : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
a : α
⊢ ((fun x x_1 => x < x_1) ⇒ r) (vecCons a f) (vecCons a f) ↔ r a (f 0) ∧ ((fun x x_1 => x < x_1) ⇒ r) f f
[PROOFSTEP]
simp only [liftFun_iff_succ r, forall_fin_succ, cons_val_succ, cons_val_zero, ← succ_castSucc, castSucc_zero]
[GOAL]
α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ Monotone (vecCons a f) ↔ a ≤ f 0 ∧ Monotone f
[PROOFSTEP]
simpa only [monotone_iff_forall_lt] using @liftFun_vecCons α n (· ≤ ·) _ f a
[GOAL]
α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ Monotone ![1, 2, 2, 3]
[PROOFSTEP]
simp


[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin m → α
i : Fin m
⊢ vecCons x u (Fin.succ i) = u i
[PROOFSTEP]
simp [vecCons]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
i : ℕ
h : Nat.succ i < Nat.succ m
x : α
u : Fin m → α
⊢ vecCons x u { val := Nat.succ i, isLt := h } = u { val := i, isLt := (_ : i < m) }
[PROOFSTEP]
simp only [vecCons, Fin.cons, Fin.cases_succ']
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin m → α
⊢ vecTail (vecCons x u) = u
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin m → α
x✝ : Fin m
⊢ vecTail (vecCons x u) x✝ = u x✝
[PROOFSTEP]
simp [vecTail]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin n → α
y : α
⊢ y ∈ Set.range (vecCons x u) ↔ y ∈ {x} ∪ Set.range u
[PROOFSTEP]
simp [Fin.exists_fin_succ, eq_comm]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin 0 → α
⊢ Set.range (vecCons x u) = {x}
[PROOFSTEP]
rw [range_cons, range_empty, Set.union_empty]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x y : α
u : Fin 0 → α
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}
[PROOFSTEP]
rw [range_cons, range_cons_empty, Set.singleton_union]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin 0 → α
⊢ ∀ (i : Fin 1), vecCons x u i = x
[PROOFSTEP]
rw [Fin.forall_fin_one]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin 0 → α
⊢ vecCons x u 0 = x
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
m n o✝ : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
⊢ vecAppend ho u v = fun i =>
    if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
[PROOFSTEP]
ext i
[GOAL]
case h
α✝ : Type u
m n o✝ : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ vecAppend ho u v i = if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
[PROOFSTEP]
rw [vecAppend, Fin.append, Function.comp_apply, Fin.addCases]
[GOAL]
case h
α✝ : Type u
m n o✝ : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (if hi : ↑(↑(Fin.castIso ho) i) < m then
      (_ : Fin.castAdd n (Fin.castLT (↑(Fin.castIso ho) i) hi) = ↑(Fin.castIso ho) i) ▸
        u (Fin.castLT (↑(Fin.castIso ho) i) hi)
    else
      (_ :
          Fin.natAdd m
              (Fin.subNat m (Fin.cast (_ : m + n = n + m) (↑(Fin.castIso ho) i)) (_ : m ≤ ↑(↑(Fin.castIso ho) i))) =
            ↑(Fin.castIso ho) i) ▸
        v (Fin.subNat m (Fin.cast (_ : m + n = n + m) (↑(Fin.castIso ho) i)) (_ : m ≤ ↑(↑(Fin.castIso ho) i)))) =
    if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
[PROOFSTEP]
congr with hi
[GOAL]
case h.e_e.h
α✝ : Type u
m n o✝ : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(↑(Fin.castIso ho) i) < m
⊢ (_ :
        Fin.natAdd m
            (Fin.subNat m (Fin.cast (_ : m + n = n + m) (↑(Fin.castIso ho) i)) (_ : m ≤ ↑(↑(Fin.castIso ho) i))) =
          ↑(Fin.castIso ho) i) ▸
      v (Fin.subNat m (Fin.cast (_ : m + n = n + m) (↑(Fin.castIso ho) i)) (_ : m ≤ ↑(↑(Fin.castIso ho) i))) =
    v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
[PROOFSTEP]
simp only [eq_rec_constant]
[GOAL]
case h.e_e.h
α✝ : Type u
m n o✝ : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(↑(Fin.castIso ho) i) < m
⊢ v (Fin.subNat m (Fin.cast (_ : m + n = n + m) (↑(Fin.castIso ho) i)) (_ : m ≤ ↑(↑(Fin.castIso ho) i))) =
    v { val := ↑i - m, isLt := (_ : ↑i - m < n) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
⊢ vecAppend (_ : n = 0 + n) ![] v = v
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
x✝ : Fin n
⊢ vecAppend (_ : n = 0 + n) ![] v x✝ = v x✝
[PROOFSTEP]
simp [vecAppend_eq_ite]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
⊢ o = m + n
[PROOFSTEP]
rwa [add_assoc, add_comm 1, ← add_assoc, add_right_cancel_iff] at ho
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
⊢ vecAppend ho (vecCons x u) v = vecCons x (vecAppend (_ : o = m + n) u v)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ vecAppend ho (vecCons x u) v i = vecCons x (vecAppend (_ : o = m + n) u v) i
[PROOFSTEP]
simp_rw [vecAppend_eq_ite]
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ (if h : ↑i < m + 1 then vecCons x u { val := ↑i, isLt := h }
    else v { val := ↑i - (m + 1), isLt := (_ : ↑i - (m + 1) < n) }) =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }) i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
h : ↑i < m + 1
⊢ vecCons x u { val := ↑i, isLt := h } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }) i
[PROOFSTEP]
rcases i with ⟨⟨⟩ | i, hi⟩
[GOAL]
case pos.mk.zero
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
hi : Nat.zero < o + 1
h : ↑{ val := Nat.zero, isLt := hi } < m + 1
⊢ vecCons x u { val := ↑{ val := Nat.zero, isLt := hi }, isLt := h } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.zero, isLt := hi }
[PROOFSTEP]
simp
[GOAL]
case pos.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : Nat.succ i < o + 1
h : ↑{ val := Nat.succ i, isLt := hi } < m + 1
⊢ vecCons x u { val := ↑{ val := Nat.succ i, isLt := hi }, isLt := h } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, add_lt_add_iff_right, Fin.val_mk] at h
[GOAL]
case pos.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : Nat.succ i < o + 1
h✝ : ↑{ val := Nat.succ i, isLt := hi } < m + 1
h : i < m
⊢ vecCons x u { val := ↑{ val := Nat.succ i, isLt := hi }, isLt := h✝ } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
h : ¬↑i < m + 1
⊢ v { val := ↑i - (m + 1), isLt := (_ : ↑i - (m + 1) < n) } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) }) i
[PROOFSTEP]
rcases i with ⟨⟨⟩ | i, hi⟩
[GOAL]
case neg.mk.zero
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
hi : Nat.zero < o + 1
h : ¬↑{ val := Nat.zero, isLt := hi } < m + 1
⊢ v
      { val := ↑{ val := Nat.zero, isLt := hi } - (m + 1),
        isLt := (_ : ↑{ val := Nat.zero, isLt := hi } - (m + 1) < n) } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.zero, isLt := hi }
[PROOFSTEP]
simp at h
[GOAL]
case neg.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : Nat.succ i < o + 1
h : ¬↑{ val := Nat.succ i, isLt := hi } < m + 1
⊢ v
      { val := ↑{ val := Nat.succ i, isLt := hi } - (m + 1),
        isLt := (_ : ↑{ val := Nat.succ i, isLt := hi } - (m + 1) < n) } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
rw [not_lt, Fin.val_mk, Nat.succ_eq_add_one, add_le_add_iff_right] at h
[GOAL]
case neg.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : Nat.succ i < o + 1
h✝ : ¬↑{ val := Nat.succ i, isLt := hi } < m + 1
h : m ≤ i
⊢ v
      { val := ↑{ val := Nat.succ i, isLt := hi } - (m + 1),
        isLt := (_ : ↑{ val := Nat.succ i, isLt := hi } - (m + 1) < n) } =
    vecCons x
      (fun i => if h : ↑i < m then u { val := ↑i, isLt := h } else v { val := ↑i - m, isLt := (_ : ↑i - m < n) })
      { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
simp [h, not_lt.2 h]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
⊢ vecAlt0 (_ : n + n = n + n) (vecAppend (_ : n + n = n + n) v v) = v ∘ bit0
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
⊢ vecAlt0 (_ : n + n = n + n) (vecAppend (_ : n + n = n + n) v v) i = (v ∘ bit0) i
[PROOFSTEP]
simp_rw [Function.comp, bit0, vecAlt0, vecAppend_eq_ite]
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
⊢ (if h : ↑i + ↑i < n then v { val := ↑i + ↑i, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } < n) }
    else v { val := ↑i + ↑i - n, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } - n < n) }) =
    v (i + i)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ v { val := ↑i + ↑i, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } < n) } = v (i + i)
[PROOFSTEP]
congr
[GOAL]
case neg
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ v { val := ↑i + ↑i - n, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } - n < n) } = v (i + i)
[PROOFSTEP]
congr
[GOAL]
case pos.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n
[PROOFSTEP]
rw [Fin.val_mk] at h
[GOAL]
case pos.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n
[PROOFSTEP]
exact (Nat.mod_eq_of_lt h).symm
[GOAL]
case neg.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
[PROOFSTEP]
rw [Fin.val_mk, not_lt] at h
[GOAL]
case neg.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
[PROOFSTEP]
simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_eq_sub_mod h]
[GOAL]
case neg.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i - n) % n
[PROOFSTEP]
refine' (Nat.mod_eq_of_lt _).symm
[GOAL]
case neg.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n < n
[PROOFSTEP]
rw [tsub_lt_iff_left h]
[GOAL]
case neg.e_a.e_val
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i < n + n
[PROOFSTEP]
exact add_lt_add i.2 i.2
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (n + 1) → α
⊢ vecAlt1 (_ : n + 1 + (n + 1) = n + 1 + (n + 1)) (vecAppend (_ : n + 1 + (n + 1) = n + 1 + (n + 1)) v v) = v ∘ bit1
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ vecAlt1 (_ : n + 1 + (n + 1) = n + 1 + (n + 1)) (vecAppend (_ : n + 1 + (n + 1) = n + 1 + (n + 1)) v v) i =
    (v ∘ bit1) i
[PROOFSTEP]
simp_rw [Function.comp, vecAlt1, vecAppend_eq_ite]
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ (if h : ↑i + ↑i + 1 < n + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt := (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < n + 1 + (n + 1)) } < n + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (n + 1),
          isLt := (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < n + 1 + (n + 1)) } - (n + 1) < n + 1) }) =
    v (bit1 i)
[PROOFSTEP]
cases n with
| zero =>
  cases' i with i hi
  simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi ; subst i; rfl
| succ n =>
  split_ifs with h <;> simp_rw [bit1, bit0] <;> congr
  · rw [Fin.val_mk] at h
    rw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)]
    erw [Nat.mod_eq_of_lt h]
  · rw [Fin.val_mk, not_lt] at h
    simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one, Nat.mod_eq_sub_mod h,
      show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by simp)]
    refine (Nat.mod_eq_of_lt ?_).symm
    rw [tsub_lt_iff_left h]
    exact Nat.add_succ_lt_add i.2 i.2
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ (if h : ↑i + ↑i + 1 < n + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt := (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < n + 1 + (n + 1)) } < n + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (n + 1),
          isLt := (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < n + 1 + (n + 1)) } - (n + 1) < n + 1) }) =
    v (bit1 i)
[PROOFSTEP]
cases n with
| zero =>
  cases' i with i hi
  simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi ; subst i; rfl
| succ n =>
  split_ifs with h <;> simp_rw [bit1, bit0] <;> congr
  · rw [Fin.val_mk] at h
    rw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)]
    erw [Nat.mod_eq_of_lt h]
  · rw [Fin.val_mk, not_lt] at h
    simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one, Nat.mod_eq_sub_mod h,
      show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by simp)]
    refine (Nat.mod_eq_of_lt ?_).symm
    rw [tsub_lt_iff_left h]
    exact Nat.add_succ_lt_add i.2 i.2
[GOAL]
case h.zero
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (Nat.zero + 1) → α
i : Fin (Nat.zero + 1)
⊢ (if h : ↑i + ↑i + 1 < Nat.zero + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt :=
            (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.zero + 1 + (Nat.zero + 1)) } < Nat.zero + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (Nat.zero + 1),
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.zero + 1 + (Nat.zero + 1)) } - (Nat.zero + 1) <
                Nat.zero + 1) }) =
    v (bit1 i)
[PROOFSTEP]

| zero =>
  cases' i with i hi
  simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi ; subst i; rfl
[GOAL]
case h.zero
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (Nat.zero + 1) → α
i : Fin (Nat.zero + 1)
⊢ (if h : ↑i + ↑i + 1 < Nat.zero + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt :=
            (_ : ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.zero + 1 + (Nat.zero + 1)) } < Nat.zero + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (Nat.zero + 1),
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.zero + 1 + (Nat.zero + 1)) } - (Nat.zero + 1) <
                Nat.zero + 1) }) =
    v (bit1 i)
[PROOFSTEP]
cases' i with i hi
[GOAL]
case h.zero.mk
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (Nat.zero + 1) → α
i : ℕ
hi : i < Nat.zero + 1
⊢ (if h : ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1 < Nat.zero + 1 then
      v
        { val := ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1,
          isLt :=
            (_ :
              ↑{ val := ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1,
                    isLt :=
                      (_ :
                        ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1 < Nat.zero + 1 + (Nat.zero + 1)) } <
                Nat.zero + 1) }
    else
      v
        { val := ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1 - (Nat.zero + 1),
          isLt :=
            (_ :
              ↑{ val := ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1,
                      isLt :=
                        (_ :
                          ↑{ val := i, isLt := hi } + ↑{ val := i, isLt := hi } + 1 < Nat.zero + 1 + (Nat.zero + 1)) } -
                  (Nat.zero + 1) <
                Nat.zero + 1) }) =
    v (bit1 { val := i, isLt := hi })
[PROOFSTEP]
simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi
[GOAL]
case h.zero.mk
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (Nat.zero + 1) → α
i : ℕ
hi✝ : i < Nat.zero + 1
hi : i = 0
⊢ (if h : ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1 < Nat.zero + 1 then
      v
        { val := ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1,
          isLt :=
            (_ :
              ↑{ val := ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1,
                    isLt :=
                      (_ :
                        ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1 < Nat.zero + 1 + (Nat.zero + 1)) } <
                Nat.zero + 1) }
    else
      v
        { val := ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1 - (Nat.zero + 1),
          isLt :=
            (_ :
              ↑{ val := ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1,
                      isLt :=
                        (_ :
                          ↑{ val := i, isLt := hi✝ } + ↑{ val := i, isLt := hi✝ } + 1 <
                            Nat.zero + 1 + (Nat.zero + 1)) } -
                  (Nat.zero + 1) <
                Nat.zero + 1) }) =
    v (bit1 { val := i, isLt := hi✝ })
[PROOFSTEP]
subst i
[GOAL]
case h.zero.mk
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
v : Fin (Nat.zero + 1) → α
hi : 0 < Nat.zero + 1
⊢ (if h : ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1 < Nat.zero + 1 then
      v
        { val := ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1,
          isLt :=
            (_ :
              ↑{ val := ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1,
                    isLt :=
                      (_ :
                        ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1 < Nat.zero + 1 + (Nat.zero + 1)) } <
                Nat.zero + 1) }
    else
      v
        { val := ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1 - (Nat.zero + 1),
          isLt :=
            (_ :
              ↑{ val := ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1,
                      isLt :=
                        (_ :
                          ↑{ val := 0, isLt := hi } + ↑{ val := 0, isLt := hi } + 1 < Nat.zero + 1 + (Nat.zero + 1)) } -
                  (Nat.zero + 1) <
                Nat.zero + 1) }) =
    v (bit1 { val := 0, isLt := hi })
[PROOFSTEP]
rfl
[GOAL]
case h.succ
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
⊢ (if h : ↑i + ↑i + 1 < Nat.succ n + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } < Nat.succ n + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (Nat.succ n + 1),
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } -
                  (Nat.succ n + 1) <
                Nat.succ n + 1) }) =
    v (bit1 i)
[PROOFSTEP]

| succ n =>
  split_ifs with h <;> simp_rw [bit1, bit0] <;> congr
  · rw [Fin.val_mk] at h
    rw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)]
    erw [Nat.mod_eq_of_lt h]
  · rw [Fin.val_mk, not_lt] at h
    simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one, Nat.mod_eq_sub_mod h,
      show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by simp)]
    refine (Nat.mod_eq_of_lt ?_).symm
    rw [tsub_lt_iff_left h]
    exact Nat.add_succ_lt_add i.2 i.2
[GOAL]
case h.succ
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
⊢ (if h : ↑i + ↑i + 1 < Nat.succ n + 1 then
      v
        { val := ↑i + ↑i + 1,
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } < Nat.succ n + 1) }
    else
      v
        { val := ↑i + ↑i + 1 - (Nat.succ n + 1),
          isLt :=
            (_ :
              ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } -
                  (Nat.succ n + 1) <
                Nat.succ n + 1) }) =
    v (bit1 i)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ↑i + ↑i + 1 < Nat.succ n + 1
⊢ v
      { val := ↑i + ↑i + 1,
        isLt :=
          (_ :
            ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } < Nat.succ n + 1) } =
    v (bit1 i)
[PROOFSTEP]
simp_rw [bit1, bit0]
[GOAL]
case neg
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ¬↑i + ↑i + 1 < Nat.succ n + 1
⊢ v
      { val := ↑i + ↑i + 1 - (Nat.succ n + 1),
        isLt :=
          (_ :
            ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } - (Nat.succ n + 1) <
              Nat.succ n + 1) } =
    v (bit1 i)
[PROOFSTEP]
simp_rw [bit1, bit0]
[GOAL]
case pos
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ↑i + ↑i + 1 < Nat.succ n + 1
⊢ v
      { val := ↑i + ↑i + 1,
        isLt :=
          (_ :
            ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } < Nat.succ n + 1) } =
    v (i + i + 1)
[PROOFSTEP]
congr
[GOAL]
case neg
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ¬↑i + ↑i + 1 < Nat.succ n + 1
⊢ v
      { val := ↑i + ↑i + 1 - (Nat.succ n + 1),
        isLt :=
          (_ :
            ↑{ val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)) } - (Nat.succ n + 1) <
              Nat.succ n + 1) } =
    v (i + i + 1)
[PROOFSTEP]
congr
[GOAL]
case pos.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ↑i + ↑i + 1 < Nat.succ n + 1
⊢ ↑i + ↑i + 1 = ((↑i + ↑i) % (Nat.succ n + 1) + 1 % (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
rw [Fin.val_mk] at h
[GOAL]
case pos.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ↑i + ↑i + 1 < Nat.succ n + 1
⊢ ↑i + ↑i + 1 = ((↑i + ↑i) % (Nat.succ n + 1) + 1 % (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
rw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)]
[GOAL]
case pos.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ↑i + ↑i + 1 < Nat.succ n + 1
⊢ ↑i + ↑i + 1 = (↑i + ↑i + 1 % (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
erw [Nat.mod_eq_of_lt h]
[GOAL]
case neg.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : ¬↑i + ↑i + 1 < Nat.succ n + 1
⊢ ↑i + ↑i + 1 - (Nat.succ n + 1) = ((↑i + ↑i) % (Nat.succ n + 1) + 1 % (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
rw [Fin.val_mk, not_lt] at h
[GOAL]
case neg.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : Nat.succ n + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (Nat.succ n + 1) = ((↑i + ↑i) % (Nat.succ n + 1) + 1 % (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one, Nat.mod_eq_sub_mod h,
  show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by simp)]
[GOAL]
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : Nat.succ n + 1 ≤ ↑i + ↑i + 1
⊢ 1 < n + 2
[PROOFSTEP]
simp
[GOAL]
case neg.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : Nat.succ n + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (Nat.succ n + 1) = (↑i + ↑i + 1 - (Nat.succ n + 1)) % (Nat.succ n + 1)
[PROOFSTEP]
refine (Nat.mod_eq_of_lt ?_).symm
[GOAL]
case neg.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : Nat.succ n + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (Nat.succ n + 1) < Nat.succ n + 1
[PROOFSTEP]
rw [tsub_lt_iff_left h]
[GOAL]
case neg.e_a.e_val
α : Type u
m o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
n : ℕ
v : Fin (Nat.succ n + 1) → α
i : Fin (Nat.succ n + 1)
h : Nat.succ n + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 < Nat.succ n + 1 + (Nat.succ n + 1)
[PROOFSTEP]
exact Nat.add_succ_lt_add i.2 i.2
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
hm : m + 2 = n + 1 + (n + 1)
v : Fin (m + 2) → α
⊢ vecHead (vecAlt1 hm v) = v 1
[PROOFSTEP]
simp [vecHead, vecAlt1]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit0 i) =
    vecAlt0 (_ : Nat.succ n + Nat.succ n = Nat.succ n + Nat.succ n)
      (vecAppend (_ : Nat.succ n + Nat.succ n = Nat.succ n + Nat.succ n) (vecCons x u) (vecCons x u)) i
[PROOFSTEP]
rw [vecAlt0_vecAppend]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit0 i) = (vecCons x u ∘ bit0) i
[PROOFSTEP]
rfl
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit1 i) =
    vecAlt1 (_ : Nat.succ n + Nat.succ n = Nat.succ n + Nat.succ n)
      (vecAppend (_ : Nat.succ n + Nat.succ n = Nat.succ n + Nat.succ n) (vecCons x u) (vecCons x u)) i
[PROOFSTEP]
rw [vecAlt1_vecAppend]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit1 i) = (vecCons x u ∘ bit1) i
[PROOFSTEP]
rfl
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n
[PROOFSTEP]
rwa [add_assoc n, add_comm 1, ← add_assoc, ← add_assoc, add_right_cancel_iff, add_right_cancel_iff] at h
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 (_ : m = n + n) u)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 (_ : m = n + n) u) i
[PROOFSTEP]
simp_rw [vecAlt0]
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) { val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) i
[PROOFSTEP]
rcases i with ⟨⟨⟩ | i, hi⟩
[GOAL]
case h.mk.zero
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : Nat.zero < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi },
        isLt := (_ : ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi } < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) { val := Nat.zero, isLt := hi }
[PROOFSTEP]
rfl
[GOAL]
case h.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : Nat.succ i < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi },
        isLt := (_ : ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi } < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
simp [vecAlt0, Nat.add_succ, Nat.succ_add]
[GOAL]
α✝ : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
h : 0 = 0 + 0
⊢ vecAlt0 h ![] = ![]
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n
[PROOFSTEP]
rwa [add_assoc n, add_comm 1, ← add_assoc, ← add_assoc, add_right_cancel_iff, add_right_cancel_iff] at h
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 (_ : m = n + n) u)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt1 h (vecCons x (vecCons y u)) i = vecCons y (vecAlt1 (_ : m = n + n) u) i
[PROOFSTEP]
simp_rw [vecAlt1]
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) { val := ↑i + ↑i + 1, isLt := (_ : ↑i + ↑i + 1 < m + 1 + 1) } =
    vecCons y (fun k => u { val := ↑k + ↑k + 1, isLt := (_ : ↑k + ↑k + 1 < m) }) i
[PROOFSTEP]
rcases i with ⟨⟨⟩ | i, hi⟩
[GOAL]
case h.mk.zero
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : Nat.zero < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi } + 1,
        isLt := (_ : ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi } + 1 < m + 1 + 1) } =
    vecCons y (fun k => u { val := ↑k + ↑k + 1, isLt := (_ : ↑k + ↑k + 1 < m) }) { val := Nat.zero, isLt := hi }
[PROOFSTEP]
rfl
[GOAL]
case h.mk.succ
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : Nat.succ i < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi } + 1,
        isLt := (_ : ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi } + 1 < m + 1 + 1) } =
    vecCons y (fun k => u { val := ↑k + ↑k + 1, isLt := (_ : ↑k + ↑k + 1 < m) }) { val := Nat.succ i, isLt := hi }
[PROOFSTEP]
simp [vecAlt1, Nat.add_succ, Nat.succ_add]
[GOAL]
α✝ : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
α : Type u_4
h : 0 = 0 + 0
⊢ vecAlt1 h ![] = ![]
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
M : Type u_4
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
⊢ x • vecCons y v = vecCons (x • y) (x • v)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
M : Type u_4
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
M : Type u_4
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (x • vecCons y v) 0 = vecCons (x • y) (x • v) 0
[PROOFSTEP]
simp
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
M : Type u_4
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (x • vecCons y v) (Fin.succ i) = vecCons (x • y) (x • v) (Fin.succ i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
⊢ vecCons x v + w = vecCons (x + vecHead w) (v + vecTail w)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ (vecCons x v + w) 0 = vecCons (x + vecHead w) (v + vecTail w) 0
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (vecCons x v + w) (Fin.succ i) = vecCons (x + vecHead w) (v + vecTail w) (Fin.succ i)
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
⊢ v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ (v + vecCons y w) 0 = vecCons (vecHead v + y) (vecTail v + w) 0
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (v + vecCons y w) (Fin.succ i) = vecCons (vecHead v + y) (vecTail v + w) (Fin.succ i)
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Add α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v + vecCons y w = vecCons (x + y) (v + w)
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
⊢ vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ (vecCons x v - w) 0 = vecCons (x - vecHead w) (v - vecTail w) 0
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (vecCons x v - w) (Fin.succ i) = vecCons (x - vecHead w) (v - vecTail w) (Fin.succ i)
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
⊢ v - vecCons y w = vecCons (vecHead v - y) (vecTail v - w)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ (v - vecCons y w) 0 = vecCons (vecHead v - y) (vecTail v - w) 0
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
v : Fin (Nat.succ n) → α
y : α
w : Fin n → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (v - vecCons y w) (Fin.succ i) = vecCons (vecHead v - y) (vecTail v - w) (Fin.succ i)
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Sub α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v - vecCons y w = vecCons (x - y) (v - w)
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
⊢ vecCons 0 0 = 0
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ vecCons 0 0 i = OfNat.ofNat 0 i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ vecCons 0 0 0 = OfNat.ofNat 0 0
[PROOFSTEP]
rfl
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), vecCons 0 0 (Fin.succ i) = OfNat.ofNat 0 (Fin.succ i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
v : Fin n → α
x : α
h : vecCons x v = 0
⊢ v = 0
[PROOFSTEP]
convert congr_arg vecTail h
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Zero α
v : Fin n → α
x : α
x✝ : x = 0 ∧ v = 0
hx : x = 0
hv : v = 0
⊢ vecCons x v = 0
[PROOFSTEP]
simp [hx, hv]
[GOAL]
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Neg α
x : α
v : Fin n → α
⊢ -vecCons x v = vecCons (-x) (-v)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (-vecCons x v) i = vecCons (-x) (-v) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (-vecCons x v) 0 = vecCons (-x) (-v) 0
[PROOFSTEP]
simp
[GOAL]
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type u_1
n' : Type u_2
o' : Type u_3
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), (-vecCons x v) (Fin.succ i) = vecCons (-x) (-v) (Fin.succ i)
[PROOFSTEP]
simp