[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q f : R[X]
⊢ { toFinsupp := f.toFinsupp } = f
[PROOFSTEP]
cases f
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := { toFinsupp := toFinsupp✝ }.toFinsupp } = { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a b : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a + b } = Polynomial.add { toFinsupp := a } { toFinsupp := b }
[PROOFSTEP]
rw [add_def]
[GOAL]
R✝ : Type u
a✝ b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := -a } = Polynomial.neg { toFinsupp := a }
[PROOFSTEP]
rw [neg_def]
[GOAL]
R✝ : Type u
a✝ b✝ : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a b : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }
[PROOFSTEP]
rw [sub_eq_add_neg, ofFinsupp_add, ofFinsupp_neg]
[GOAL]
R✝ : Type u
a✝ b✝ : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a b : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a } + -{ toFinsupp := b } = { toFinsupp := a } - { toFinsupp := b }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a b : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a * b } = Polynomial.mul { toFinsupp := a } { toFinsupp := b }
[PROOFSTEP]
rw [mul_def]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := a ^ n } = { toFinsupp := a } ^ n
[PROOFSTEP]
change _ = npowRec n _
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
[PROOFSTEP]
induction n with
| zero => simp [npowRec]
| succ n n_ih => simp [npowRec, n_ih, pow_succ]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
[PROOFSTEP]
induction n with
| zero => simp [npowRec]
| succ n n_ih => simp [npowRec, n_ih, pow_succ]
[GOAL]
case zero
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a ^ Nat.zero } = npowRec Nat.zero { toFinsupp := a }
[PROOFSTEP]

| zero => simp [npowRec]
[GOAL]
case zero
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a ^ Nat.zero } = npowRec Nat.zero { toFinsupp := a }
[PROOFSTEP]
simp [npowRec]
[GOAL]
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := a ^ Nat.succ n } = npowRec (Nat.succ n) { toFinsupp := a }
[PROOFSTEP]

| succ n n_ih => simp [npowRec, n_ih, pow_succ]
[GOAL]
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := a ^ Nat.succ n } = npowRec (Nat.succ n) { toFinsupp := a }
[PROOFSTEP]
simp [npowRec, n_ih, pow_succ]
[GOAL]
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
p q a b : R[X]
⊢ (a + b).toFinsupp = a.toFinsupp + b.toFinsupp
[PROOFSTEP]
cases a
[GOAL]
case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q b : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } + b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp + b.toFinsupp
[PROOFSTEP]
cases b
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp + { toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
rw [← ofFinsupp_add]
[GOAL]
R✝ : Type u
a✝ b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a : R[X]
⊢ (-a).toFinsupp = -a.toFinsupp
[PROOFSTEP]
cases a
[GOAL]
case ofFinsupp
R✝ : Type u
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (-{ toFinsupp := toFinsupp✝ }).toFinsupp = -{ toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
rw [← ofFinsupp_neg]
[GOAL]
R✝ : Type u
a✝ b✝ : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp - b.toFinsupp
[PROOFSTEP]
rw [sub_eq_add_neg, ← toFinsupp_neg, ← toFinsupp_add]
[GOAL]
R✝ : Type u
a✝ b✝ : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = (a + -b).toFinsupp
[PROOFSTEP]
rfl
[GOAL]
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
p q a b : R[X]
⊢ (a * b).toFinsupp = a.toFinsupp * b.toFinsupp
[PROOFSTEP]
cases a
[GOAL]
case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q b : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } * b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp * b.toFinsupp
[PROOFSTEP]
cases b
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp * { toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
rw [← ofFinsupp_mul]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q a : R[X]
n : ℕ
⊢ (a ^ n).toFinsupp = a.toFinsupp ^ n
[PROOFSTEP]
cases a
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } ^ n).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp ^ n
[PROOFSTEP]
rw [← ofFinsupp_pow]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q a : R[X]
⊢ a.toFinsupp = 0 ↔ a = 0
[PROOFSTEP]
rw [← toFinsupp_zero, toFinsupp_inj]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q a : R[X]
⊢ a.toFinsupp = 1 ↔ a = 1
[PROOFSTEP]
rw [← toFinsupp_one, toFinsupp_inj]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a } = 0 ↔ a = 0
[PROOFSTEP]
rw [← ofFinsupp_zero, ofFinsupp_inj]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a } = 1 ↔ a = 1
[PROOFSTEP]
rw [← ofFinsupp_one, ofFinsupp_inj]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S₁ : Type ?u.114071
S₂ : Type ?u.114238
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : SMulCommClass S₁ S₂ R
⊢ ∀ (m : S₁) (n : S₂) (a : R[X]), m • n • a = n • m • a
[PROOFSTEP]
rintro m n ⟨f⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝³ : Semiring R
p q : R[X]
S₁ : Type ?u.114071
S₂ : Type ?u.114238
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : SMulCommClass S₁ S₂ R
m : S₁
n : S₂
f : AddMonoidAlgebra R ℕ
⊢ m • n • { toFinsupp := f } = n • m • { toFinsupp := f }
[PROOFSTEP]
simp_rw [← ofFinsupp_smul, smul_comm m n f]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝⁴ : Semiring R
p q : R[X]
S₁ : Type ?u.117123
S₂ : Type ?u.117122
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : IsScalarTower S₁ S₂ R
⊢ ∀ (x : S₁) (y : S₂) (z : R[X]), (x • y) • z = x • y • z
[PROOFSTEP]
rintro _ _ ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝⁴ : Semiring R
p q : R[X]
S₁ : Type ?u.117123
S₂ : Type ?u.117122
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : IsScalarTower S₁ S₂ R
x✝ : S₁
y✝ : S₂
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (x✝ • y✝) • { toFinsupp := toFinsupp✝ } = x✝ • y✝ • { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
simp_rw [← ofFinsupp_smul, smul_assoc]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst✝² : Semiring K
inst✝¹ : DistribSMul α K
inst✝ : IsScalarTower α K K
⊢ ∀ (x : α) (y z : K[X]), (x • y) • z = x • y • z
[PROOFSTEP]
rintro _ ⟨⟩ ⟨⟩
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst✝² : Semiring K
inst✝¹ : DistribSMul α K
inst✝ : IsScalarTower α K K
x✝ : α
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra K ℕ
⊢ (x✝ • { toFinsupp := toFinsupp✝¹ }) • { toFinsupp := toFinsupp✝ } =
    x✝ • { toFinsupp := toFinsupp✝¹ } • { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type ?u.129006
inst✝² : SMulZeroClass S R
inst✝¹ : SMulZeroClass Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
⊢ ∀ (m : S) (a : R[X]), MulOpposite.op m • a = m • a
[PROOFSTEP]
rintro _ ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type ?u.129006
inst✝² : SMulZeroClass S R
inst✝¹ : SMulZeroClass Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
m✝ : S
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ MulOpposite.op m✝ • { toFinsupp := toFinsupp✝ } = m✝ • { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
simp_rw [← ofFinsupp_smul, op_smul_eq_smul]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Subsingleton R
src✝ : Inhabited R[X] := inhabited
⊢ ∀ (a : R[X]), a = default
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Subsingleton R
src✝ : Inhabited R[X] := inhabited
x : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := x } = default
[PROOFSTEP]
refine' congr_arg ofFinsupp _
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Subsingleton R
src✝ : Inhabited R[X] := inhabited
x : AddMonoidAlgebra R ℕ
⊢ x = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
p : AddMonoidAlgebra R ℕ
⊢ support { toFinsupp := p } = p.support
[PROOFSTEP]
rw [support]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
⊢ p.toFinsupp.support = support p
[PROOFSTEP]
rw [support]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ support p = ∅ ↔ p = 0
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support { toFinsupp := toFinsupp✝ } = ∅ ↔ { toFinsupp := toFinsupp✝ } = 0
[PROOFSTEP]
simp [support]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ Finset.card (support p) = 0 ↔ p = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
x y : R
⊢ (fun t => { toFinsupp := Finsupp.single n t }) (x + y) =
    (fun t => { toFinsupp := Finsupp.single n t }) x + (fun t => { toFinsupp := Finsupp.single n t }) y
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
x y : R
⊢ { toFinsupp := Finsupp.single n x + Finsupp.single n y } =
    { toFinsupp := Finsupp.single n x } + { toFinsupp := Finsupp.single n y }
[PROOFSTEP]
rw [ofFinsupp_add]
  -- Porting note: Was `simp [← ofFinsupp_smul]`.
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r x : R
⊢ AddHom.toFun
      { toFun := fun t => { toFinsupp := Finsupp.single n t },
        map_add' :=
          (_ :
            ∀ (x y : R),
              (fun t => { toFinsupp := Finsupp.single n t }) (x + y) =
                (fun t => { toFinsupp := Finsupp.single n t }) x + (fun t => { toFinsupp := Finsupp.single n t }) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun t => { toFinsupp := Finsupp.single n t },
          map_add' :=
            (_ :
              ∀ (x y : R),
                (fun t => { toFinsupp := Finsupp.single n t }) (x + y) =
                  (fun t => { toFinsupp := Finsupp.single n t }) x + (fun t => { toFinsupp := Finsupp.single n t }) y) }
        x
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r x : R
⊢ { toFinsupp := Finsupp.single n (r * x) } = r • { toFinsupp := Finsupp.single n x }
[PROOFSTEP]
rw [← ofFinsupp_smul, smul_single']
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ (↑(monomial n) r).toFinsupp = Finsupp.single n r
[PROOFSTEP]
simp [monomial]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ { toFinsupp := Finsupp.single n r } = ↑(monomial n) r
[PROOFSTEP]
simp [monomial]
[GOAL]
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n m : ℕ
r s : R
⊢ (↑(monomial n) r * ↑(monomial m) s).toFinsupp = (↑(monomial (n + m)) (r * s)).toFinsupp
[PROOFSTEP]
simp only [toFinsupp_monomial, toFinsupp_mul, AddMonoidAlgebra.single_mul_single]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
⊢ ↑(monomial n) r ^ k = ↑(monomial (n * k)) (r ^ k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ ↑(monomial n) r ^ Nat.zero = ↑(monomial (n * Nat.zero)) (r ^ Nat.zero)
[PROOFSTEP]
simp [pow_zero, monomial_zero_one]
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
ih : ↑(monomial n) r ^ k = ↑(monomial (n * k)) (r ^ k)
⊢ ↑(monomial n) r ^ Nat.succ k = ↑(monomial (n * Nat.succ k)) (r ^ Nat.succ k)
[PROOFSTEP]
simp [pow_succ, ih, monomial_mul_monomial, Nat.succ_eq_add_one, mul_add, add_comm]
[GOAL]
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : SMulZeroClass S R
a : S
n : ℕ
b : R
⊢ (a • ↑(monomial n) b).toFinsupp = (↑(monomial n) (a • b)).toFinsupp
[PROOFSTEP]
simp
[GOAL]
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : SMulZeroClass S R
a : S
n : ℕ
b : R
⊢ a • Finsupp.single n b = Finsupp.single n (a • b)
[PROOFSTEP]
rw [smul_single]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ support (p + q) ⊆ support p ∪ support q
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support ({ toFinsupp := toFinsupp✝ } + q) ⊆ support { toFinsupp := toFinsupp✝ } ∪ support q
[PROOFSTEP]
rcases q with ⟨⟩
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }) ⊆
    support { toFinsupp := toFinsupp✝¹ } ∪ support { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
simp only [← ofFinsupp_add, support]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (toFinsupp✝¹ + toFinsupp✝).support ⊆ toFinsupp✝¹.support ∪ toFinsupp✝.support
[PROOFSTEP]
exact support_add
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
src✝ : R →ₗ[R] R[X] := monomial 0
⊢ AddHom.toFun src✝.toAddHom 1 = 1
[PROOFSTEP]
simp [monomial_zero_one]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
src✝ : R →ₗ[R] R[X] := monomial 0
⊢ ∀ (x y : R),
    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : 1 = 1) } (x * y) =
      OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : 1 = 1) } x *
        OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : 1 = 1) } y
[PROOFSTEP]
simp [monomial_mul_monomial]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
src✝ : R →ₗ[R] R[X] := monomial 0
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : 1 = 1) },
          map_mul' := (_ : ∀ (a a_1 : R), ↑(monomial 0) (a * a_1) = ↑(monomial 0) a * ↑(monomial 0) a_1) })
      0 =
    0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑C 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑C (bit1 a) = bit1 (↑C a)
[PROOFSTEP]
simp [bit1, C_bit0]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑C a * ↑(monomial n) b = ↑(monomial n) (a * b)
[PROOFSTEP]
simp only [← monomial_zero_left, monomial_mul_monomial, zero_add]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑(monomial n) a * ↑C b = ↑(monomial n) (a * b)
[PROOFSTEP]
simp only [← monomial_zero_left, monomial_mul_monomial, add_zero]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ ↑(monomial n) 1 = X ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑(monomial Nat.zero) 1 = X ^ Nat.zero
[PROOFSTEP]
simp [monomial_zero_one]
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : ↑(monomial n) 1 = X ^ n
⊢ ↑(monomial (Nat.succ n)) 1 = X ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, add_comm, one_mul]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ X * p = p * X
[PROOFSTEP]
rcases p with
  ⟨⟩
    -- Porting note: `ofFinsupp.injEq` is required.
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ X * { toFinsupp := toFinsupp✝ } = { toFinsupp := toFinsupp✝ } * X
[PROOFSTEP]
simp only [X, ← ofFinsupp_single, ← ofFinsupp_mul, LinearMap.coe_mk, ofFinsupp.injEq]
  -- Porting note: Was `ext`.
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ Finsupp.single 1 1 * toFinsupp✝ = toFinsupp✝ * Finsupp.single 1 1
[PROOFSTEP]
refine Finsupp.ext fun _ => ?_
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
x✝ : ℕ
⊢ ↑(Finsupp.single 1 1 * toFinsupp✝) x✝ = ↑(toFinsupp✝ * Finsupp.single 1 1) x✝
[PROOFSTEP]
simp [AddMonoidAlgebra.mul_apply, AddMonoidAlgebra.sum_single_index, add_comm]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ X ^ n * p = p * X ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ X ^ Nat.zero * p = p * X ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ Nat.succ n * p = p * X ^ Nat.succ n
[PROOFSTEP]
conv_lhs => rw [pow_succ']
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
| X ^ Nat.succ n * p
[PROOFSTEP]
rw [pow_succ']
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
| X ^ Nat.succ n * p
[PROOFSTEP]
rw [pow_succ']
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
| X ^ Nat.succ n * p
[PROOFSTEP]
rw [pow_succ']
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * X * p = p * X ^ Nat.succ n
[PROOFSTEP]
rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ']
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * X ^ n * q = p * q * X ^ n
[PROOFSTEP]
rw [mul_assoc, X_pow_mul, ← mul_assoc]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ ↑(monomial n) r * X = ↑(monomial (n + 1)) r
[PROOFSTEP]
erw [monomial_mul_monomial, mul_one]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
⊢ ↑(monomial n) r * X ^ k = ↑(monomial (n + k)) r
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ ↑(monomial n) r * X ^ Nat.zero = ↑(monomial (n + Nat.zero)) r
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
ih : ↑(monomial n) r * X ^ k = ↑(monomial (n + k)) r
⊢ ↑(monomial n) r * X ^ Nat.succ k = ↑(monomial (n + Nat.succ k)) r
[PROOFSTEP]
simp [ih, pow_succ', ← mul_assoc, add_assoc]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ X * ↑(monomial n) r = ↑(monomial (n + 1)) r
[PROOFSTEP]
rw [X_mul, monomial_mul_X]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
k n : ℕ
r : R
⊢ X ^ k * ↑(monomial n) r = ↑(monomial (n + k)) r
[PROOFSTEP]
rw [X_pow_mul, monomial_mul_X_pow]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
p : AddMonoidAlgebra R ℕ
⊢ coeff { toFinsupp := p } = ↑p
[PROOFSTEP]
rw [coeff]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ Injective coeff
[PROOFSTEP]
rintro ⟨p⟩
  ⟨q⟩
      -- Porting note: `ofFinsupp.injEq` is required.
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
p q : AddMonoidAlgebra R ℕ
⊢ coeff { toFinsupp := p } = coeff { toFinsupp := q } → { toFinsupp := p } = { toFinsupp := q }
[PROOFSTEP]
simp only [coeff, FunLike.coe_fn_eq, imp_self, ofFinsupp.injEq]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q f : R[X]
i : ℕ
⊢ ↑f.toFinsupp i = coeff f i
[PROOFSTEP]
cases f
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑{ toFinsupp := toFinsupp✝ }.toFinsupp i = coeff { toFinsupp := toFinsupp✝ } i
[PROOFSTEP]
rfl
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (↑(monomial n) a) m = if n = m then a else 0
[PROOFSTEP]
rw [← ofFinsupp_single]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff { toFinsupp := Finsupp.single n a } m = if n = m then a else 0
[PROOFSTEP]
simp only [coeff, LinearMap.coe_mk]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑(Finsupp.single n a) m = if n = m then a else 0
[PROOFSTEP]
rw [Finsupp.single_apply]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff 1 0 = 1
[PROOFSTEP]
rw [← monomial_zero_one, coeff_monomial]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (if 0 = 0 then 1 else 0) = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (↑(monomial (n + 1)) a) 0 = 0
[PROOFSTEP]
simp [coeff_monomial]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≠ 1
⊢ coeff X n = 0
[PROOFSTEP]
rw [coeff_X, if_neg hn.symm]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ n ∈ support p ↔ coeff p n ≠ 0
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ n ∈ support { toFinsupp := toFinsupp✝ } ↔ coeff { toFinsupp := toFinsupp✝ } n ≠ 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ¬n ∈ support p ↔ coeff p n = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (↑C a) n = if n = 0 then a else 0
[PROOFSTEP]
convert coeff_monomial (a := a) (m := n) (n := 0) using 2
[GOAL]
case h.e'_3.h₁.a
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ n = 0 ↔ 0 = n
[PROOFSTEP]
simp [eq_comm]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
h : n ≠ 0
⊢ coeff (↑C a) n = 0
[PROOFSTEP]
rw [coeff_C, if_neg h]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
r : R
n : ℕ
⊢ coeff (↑C r) (n + 1) = 0
[PROOFSTEP]
simp [coeff_C]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (↑m) n = ↑(if n = 0 then m else 0)
[PROOFSTEP]
simp only [← C_eq_nat_cast, coeff_C, Nat.cast_ite, Nat.cast_zero]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ ↑C a * X ^ (n + 1) = ↑(monomial (n + 1)) a
[PROOFSTEP]
rw [pow_succ', ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : R
n : ℕ
⊢ (↑C a * X ^ n).toFinsupp = Finsupp.single n a
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, toFinsupp_monomial]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑C a * X = ↑(monomial 1) a
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial, pow_one]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : R
⊢ (↑C a * X).toFinsupp = Finsupp.single 1 a
[PROOFSTEP]
rw [C_mul_X_eq_monomial, toFinsupp_monomial]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ Subsingleton R → Subsingleton R[X]
[PROOFSTEP]
intro
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a✝ : Subsingleton R
⊢ Subsingleton R[X]
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (∀ (f g : R[X]), f = g) ↔ ∀ (a b : R), a = b
[PROOFSTEP]
simpa only [← subsingleton_iff] using subsingleton_iff_subsingleton
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ p q : R[X]
⊢ p = q ↔ ∀ (n : ℕ), coeff p n = coeff q n
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q✝ q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝ } = q ↔ ∀ (n : ℕ), coeff { toFinsupp := toFinsupp✝ } n = coeff q n
[PROOFSTEP]
rcases q with
  ⟨⟩
    -- Porting note: Was `simp [coeff, FunLike.ext_iff]`
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝¹ } = { toFinsupp := toFinsupp✝ } ↔
    ∀ (n : ℕ), coeff { toFinsupp := toFinsupp✝¹ } n = coeff { toFinsupp := toFinsupp✝ } n
[PROOFSTEP]
simp [coeff]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ toFinsupp✝¹ = toFinsupp✝ ↔ ∀ (n : ℕ), ↑toFinsupp✝¹ n = ↑toFinsupp✝ n
[PROOFSTEP]
exact FunLike.ext_iff (F := ℕ →₀ R)
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a} = ⊤
[PROOFSTEP]
apply top_unique
[GOAL]
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ⊤ ≤ AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a}
[PROOFSTEP]
rw [← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv, ← Finsupp.add_closure_setOf_eq_single,
  AddMonoidHom.map_mclosure]
[GOAL]
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ AddSubmonoid.closure
      (↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ''
        {f | ∃ a b, f = Finsupp.single a b}) ≤
    AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a}
[PROOFSTEP]
refine' AddSubmonoid.closure_mono (Set.image_subset_iff.2 _)
[GOAL]
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ {f | ∃ a b, f = Finsupp.single a b} ⊆
    ↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ⁻¹'
      {p | ∃ n a, p = ↑(monomial n) a}
[PROOFSTEP]
rintro _ ⟨n, a, rfl⟩
[GOAL]
case h.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ Finsupp.single n a ∈
    ↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ⁻¹'
      {p | ∃ n a, p = ↑(monomial n) a}
[PROOFSTEP]
exact ⟨n, a, Polynomial.ofFinsupp_single _ _⟩
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
M : Type u_1
inst✝ : AddMonoid M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
⊢ Set.EqOn ↑f ↑g {p | ∃ n a, p = ↑(monomial n) a}
[PROOFSTEP]
rintro p ⟨n, a, rfl⟩
[GOAL]
case intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
M : Type u_1
inst✝ : AddMonoid M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
n : ℕ
a : R
⊢ ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
[PROOFSTEP]
exact h n a
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
h : 0 = 1
p : R[X]
⊢ p = 0
[PROOFSTEP]
rw [← one_smul R p, ← h, zero_smul]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
H : a ≠ 0
⊢ support (↑(monomial n) a) = {n}
[PROOFSTEP]
rw [← ofFinsupp_single, support]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
H : a ≠ 0
⊢ (match { toFinsupp := Finsupp.single n a } with
    | { toFinsupp := p } => p.support) =
    {n}
[PROOFSTEP]
exact Finsupp.support_single_ne_zero _ H
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ support (↑(monomial n) a) ⊆ {n}
[PROOFSTEP]
rw [← ofFinsupp_single, support]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ (match { toFinsupp := Finsupp.single n a } with
    | { toFinsupp := p } => p.support) ⊆
    {n}
[PROOFSTEP]
exact Finsupp.support_single_subset
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
c : R
h : c ≠ 0
⊢ support (↑C c * X) = {1}
[PROOFSTEP]
rw [C_mul_X_eq_monomial, support_monomial 1 h]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
c : R
⊢ support (↑C c * X) ⊆ {1}
[PROOFSTEP]
simpa only [C_mul_X_eq_monomial] using support_monomial' 1 c
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
c : R
h : c ≠ 0
⊢ support (↑C c * X ^ n) = {n}
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, support_monomial n h]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
c : R
⊢ support (↑C c * X ^ n) ⊆ {n}
[PROOFSTEP]
simpa only [C_mul_X_pow_eq_monomial] using support_monomial' n c
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ X ^ n = ↑(monomial n) 1
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ X ^ Nat.zero = ↑(monomial Nat.zero) 1
[PROOFSTEP]
rw [pow_zero, monomial_zero_one]
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : X ^ n = ↑(monomial n) 1
⊢ X ^ Nat.succ n = ↑(monomial (Nat.succ n)) 1
[PROOFSTEP]
rw [pow_succ', hn, X, monomial_mul_monomial, one_mul]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (X ^ n).toFinsupp = Finsupp.single n 1
[PROOFSTEP]
rw [X_pow_eq_monomial, toFinsupp_monomial]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ a • X ^ n = ↑(monomial n) a
[PROOFSTEP]
rw [X_pow_eq_monomial, smul_monomial, smul_eq_mul, mul_one]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
H : ¬1 = 0
n : ℕ
⊢ support (X ^ n) = {n}
[PROOFSTEP]
convert support_monomial n H
[GOAL]
case h.e'_2.h.e'_3
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
H : ¬1 = 0
n : ℕ
⊢ X ^ n = ↑(monomial n) 1
[PROOFSTEP]
exact X_pow_eq_monomial n
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
H : 1 = 0
⊢ support X = ∅
[PROOFSTEP]
rw [X, H, monomial_zero_right, support_zero]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
H : ¬1 = 0
⊢ support X = {1}
[PROOFSTEP]
rw [← pow_one X, support_X_pow H 1]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : R
ha : a ≠ 0
i j : ℕ
⊢ ↑(monomial i) a = ↑(monomial j) a ↔ i = j
[PROOFSTEP]
rw [← ofFinsupp_single, ← ofFinsupp_single, ofFinsupp.injEq, Finsupp.single_left_inj ha]
[GOAL]
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ ↑C u * X ^ k + ↑C v * X ^ l = ↑C u * X ^ m + ↑C v * X ^ n ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
[PROOFSTEP]
simp_rw [C_mul_X_pow_eq_monomial, ← toFinsupp_inj, toFinsupp_add, toFinsupp_monomial]
[GOAL]
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ Finsupp.single k u + Finsupp.single l v = Finsupp.single m u + Finsupp.single n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
[PROOFSTEP]
exact Finsupp.single_add_single_eq_single_add_single hu hv
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ p * q = ∑ i in support p, sum q fun j a => ↑(monomial (i + j)) (coeff p i * a)
[PROOFSTEP]
apply toFinsupp_injective
[GOAL]
case a
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp = (∑ i in support p, sum q fun j a => ↑(monomial (i + j)) (coeff p i * a)).toFinsupp
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case a.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } * q).toFinsupp =
    (∑ i in support { toFinsupp := toFinsupp✝ },
        sum q fun j a => ↑(monomial (i + j)) (coeff { toFinsupp := toFinsupp✝ } i * a)).toFinsupp
[PROOFSTEP]
rcases q with ⟨⟩
[GOAL]
case a.ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    (∑ i in support { toFinsupp := toFinsupp✝¹ },
        sum { toFinsupp := toFinsupp✝ } fun j a =>
          ↑(monomial (i + j)) (coeff { toFinsupp := toFinsupp✝¹ } i * a)).toFinsupp
[PROOFSTEP]
simp [support, sum, coeff, toFinsupp_sum]
[GOAL]
case a.ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ toFinsupp✝¹ * toFinsupp✝ =
    ∑ x in toFinsupp✝¹.support, ∑ x_1 in toFinsupp✝.support, Finsupp.single (x + x_1) (↑toFinsupp✝¹ x * ↑toFinsupp✝ x_1)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
f : ℕ → R → S
⊢ sum 0 f = 0
[PROOFSTEP]
simp [sum]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ sum (p + q) f = sum p f + sum q f
[PROOFSTEP]
rw [show p + q = ⟨p.toFinsupp + q.toFinsupp⟩ from add_def p q]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ sum { toFinsupp := p.toFinsupp + q.toFinsupp } f = sum p f + sum q f
[PROOFSTEP]
exact Finsupp.sum_add_index (fun i _ ↦ hf i) (fun a _ b₁ b₂ ↦ h_add a b₁ b₂)
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f g : ℕ → R → S
⊢ sum p (f + g) = sum p f + sum p g
[PROOFSTEP]
simp [sum_def, Finset.sum_add_distrib]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
⊢ (sum p fun n a => ↑C a * X ^ n) = p
[PROOFSTEP]
simp_rw [C_mul_X_pow_eq_monomial, sum_monomial_eq]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ (erase n p).toFinsupp = Finsupp.erase n p.toFinsupp
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (erase n { toFinsupp := toFinsupp✝ }).toFinsupp = Finsupp.erase n { toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
simp only [erase_def]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q : R[X]
p : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := Finsupp.erase n p } = erase n { toFinsupp := p }
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case mk
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
support✝ : Finset ℕ
toFun✝ : ℕ → R
mem_support_toFun✝ : ∀ (a : ℕ), a ∈ support✝ ↔ toFun✝ a ≠ 0
⊢ { toFinsupp := Finsupp.erase n { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } } =
    erase n { toFinsupp := { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } }
[PROOFSTEP]
simp only [erase_def]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ support (erase n p) = Finset.erase (support p) n
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (erase n { toFinsupp := toFinsupp✝ }) = Finset.erase (support { toFinsupp := toFinsupp✝ }) n
[PROOFSTEP]
simp only [support, erase_def, Finsupp.support_erase]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ (↑(monomial n) (coeff p n) + erase n p).toFinsupp = p.toFinsupp
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (↑(monomial n) (coeff { toFinsupp := toFinsupp✝ } n) + erase n { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
rw [toFinsupp_add, toFinsupp_monomial, toFinsupp_erase, coeff]
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ Finsupp.single n
        ((match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝ } with
          | { toFinsupp := p } => ↑p)
          n) +
      Finsupp.erase n { toFinsupp := toFinsupp✝ }.toFinsupp =
    { toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
exact Finsupp.single_add_erase _ _
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n i : ℕ
⊢ coeff (erase n p) i = if i = n then 0 else coeff p i
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (erase n { toFinsupp := toFinsupp✝ }) i = if i = n then 0 else coeff { toFinsupp := toFinsupp✝ } i
[PROOFSTEP]
simp only [erase_def, coeff]
  -- Porting note: Was `convert rfl`.
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(Finsupp.erase n toFinsupp✝) i = if i = n then 0 else ↑toFinsupp✝ i
[PROOFSTEP]
exact ite_congr rfl (fun _ => rfl) (fun _ => rfl)
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (erase n 0).toFinsupp = 0.toFinsupp
[PROOFSTEP]
simp
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ (erase n (↑(monomial n) a)).toFinsupp = 0.toFinsupp
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ coeff (erase n p) n = 0
[PROOFSTEP]
simp [coeff_erase]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n i : ℕ
h : i ≠ n
⊢ coeff (erase n p) i = coeff p i
[PROOFSTEP]
simp [coeff_erase, h]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
⊢ coeff (update p n a) = Function.update (coeff p) n a
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
x✝ : ℕ
⊢ coeff (update p n a) x✝ = Function.update (coeff p) n a x✝
[PROOFSTEP]
cases p
[GOAL]
case h.ofFinsupp
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
x✝ : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (update { toFinsupp := toFinsupp✝ } n a) x✝ = Function.update (coeff { toFinsupp := toFinsupp✝ }) n a x✝
[PROOFSTEP]
simp only [coeff, update, Function.update_apply, coe_update]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
i : ℕ
⊢ coeff (update p n a) i = if i = n then a else coeff p i
[PROOFSTEP]
rw [coeff_update, Function.update_apply]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
⊢ coeff (update p n a) n = a
[PROOFSTEP]
rw [p.coeff_update_apply, if_pos rfl]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
i : ℕ
h : i ≠ n
⊢ coeff (update p n a) i = coeff p i
[PROOFSTEP]
rw [p.coeff_update_apply, if_neg h]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ update p n 0 = erase n p
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
a b : R
m n✝¹ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n n✝ : ℕ
⊢ coeff (update p n 0) n✝ = coeff (erase n p) n✝
[PROOFSTEP]
rw [coeff_update_apply, coeff_erase]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ support (update p n a) = if a = 0 then Finset.erase (support p) n else insert n (support p)
[PROOFSTEP]
classical
cases p
simp only [support, update, Finsupp.support_update]
congr
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ support (update p n a) = if a = 0 then Finset.erase (support p) n else insert n (support p)
[PROOFSTEP]
cases p
[GOAL]
case ofFinsupp
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (update { toFinsupp := toFinsupp✝ } n a) =
    if a = 0 then Finset.erase (support { toFinsupp := toFinsupp✝ }) n
    else insert n (support { toFinsupp := toFinsupp✝ })
[PROOFSTEP]
simp only [support, update, Finsupp.support_update]
[GOAL]
case ofFinsupp
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (if a = 0 then Finset.erase toFinsupp✝.support n else insert n toFinsupp✝.support) =
    if a = 0 then Finset.erase toFinsupp✝.support n else insert n toFinsupp✝.support
[PROOFSTEP]
congr
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ support (update p n 0) = Finset.erase (support p) n
[PROOFSTEP]
rw [update_zero_eq_erase, support_erase]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ support (update p n a) = insert n (support p)
[PROOFSTEP]
classical rw [support_update, if_neg ha]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ support (update p n a) = insert n (support p)
[PROOFSTEP]
rw [support_update, if_neg ha]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ coeff (-p) n = -coeff p n
[PROOFSTEP]
rcases p with
  ⟨⟩
    -- Porting note: The last rule should be `apply`ed.
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (-{ toFinsupp := toFinsupp✝ }) n = -coeff { toFinsupp := toFinsupp✝ } n
[PROOFSTEP]
rw [← ofFinsupp_neg, coeff, coeff]
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (match (motive := R[X] → ℕ → R) { toFinsupp := -toFinsupp✝ } with
      | { toFinsupp := p } => ↑p)
      n =
    -(match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝ } with
        | { toFinsupp := p } => ↑p)
        n
[PROOFSTEP]
apply Finsupp.neg_apply
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
p q : R[X]
n : ℕ
⊢ coeff (p - q) n = coeff p n - coeff q n
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝ } - q) n = coeff { toFinsupp := toFinsupp✝ } n - coeff q n
[PROOFSTEP]
rcases q with
  ⟨⟩
    -- Porting note: The last rule should be `apply`ed.
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝¹ } - { toFinsupp := toFinsupp✝ }) n =
    coeff { toFinsupp := toFinsupp✝¹ } n - coeff { toFinsupp := toFinsupp✝ } n
[PROOFSTEP]
rw [← ofFinsupp_sub, coeff, coeff, coeff]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝¹ - toFinsupp✝ } with
      | { toFinsupp := p } => ↑p)
      n =
    (match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝¹ } with
        | { toFinsupp := p } => ↑p)
        n -
      (match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝ } with
        | { toFinsupp := p } => ↑p)
        n
[PROOFSTEP]
apply Finsupp.sub_apply
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℕ
a : R
⊢ ↑(monomial n) (-a) = -↑(monomial n) a
[PROOFSTEP]
rw [eq_neg_iff_add_eq_zero, ← monomial_add, neg_add_self, monomial_zero_right]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
p : R[X]
⊢ support (-p) = support p
[PROOFSTEP]
rcases p with
  ⟨⟩
    -- Porting note: The last rule should be `apply`ed.
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (-{ toFinsupp := toFinsupp✝ }) = support { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
rw [← ofFinsupp_neg, support, support]
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (match { toFinsupp := -toFinsupp✝ } with
    | { toFinsupp := p } => p.support) =
    match { toFinsupp := toFinsupp✝ } with
    | { toFinsupp := p } => p.support
[PROOFSTEP]
apply Finsupp.support_neg
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℤ
⊢ ↑C ↑n = ↑n
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ Nontrivial R[X]
[PROOFSTEP]
have h : Nontrivial (AddMonoidAlgebra R ℕ) := by infer_instance
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ Nontrivial (AddMonoidAlgebra R ℕ)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
h : Nontrivial (AddMonoidAlgebra R ℕ)
⊢ Nontrivial R[X]
[PROOFSTEP]
rcases h.exists_pair_ne with ⟨x, y, hxy⟩
[GOAL]
case intro.intro
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
h : Nontrivial (AddMonoidAlgebra R ℕ)
x y : AddMonoidAlgebra R ℕ
hxy : x ≠ y
⊢ Nontrivial R[X]
[PROOFSTEP]
refine' ⟨⟨⟨x⟩, ⟨y⟩, _⟩⟩
[GOAL]
case intro.intro
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
h : Nontrivial (AddMonoidAlgebra R ℕ)
x y : AddMonoidAlgebra R ℕ
hxy : x ≠ y
⊢ { toFinsupp := x } ≠ { toFinsupp := y }
[PROOFSTEP]
simp [hxy]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬coeff X 1 = coeff 0 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : DivisionRing R
a : ℚ
f : R[X]
⊢ a • f = ↑C ↑a * f
[PROOFSTEP]
rw [← Rat.smul_one_eq_coe, ← Polynomial.smul_C, C_1, smul_one_mul]


[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
⊢ enumerate sel s 0 = none
[PROOFSTEP]
simp [h, enumerate]
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
n : ℕ
⊢ enumerate sel s (n + 1) = none
[PROOFSTEP]
simp [h, enumerate]
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
n : ℕ
⊢ (do
      let a ← none
      enumerate sel (s \ {a}) n) =
    none
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
⊢ enumerate sel s m = none
[PROOFSTEP]
cases hs : sel s
[GOAL]
case none
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
hs : sel s = none
⊢ enumerate sel s m = none
[PROOFSTEP]
exact enumerate_eq_none_of_sel sel hs
[GOAL]
case some
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
val✝ : α
hs : sel s = some val✝
⊢ enumerate sel s m = none
[PROOFSTEP]
cases m
[GOAL]
case some.zero
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
hm : n + 1 ≤ Nat.zero
⊢ enumerate sel s Nat.zero = none
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
n✝ : ℕ
hm : n + 1 ≤ Nat.succ n✝
⊢ enumerate sel s (Nat.succ n✝) = none
[PROOFSTEP]
case zero => contradiction
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
hm : n + 1 ≤ Nat.zero
⊢ enumerate sel s Nat.zero = none
[PROOFSTEP]
case zero => contradiction
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
hm : n + 1 ≤ Nat.zero
⊢ enumerate sel s Nat.zero = none
[PROOFSTEP]
contradiction
[GOAL]
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
n✝ : ℕ
hm : n + 1 ≤ Nat.succ n✝
⊢ enumerate sel s (Nat.succ n✝) = none
[PROOFSTEP]
case succ m' =>
  simp [hs, enumerate] at h ⊢
  have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
  exact enumerate_eq_none h hm
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ Nat.succ m'
⊢ enumerate sel s (Nat.succ m') = none
[PROOFSTEP]
case succ m' =>
  simp [hs, enumerate] at h ⊢
  have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
  exact enumerate_eq_none h hm
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ Nat.succ m'
⊢ enumerate sel s (Nat.succ m') = none
[PROOFSTEP]
simp [hs, enumerate] at h ⊢
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ Nat.succ m'
h :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) n) =
    none
⊢ (do
      let a ← some val✝
      enumerate sel (s \ {a}) m') =
    none
[PROOFSTEP]
have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm✝ : n + 1 ≤ Nat.succ m'
h :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) n) =
    none
hm : n ≤ m'
⊢ (do
      let a ← some val✝
      enumerate sel (s \ {a}) m') =
    none
[PROOFSTEP]
exact enumerate_eq_none h hm
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
cases h : sel s
[GOAL]
case none
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
h : sel s = none
⊢ enumerate sel s (n + 1) = some a → a ∈ s
case some
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a val✝ : α
h : sel s = some val✝
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
case none => simp [enumerate_eq_none_of_sel, h]
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
h : sel s = none
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
case none => simp [enumerate_eq_none_of_sel, h]
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
h : sel s = none
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
simp [enumerate_eq_none_of_sel, h]
[GOAL]
case some
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a val✝ : α
h : sel s = some val✝
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
case some a' =>
  simp [enumerate, h]
  exact fun h' : enumerate sel (s \ { a' }) n = some a ↦
    have : a ∈ s \ { a' } := enumerate_mem h_sel h'
    this.left
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
case some a' =>
  simp [enumerate, h]
  exact fun h' : enumerate sel (s \ { a' }) n = some a ↦
    have : a ∈ s \ { a' } := enumerate_mem h_sel h'
    this.left
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
simp [enumerate, h]
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ (do
        let a ← some a'
        enumerate sel (s \ {a}) n) =
      some a →
    a ∈ s
[PROOFSTEP]
exact fun h' : enumerate sel (s \ { a' }) n = some a ↦
  have : a ∈ s \ { a' } := enumerate_mem h_sel h'
  this.left
[GOAL]
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
⊢ n₁ = n₂
[PROOFSTEP]
rcases le_total n₁ n₂ with (hn | hn)
[GOAL]
case inl
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₁ ≤ n₂
⊢ n₁ = n₂
case inr
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₂ ≤ n₁
⊢ n₁ = n₂
[PROOFSTEP]
on_goal 2 => swap_var n₁ ↔ n₂, h₁ ↔ h₂
[GOAL]
case inl
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₁ ≤ n₂
⊢ n₁ = n₂
case inr
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₂ ≤ n₁
⊢ n₁ = n₂
[PROOFSTEP]
on_goal 2 => swap_var n₁ ↔ n₂, h₁ ↔ h₂
[GOAL]
case inr
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₂ ≤ n₁
⊢ n₁ = n₂
[PROOFSTEP]
swap_var n₁ ↔ n₂, h₁ ↔ h₂
[GOAL]
case inl
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₁ ≤ n₂
⊢ n₁ = n₂
case inr
α : Type u_1
sel : Set α → Option α
n₂ n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₂ : enumerate sel s n₂ = some a
h₁ : enumerate sel s n₁ = some a
hn : n₁ ≤ n₂
⊢ n₂ = n₁
[PROOFSTEP]
all_goals
  rcases Nat.le.dest hn with ⟨m, rfl⟩
  clear hn
  induction n₁ generalizing s
  case zero =>
    cases m
    case zero => rfl
    case succ
      m =>
      have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
        exact h₂
      have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
      simp_all [Set.mem_diff_singleton]
  case succ k ih =>
    cases h : sel s
    case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
    case some
      _ =>
      simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
        Nat.succ.injEq]
      exact ih h₁ h₂
[GOAL]
case inl
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₁ ≤ n₂
⊢ n₁ = n₂
[PROOFSTEP]
rcases Nat.le.dest hn with ⟨m, rfl⟩
[GOAL]
case inl.intro
α : Type u_1
sel : Set α → Option α
n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
hn : n₁ ≤ n₁ + m
⊢ n₁ = n₁ + m
[PROOFSTEP]
clear hn
[GOAL]
case inl.intro
α : Type u_1
sel : Set α → Option α
n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
⊢ n₁ = n₁ + m
[PROOFSTEP]
induction n₁ generalizing s
[GOAL]
case inl.intro.zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero = Nat.zero + m
case inl.intro.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m n✝ : ℕ
n_ih✝ : ∀ {s : Set α}, enumerate sel s n✝ = some a → enumerate sel s (n✝ + m) = some a → n✝ = n✝ + m
s : Set α
h₁ : enumerate sel s (Nat.succ n✝) = some a
h₂ : enumerate sel s (Nat.succ n✝ + m) = some a
⊢ Nat.succ n✝ = Nat.succ n✝ + m
[PROOFSTEP]
case zero =>
  cases m
  case zero => rfl
  case succ
    m =>
    have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
      exact h₂
    have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
    simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero = Nat.zero + m
[PROOFSTEP]
case zero =>
  cases m
  case zero => rfl
  case succ
    m =>
    have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
      exact h₂
    have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
    simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero = Nat.zero + m
[PROOFSTEP]
cases m
[GOAL]
case zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero = Nat.zero + Nat.zero
case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
n✝ : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ n✝) = some a
⊢ Nat.zero = Nat.zero + Nat.succ n✝
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero = Nat.zero + Nat.zero
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero = Nat.zero + Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
n✝ : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ n✝) = some a
⊢ Nat.zero = Nat.zero + Nat.succ n✝
[PROOFSTEP]
case succ
  m =>
  have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
    exact h₂
  have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
  simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ Nat.zero = Nat.zero + Nat.succ m
[PROOFSTEP]
case succ
  m =>
  have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
    exact h₂
  have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
  simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ Nat.zero = Nat.zero + Nat.succ m
[PROOFSTEP]
have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
  exact h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ enumerate sel (s \ {a}) m = some a
[PROOFSTEP]
simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
m : ℕ
h₁ : sel s = some a
h₂ :
  (do
      let a ← some a
      enumerate sel (s \ {a}) m) =
    some a
⊢ enumerate sel (s \ {a}) m = some a
[PROOFSTEP]
exact h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
h' : enumerate sel (s \ {a}) m = some a
⊢ Nat.zero = Nat.zero + Nat.succ m
[PROOFSTEP]
have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
h' : enumerate sel (s \ {a}) m = some a
this : a ∈ s \ {a}
⊢ Nat.zero = Nat.zero + Nat.succ m
[PROOFSTEP]
simp_all [Set.mem_diff_singleton]
[GOAL]
case inl.intro.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m n✝ : ℕ
n_ih✝ : ∀ {s : Set α}, enumerate sel s n✝ = some a → enumerate sel s (n✝ + m) = some a → n✝ = n✝ + m
s : Set α
h₁ : enumerate sel s (Nat.succ n✝) = some a
h₂ : enumerate sel s (Nat.succ n✝ + m) = some a
⊢ Nat.succ n✝ = Nat.succ n✝ + m
[PROOFSTEP]
case succ k ih =>
  cases h : sel s
  case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
  case some
    _ =>
    simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
      Nat.succ.injEq]
    exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
case succ k ih =>
  cases h : sel s
  case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
  case some
    _ =>
    simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
      Nat.succ.injEq]
    exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
cases h : sel s
[GOAL]
case none
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k = Nat.succ k + m
case some
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
case some
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
case some
  _ =>
  simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
    Nat.succ.injEq]
  exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
case some
  _ =>
  simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
    Nat.succ.injEq]
  exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2, Nat.succ.injEq]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
s : Set α
val✝ : α
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (m + k) = some a → m = 0
h₁ :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) k) =
    some a
h₂ :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) (m + k)) =
    some a
h : sel s = some val✝
⊢ m = 0
[PROOFSTEP]
exact ih h₁ h₂
[GOAL]
case inr
α : Type u_1
sel : Set α → Option α
n₂ n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₂ : enumerate sel s n₂ = some a
h₁ : enumerate sel s n₁ = some a
hn : n₁ ≤ n₂
⊢ n₂ = n₁
[PROOFSTEP]
rcases Nat.le.dest hn with ⟨m, rfl⟩
[GOAL]
case inr.intro
α : Type u_1
sel : Set α → Option α
n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
hn : n₁ ≤ n₁ + m
⊢ n₁ + m = n₁
[PROOFSTEP]
clear hn
[GOAL]
case inr.intro
α : Type u_1
sel : Set α → Option α
n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
⊢ n₁ + m = n₁
[PROOFSTEP]
induction n₁ generalizing s
[GOAL]
case inr.intro.zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero + m = Nat.zero
case inr.intro.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m n✝ : ℕ
n_ih✝ : ∀ {s : Set α}, enumerate sel s n✝ = some a → enumerate sel s (n✝ + m) = some a → n✝ + m = n✝
s : Set α
h₁ : enumerate sel s (Nat.succ n✝) = some a
h₂ : enumerate sel s (Nat.succ n✝ + m) = some a
⊢ Nat.succ n✝ + m = Nat.succ n✝
[PROOFSTEP]
case zero =>
  cases m
  case zero => rfl
  case succ
    m =>
    have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
      exact h₂
    have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
    simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero + m = Nat.zero
[PROOFSTEP]
case zero =>
  cases m
  case zero => rfl
  case succ
    m =>
    have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
      exact h₂
    have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
    simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero + m = Nat.zero
[PROOFSTEP]
cases m
[GOAL]
case zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero + Nat.zero = Nat.zero
case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
n✝ : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ n✝) = some a
⊢ Nat.zero + Nat.succ n✝ = Nat.zero
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero + Nat.zero = Nat.zero
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero + Nat.zero = Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
n✝ : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ n✝) = some a
⊢ Nat.zero + Nat.succ n✝ = Nat.zero
[PROOFSTEP]
case succ
  m =>
  have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
    exact h₂
  have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
  simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ Nat.zero + Nat.succ m = Nat.zero
[PROOFSTEP]
case succ
  m =>
  have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
    exact h₂
  have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
  simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ Nat.zero + Nat.succ m = Nat.zero
[PROOFSTEP]
have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
  exact h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ enumerate sel (s \ {a}) m = some a
[PROOFSTEP]
simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
m : ℕ
h₁ : sel s = some a
h₂ :
  (do
      let a ← some a
      enumerate sel (s \ {a}) m) =
    some a
⊢ enumerate sel (s \ {a}) m = some a
[PROOFSTEP]
exact h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
h' : enumerate sel (s \ {a}) m = some a
⊢ Nat.zero + Nat.succ m = Nat.zero
[PROOFSTEP]
have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
h' : enumerate sel (s \ {a}) m = some a
this : a ∈ s \ {a}
⊢ Nat.zero + Nat.succ m = Nat.zero
[PROOFSTEP]
simp_all [Set.mem_diff_singleton]
[GOAL]
case inr.intro.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m n✝ : ℕ
n_ih✝ : ∀ {s : Set α}, enumerate sel s n✝ = some a → enumerate sel s (n✝ + m) = some a → n✝ + m = n✝
s : Set α
h₁ : enumerate sel s (Nat.succ n✝) = some a
h₂ : enumerate sel s (Nat.succ n✝ + m) = some a
⊢ Nat.succ n✝ + m = Nat.succ n✝
[PROOFSTEP]
case succ k ih =>
  cases h : sel s
  case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
  case some
    _ =>
    simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
      Nat.succ.injEq]
    exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
case succ k ih =>
  cases h : sel s
  case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
  case some
    _ =>
    simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
      Nat.succ.injEq]
    exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
cases h : sel s
[GOAL]
case none
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k + m = Nat.succ k
case some
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
case some
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
case some
  _ =>
  simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
    Nat.succ.injEq]
  exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
case some
  _ =>
  simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
    Nat.succ.injEq]
  exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2, Nat.succ.injEq]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
s : Set α
val✝ : α
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (m + k) = some a → m + k = k
h₁ :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) k) =
    some a
h₂ :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) (m + k)) =
    some a
h : sel s = some val✝
⊢ m + k = k
[PROOFSTEP]
exact ih h₁ h₂


[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
⊢ WPath P (WType.mk a f) ⟹ α
[PROOFSTEP]
intro i x
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i : Fin2 n
x : WPath P (WType.mk a f) i
⊢ α i
[PROOFSTEP]
match x with
| WPath.root _ _ i c => exact g' i c
| WPath.child _ _ i j c => exact g j i c
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i✝ : Fin2 n
x : WPath P (WType.mk a f) i✝
i : Fin2 n
c : B (drop P) a i
⊢ α i
[PROOFSTEP]
exact g' i c
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i✝ : Fin2 n
x : WPath P (WType.mk a f) i✝
i : Fin2 n
j : PFunctor.B (last P) a
c : WPath P (f j) i
⊢ α i
[PROOFSTEP]
exact g j i c
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) = h
[PROOFSTEP]
ext i x
[GOAL]
case a.h
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
i : Fin2 n
x : WPath P (WType.mk a fun j => f j) i
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) i x = h i x
[PROOFSTEP]
cases x
[GOAL]
case a.h.root
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
i : Fin2 n
c✝ : B (drop P) a i
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) i (WPath.root a (fun j => f j) i c✝) =
    h i (WPath.root a (fun j => f j) i c✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.child
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
i : Fin2 n
j✝ : PFunctor.B (last P) a
c✝ : WPath P ((fun j => f j) j✝) i
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) i (WPath.child a (fun j => f j) i j✝ c✝) =
    h i (WPath.child a (fun j => f j) i j✝ c✝)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
⊢ h ⊚ wPathCasesOn P g' g = wPathCasesOn P (h ⊚ g') fun i => h ⊚ g i
[PROOFSTEP]
ext i x
[GOAL]
case a.h
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i : Fin2 n
x : WPath P (WType.mk a fun j => f j) i
⊢ (h ⊚ wPathCasesOn P g' g) i x = wPathCasesOn P (h ⊚ g') (fun i => h ⊚ g i) i x
[PROOFSTEP]
cases x
[GOAL]
case a.h.root
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i : Fin2 n
c✝ : B (drop P) a i
⊢ (h ⊚ wPathCasesOn P g' g) i (WPath.root a (fun j => f j) i c✝) =
    wPathCasesOn P (h ⊚ g') (fun i => h ⊚ g i) i (WPath.root a (fun j => f j) i c✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.child
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i : Fin2 n
j✝ : PFunctor.B (last P) a
c✝ : WPath P ((fun j => f j) j✝) i
⊢ (h ⊚ wPathCasesOn P g' g) i (WPath.child a (fun j => f j) i j✝ c✝) =
    wPathCasesOn P (h ⊚ g') (fun i => h ⊚ g i) i (WPath.child a (fun j => f j) i j✝ c✝)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
⊢ MvFunctor (W P)
[PROOFSTEP]
delta MvPFunctor.W
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
⊢ MvFunctor fun α => Obj (wp P) α
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ wRec P g (wMk P a f' f) = g a f' f fun i => wRec P g (f i)
[PROOFSTEP]
rw [wMk, wRec]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (match
      let g := fun i => (f i).fst;
      let g' := wPathCasesOn P f' fun i => (f i).snd;
      { fst := WType.mk a g, snd := g' } with
    | { fst := a, snd := f' } =>
      let g' := fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h';
      wpRec P g' a f') =
    g a f' f fun i => wRec P g (f i)
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
      (WType.mk a fun i => (f i).fst) (wPathCasesOn P f' fun i => (f i).snd) =
    g a f' f fun i => wRec P g (f i)
[PROOFSTEP]
rw [wpRec_eq]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g a (wPathDestLeft P (wPathCasesOn P f' fun i => (f i).snd))
      (fun i => { fst := (f i).fst, snd := wPathDestRight P (wPathCasesOn P f' fun i => (f i).snd) i }) fun i =>
      wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
        (f i).fst (wPathDestRight P (wPathCasesOn P f' fun i => (f i).snd) i)) =
    g a f' f fun i => wRec P g (f i)
[PROOFSTEP]
dsimp only [wPathDestLeft_wPathCasesOn, wPathDestRight_wPathCasesOn]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g a f' (fun i => { fst := (f i).fst, snd := (f i).snd }) fun i =>
      wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
        (f i).fst (f i).snd) =
    g a f' f fun i => wRec P g (f i)
[PROOFSTEP]
congr
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
⊢ ∀ (x : W P α), C x
[PROOFSTEP]
intro x
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
x : W P α
⊢ C x
[PROOFSTEP]
cases' x with a f
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a : (wp P).A
f : B (wp P) a ⟹ α
⊢ C { fst := a, snd := f }
[PROOFSTEP]
apply @wp_ind n P α fun a f => C ⟨a, f⟩
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a : (wp P).A
f : B (wp P) a ⟹ α
⊢ ∀ (a : P.A) (f : PFunctor.B (last P) a → PFunctor.W (last P)) (f' : WPath P (WType.mk a f) ⟹ α),
    (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
      C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
intro a f f' ih'
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
dsimp [wMk] at ih
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
let ih'' := ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' : (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
  C
    { fst := WType.mk a fun i => { fst := f i, snd := wPathDestRight P f' i }.fst,
      snd := wPathCasesOn P (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }.snd } :=
  ih a (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
dsimp at ih''
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' : (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
  C { fst := WType.mk a fun i => f i, snd := wPathCasesOn P (wPathDestLeft P f') fun i => wPathDestRight P f' i } :=
  ih a (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
rw [wPathCasesOn_eta] at ih''
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' :
  (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
    C { fst := WType.mk a fun i => f i, snd := f' }
⊢ C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
apply ih''
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' :
  (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
    C { fst := WType.mk a fun i => f i, snd := f' }
⊢ ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
[PROOFSTEP]
apply ih'
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ g <$$> wMk P a f' f = wMk P a (g ⊚ f') fun i => g <$$> f i
[PROOFSTEP]
show _ = P.wMk a (g ⊚ f') (MvFunctor.map g ∘ f)
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ g <$$> wMk P a f' f = wMk P a (g ⊚ f') (MvFunctor.map g ∘ f)
[PROOFSTEP]
have : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩ :=
  by
  ext i : 1
  dsimp [Function.comp]
  cases f i
  rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
ext i : 1
[GOAL]
case h
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
i : PFunctor.B (last P) a
⊢ (MvFunctor.map g ∘ f) i = { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
dsimp [Function.comp]
[GOAL]
case h
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
i : PFunctor.B (last P) a
⊢ g <$$> f i = { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
cases f i
[GOAL]
case h.mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
i : PFunctor.B (last P) a
fst✝ : (wp P).A
snd✝ : B (wp P) fst✝ ⟹ α
⊢ g <$$> { fst := fst✝, snd := snd✝ } =
    { fst := { fst := fst✝, snd := snd✝ }.fst, snd := g ⊚ { fst := fst✝, snd := snd✝ }.snd }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
⊢ g <$$> wMk P a f' f = wMk P a (g ⊚ f') (MvFunctor.map g ∘ f)
[PROOFSTEP]
rw [this]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
⊢ g <$$> wMk P a f' f = wMk P a (g ⊚ f') fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
have : f = fun i => ⟨(f i).fst, (f i).snd⟩ := by
  ext1 x
  cases f x
  rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
⊢ f = fun i => { fst := (f i).fst, snd := (f i).snd }
[PROOFSTEP]
ext1 x
[GOAL]
case h
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
x : PFunctor.B (last P) a
⊢ f x = { fst := (f x).fst, snd := (f x).snd }
[PROOFSTEP]
cases f x
[GOAL]
case h.mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
x : PFunctor.B (last P) a
fst✝ : (wp P).A
snd✝ : B (wp P) fst✝ ⟹ α
⊢ { fst := fst✝, snd := snd✝ } = { fst := { fst := fst✝, snd := snd✝ }.fst, snd := { fst := fst✝, snd := snd✝ }.snd }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this✝ : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
this : f = fun i => { fst := (f i).fst, snd := (f i).snd }
⊢ g <$$> wMk P a f' f = wMk P a (g ⊚ f') fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
rw [this]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this✝ : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
this : f = fun i => { fst := (f i).fst, snd := (f i).snd }
⊢ (g <$$> wMk P a f' fun i => { fst := (f i).fst, snd := (f i).snd }) =
    wMk P a (g ⊚ f') fun i =>
      { fst := ((fun i => { fst := (f i).fst, snd := (f i).snd }) i).fst,
        snd := g ⊚ ((fun i => { fst := (f i).fst, snd := (f i).snd }) i).snd }
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this✝ : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
this : f = fun i => { fst := (f i).fst, snd := (f i).snd }
⊢ (g <$$> wMk P a f' fun i => { fst := (f i).fst, snd := (f i).snd }) =
    wMk P a (g ⊚ f') fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
rw [wMk_eq, wMk_eq]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this✝ : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
this : f = fun i => { fst := (f i).fst, snd := (f i).snd }
⊢ g <$$> { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd } =
    { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P (g ⊚ f') fun i => g ⊚ (f i).snd }
[PROOFSTEP]
have h := MvPFunctor.map_eq P.wp g
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this✝ : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
this : f = fun i => { fst := (f i).fst, snd := (f i).snd }
h : ∀ (a : (wp P).A) (f : B (wp P) a ⟹ α), g <$$> { fst := a, snd := f } = { fst := a, snd := g ⊚ f }
⊢ g <$$> { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd } =
    { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P (g ⊚ f') fun i => g ⊚ (f i).snd }
[PROOFSTEP]
rw [h, comp_wPathCasesOn]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α γ : TypeVec n
g : α ⟹ γ
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g ::: wMap P g) <$$> objAppend1 P a f' f = objAppend1 P a (g ⊚ f') fun x => wMap P g (f x)
[PROOFSTEP]
rw [objAppend1, objAppend1, map_eq, appendFun, ← splitFun_comp]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α γ : TypeVec n
g : α ⟹ γ
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ { fst := a, snd := splitFun (g ⊚ f') (wMap P g ∘ f) } = { fst := a, snd := splitFun (g ⊚ f') fun x => wMap P g (f x) }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ wDest' P (wMk P a f' f) = { fst := a, snd := splitFun f' f }
[PROOFSTEP]
rw [wDest', wRec_eq]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
x : Obj P (α ::: W P α)
⊢ wDest' P (wMk' P x) = x
[PROOFSTEP]
cases' x with a f
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : B P a ⟹ α ::: W P α
⊢ wDest' P (wMk' P { fst := a, snd := f }) = { fst := a, snd := f }
[PROOFSTEP]
rw [wMk', wDest'_wMk, split_dropFun_lastFun]