[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
p : MvPolynomial (Fin n) R
h : ∀ (x : Fin n → R), ↑(eval x) p = 0
⊢ p = 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
p✝ : MvPolynomial (Fin n) R
h✝ : ∀ (x : Fin n → R), ↑(eval x) p✝ = 0
p : MvPolynomial (Fin Nat.zero) R
h : ∀ (x : Fin Nat.zero → R), ↑(eval x) p = 0
⊢ p = 0
[PROOFSTEP]
apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective
[GOAL]
case zero.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
p✝ : MvPolynomial (Fin n) R
h✝ : ∀ (x : Fin n → R), ↑(eval x) p✝ = 0
p : MvPolynomial (Fin Nat.zero) R
h : ∀ (x : Fin Nat.zero → R), ↑(eval x) p = 0
⊢ ↑(isEmptyRingEquiv R (Fin 0)) p = ↑(isEmptyRingEquiv R (Fin 0)) 0
[PROOFSTEP]
rw [RingEquiv.map_zero]
[GOAL]
case zero.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
p✝ : MvPolynomial (Fin n) R
h✝ : ∀ (x : Fin n → R), ↑(eval x) p✝ = 0
p : MvPolynomial (Fin Nat.zero) R
h : ∀ (x : Fin Nat.zero → R), ↑(eval x) p = 0
⊢ ↑(isEmptyRingEquiv R (Fin 0)) p = 0
[PROOFSTEP]
convert h finZeroElim
[GOAL]
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
⊢ p = 0
[PROOFSTEP]
apply (finSuccEquiv R n).injective
[GOAL]
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
⊢ ↑(finSuccEquiv R n) p = ↑(finSuccEquiv R n) 0
[PROOFSTEP]
simp only [AlgEquiv.map_zero]
[GOAL]
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
⊢ ↑(finSuccEquiv R n) p = 0
[PROOFSTEP]
refine Polynomial.funext fun q => ?_
[GOAL]
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
q : MvPolynomial (Fin n) R
⊢ Polynomial.eval q (↑(finSuccEquiv R n) p) = Polynomial.eval q 0
[PROOFSTEP]
rw [Polynomial.eval_zero]
[GOAL]
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
q : MvPolynomial (Fin n) R
⊢ Polynomial.eval q (↑(finSuccEquiv R n) p) = 0
[PROOFSTEP]
apply ih fun x => ?_
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
q : MvPolynomial (Fin n) R
x : Fin n → R
⊢ ↑(eval x) (Polynomial.eval q (↑(finSuccEquiv R n) p)) = 0
[PROOFSTEP]
calc
  _ = _ := eval_polynomial_eval_finSuccEquiv p _
  _ = 0 := h _
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
⊢ p = q
[PROOFSTEP]
suffices ∀ p, (∀ x : σ → R, eval x p = 0) → p = 0
  by
  rw [← sub_eq_zero, this (p - q)]
  simp only [h, RingHom.map_sub, forall_const, sub_self]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
⊢ p = q
[PROOFSTEP]
rw [← sub_eq_zero, this (p - q)]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
⊢ ∀ (x : σ → R), ↑(eval x) (p - q) = 0
[PROOFSTEP]
simp only [h, RingHom.map_sub, forall_const, sub_self]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
⊢ ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
[PROOFSTEP]
clear h p q
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
⊢ ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
[PROOFSTEP]
intro p h
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = 0
⊢ p = 0
[PROOFSTEP]
obtain ⟨n, f, hf, p, rfl⟩ := exists_fin_rename p
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
⊢ ↑(rename f) p = 0
[PROOFSTEP]
suffices p = 0 by rw [this, AlgHom.map_zero]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
this : p = 0
⊢ ↑(rename f) p = 0
[PROOFSTEP]
rw [this, AlgHom.map_zero]
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
⊢ p = 0
[PROOFSTEP]
apply funext_fin
[GOAL]
case intro.intro.intro.intro.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
⊢ ∀ (x : Fin n → R), ↑(eval x) p = 0
[PROOFSTEP]
intro x
[GOAL]
case intro.intro.intro.intro.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
x : Fin n → R
⊢ ↑(eval x) p = 0
[PROOFSTEP]
classical
convert h (Function.extend f x 0)
simp only [eval, eval₂Hom_rename, Function.extend_comp hf]
[GOAL]
case intro.intro.intro.intro.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
x : Fin n → R
⊢ ↑(eval x) p = 0
[PROOFSTEP]
convert h (Function.extend f x 0)
[GOAL]
case h.e'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
x : Fin n → R
⊢ ↑(eval x) p = ↑(eval (Function.extend f x 0)) (↑(rename f) p)
[PROOFSTEP]
simp only [eval, eval₂Hom_rename, Function.extend_comp hf]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
⊢ p = q → ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p : MvPolynomial σ R
⊢ ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) p
[PROOFSTEP]
simp only [forall_const, eq_self_iff_true]


[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
⊢ supported R s = AlgHom.range (rename Subtype.val)
[PROOFSTEP]
rw [supported, Set.image_eq_range, adjoin_range_eq_range_aeval, rename]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
⊢ AlgHom.range (aeval fun x => X ↑x) = AlgHom.range (aeval (X ∘ Subtype.val))
[PROOFSTEP]
congr
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
x : R
⊢ ↑(AlgEquiv.symm (supportedEquivMvPolynomial s)) (↑C x) = ↑(algebraMap R { x // x ∈ supported R s }) x
[PROOFSTEP]
ext1
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
x : R
⊢ ↑(↑(AlgEquiv.symm (supportedEquivMvPolynomial s)) (↑C x)) = ↑(↑(algebraMap R { x // x ∈ supported R s }) x)
[PROOFSTEP]
simp [supportedEquivMvPolynomial, MvPolynomial.algebraMap_eq]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
i : ↑s
⊢ ↑(↑(AlgEquiv.symm (supportedEquivMvPolynomial s)) (X i)) = X ↑i
[PROOFSTEP]
simp [supportedEquivMvPolynomial]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ p ∈ supported R s ↔ ↑(vars p) ⊆ s
[PROOFSTEP]
classical
rw [supported_eq_range_rename, AlgHom.mem_range]
constructor
· rintro ⟨p, rfl⟩
  refine' _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) _
  simp
· intro hs
  exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ p ∈ supported R s ↔ ↑(vars p) ⊆ s
[PROOFSTEP]
rw [supported_eq_range_rename, AlgHom.mem_range]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ (∃ x, ↑(rename Subtype.val) x = p) ↔ ↑(vars p) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ (∃ x, ↑(rename Subtype.val) x = p) → ↑(vars p) ⊆ s
[PROOFSTEP]
rintro ⟨p, rfl⟩
[GOAL]
case mp.intro
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
q : MvPolynomial σ R
s t : Set σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(vars (↑(rename Subtype.val) p)) ⊆ s
[PROOFSTEP]
refine' _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) _
[GOAL]
case mp.intro
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
q : MvPolynomial σ R
s t : Set σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(Finset.image Subtype.val (vars p)) ⊆ s
[PROOFSTEP]
simp
[GOAL]
case mpr
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ ↑(vars p) ⊆ s → ∃ x, ↑(rename Subtype.val) x = p
[PROOFSTEP]
intro hs
[GOAL]
case mpr
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
hs : ↑(vars p) ⊆ s
⊢ ∃ x, ↑(rename Subtype.val) x = p
[PROOFSTEP]
exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
hs : ↑(vars p) ⊆ s
⊢ ↑(vars p) ⊆ Set.range Subtype.val
[PROOFSTEP]
simpa
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
s t : Set σ
p : MvPolynomial σ R
⊢ p ∈ supported R ↑(vars p)
[PROOFSTEP]
rw [mem_supported]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ supported R Set.univ = ⊤
[PROOFSTEP]
simp [Algebra.eq_top_iff, mem_supported]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ supported R ∅ = ⊥
[PROOFSTEP]
simp [supported_eq_adjoin_X]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
i : σ
⊢ X i ∈ supported R s ↔ i ∈ s
[PROOFSTEP]
simp [mem_supported]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t ↔ s ⊆ t
[PROOFSTEP]
constructor
[GOAL]
case mp
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t → s ⊆ t
[PROOFSTEP]
intro h i
[GOAL]
case mp
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
h : supported R s ≤ supported R t
i : σ
⊢ i ∈ s → i ∈ t
[PROOFSTEP]
simpa using @h (X i)
[GOAL]
case mpr
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ s ⊆ t → supported R s ≤ supported R t
[PROOFSTEP]
exact supported_mono
[GOAL]
σ : Type u_1
τ : Type u_2
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_3
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ↑(vars F) ⊆ s
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = ↑(aeval x) F
[PROOFSTEP]
rw [← mem_supported, supported_eq_range_rename, AlgHom.mem_range] at hF
[GOAL]
σ : Type u_1
τ : Type u_2
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_3
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ∃ x, ↑(rename Subtype.val) x = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = ↑(aeval x) F
[PROOFSTEP]
cases' hF with F' hF'
[GOAL]
case intro
σ : Type u_1
τ : Type u_2
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_3
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : ↑(rename Subtype.val) F' = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = ↑(aeval x) F
[PROOFSTEP]
use fun z ↦ aeval z F'
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_3
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : ↑(rename Subtype.val) F' = F
⊢ ∀ (x : σ → R), ↑(aeval (x ∘ Subtype.val)) F' = ↑(aeval x) F
[PROOFSTEP]
intro x
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_3
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : ↑(rename Subtype.val) F' = F
x : σ → R
⊢ ↑(aeval (x ∘ Subtype.val)) F' = ↑(aeval x) F
[PROOFSTEP]
simp only [← hF', aeval_rename]


[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
⊢ pderiv i = mkDerivation R (Pi.single i 1)
[PROOFSTEP]
unfold pderiv
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
⊢ mkDerivation R (Pi.single i 1) = mkDerivation R (Pi.single i 1)
[PROOFSTEP]
congr!
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ ↑(pderiv i) (↑(monomial s) a) = ↑(monomial (s - single i 1)) (a * ↑(↑s i))
[PROOFSTEP]
classical
simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc, ← (monomial _).map_smul]
refine' (Finset.sum_eq_single i (fun j _ hne => _) fun hi => _).trans _
· simp [Pi.single_eq_of_ne hne]
· rw [Finsupp.not_mem_support_iff] at hi ; simp [hi]
· simp
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ ↑(pderiv i) (↑(monomial s) a) = ↑(monomial (s - single i 1)) (a * ↑(↑s i))
[PROOFSTEP]
simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc, ← (monomial _).map_smul]
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (sum s fun a_1 b => ↑(monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) =
    ↑(monomial (s - single i 1)) (a * ↑(↑s i))
[PROOFSTEP]
refine' (Finset.sum_eq_single i (fun j _ hne => _) fun hi => _).trans _
[GOAL]
case refine'_1
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i j : σ
x✝ : j ∈ s.support
hne : j ≠ i
⊢ (fun a_1 b => ↑(monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) j (↑s j) = 0
[PROOFSTEP]
simp [Pi.single_eq_of_ne hne]
[GOAL]
case refine'_2
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
hi : ¬i ∈ s.support
⊢ (fun a_1 b => ↑(monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (↑s i) = 0
[PROOFSTEP]
rw [Finsupp.not_mem_support_iff] at hi
[GOAL]
case refine'_2
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
hi : ↑s i = 0
⊢ (fun a_1 b => ↑(monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (↑s i) = 0
[PROOFSTEP]
simp [hi]
[GOAL]
case refine'_3
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (fun a_1 b => ↑(monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (↑s i) =
    ↑(monomial (s - single i 1)) (a * ↑(↑s i))
[PROOFSTEP]
simp
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i j : σ
⊢ ↑(pderiv i) (X j) = Pi.single i 1 j
[PROOFSTEP]
rw [pderiv_def, mkDerivation_X]
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ ↑(pderiv i) (X i) = 1
[PROOFSTEP]
classical simp
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ ↑(pderiv i) (X i) = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
⊢ ↑(pderiv i) (X j) = 0
[PROOFSTEP]
classical simp [h]
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
⊢ ↑(pderiv i) (X j) = 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
n : ℕ
⊢ ↑(pderiv i) (↑(monomial (single i n)) a) = ↑(monomial (single i (n - 1))) (a * ↑n)
[PROOFSTEP]
simp
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑(pderiv i) (f * g) = ↑(pderiv i) f * g + f * ↑(pderiv i) g
[PROOFSTEP]
simp only [(pderiv i).leibniz f g, smul_eq_mul, mul_comm, add_comm]
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : MvPolynomial σ R
i : σ
⊢ ↑(pderiv i) (↑C a * f) = ↑C a * ↑(pderiv i) f
[PROOFSTEP]
rw [C_mul', Derivation.map_smul, C_mul']


[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
⊢ (toMatrix f * M) i j = Option.casesOn (↑f i) 0 fun fi => M fi j
[PROOFSTEP]
dsimp [toMatrix, Matrix.mul_apply]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
⊢ (Finset.sum Finset.univ fun j_1 => (if j_1 ∈ ↑f i then 1 else 0) * M j_1 j) = Option.rec 0 (fun val => M val j) (↑f i)
[PROOFSTEP]
cases' h : f i with fi
[GOAL]
case none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
h : ↑f i = none
⊢ (Finset.sum Finset.univ fun j_1 => (if j_1 ∈ none then 1 else 0) * M j_1 j) = Option.rec 0 (fun val => M val j) none
[PROOFSTEP]
simp [h]
[GOAL]
case some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : ↑f i = some fi
⊢ (Finset.sum Finset.univ fun j_1 => (if j_1 ∈ some fi then 1 else 0) * M j_1 j) =
    Option.rec 0 (fun val => M val j) (some fi)
[PROOFSTEP]
rw [Finset.sum_eq_single fi]
[GOAL]
case some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : ↑f i = some fi
⊢ (if fi ∈ some fi then 1 else 0) * M fi j = Option.rec 0 (fun val => M val j) (some fi)
[PROOFSTEP]
simp (config := { contextual := true }) [h, eq_comm]
[GOAL]
case some.h₀
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : ↑f i = some fi
⊢ ∀ (b : m), b ∈ Finset.univ → b ≠ fi → (if b ∈ some fi then 1 else 0) * M b j = 0
[PROOFSTEP]
simp (config := { contextual := true }) [h, eq_comm]
[GOAL]
case some.h₁
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : ↑f i = some fi
⊢ ¬fi ∈ Finset.univ → (if fi ∈ some fi then 1 else 0) * M fi j = 0
[PROOFSTEP]
simp (config := { contextual := true }) [h, eq_comm]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
⊢ toMatrix (PEquiv.symm f) = (toMatrix f)ᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
x✝ : m
⊢ toMatrix (PEquiv.symm f) i✝ x✝ = (toMatrix f)ᵀ i✝ x✝
[PROOFSTEP]
simp only [transpose, mem_iff_mem f, toMatrix_apply]
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
x✝ : m
⊢ (if i✝ ∈ ↑f x✝ then 1 else 0) = ↑of (fun x y => if x ∈ ↑f y then 1 else 0) i✝ x✝
[PROOFSTEP]
congr
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
⊢ toMatrix (PEquiv.refl n) = 1
[PROOFSTEP]
ext
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i✝ x✝ : n
⊢ toMatrix (PEquiv.refl n) i✝ x✝ = OfNat.ofNat 1 i✝ x✝
[PROOFSTEP]
simp [toMatrix_apply, one_apply]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (M * toMatrix f) i j = Option.casesOn (↑(PEquiv.symm f) j) 0 fun fj => M i fj
[PROOFSTEP]
dsimp [toMatrix, Matrix.mul_apply]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) =
    Option.rec 0 (fun val => M i val) (↑(PEquiv.symm f) j)
[PROOFSTEP]
cases' h : f.symm j with fj
[GOAL]
case none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
h : ↑(PEquiv.symm f) j = none
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) none
[PROOFSTEP]
simp [h, ← f.eq_some_iff]
[GOAL]
case some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) =
    Option.rec 0 (fun val => M i val) (some fj)
[PROOFSTEP]
rw [Finset.sum_eq_single fj]
[GOAL]
case some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ (M i fj * if j ∈ ↑f fj then 1 else 0) = Option.rec 0 (fun val => M i val) (some fj)
[PROOFSTEP]
simp [h, ← f.eq_some_iff]
[GOAL]
case some.h₀
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ ∀ (b : m), b ∈ Finset.univ → b ≠ fj → (M i b * if j ∈ ↑f b then 1 else 0) = 0
[PROOFSTEP]
rintro b - n
[GOAL]
case some.h₀
k : Type u_1
l : Type u_2
m : Type u_3
n✝ : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n✝
M : Matrix l m α
f : m ≃. n✝
i : l
j : n✝
fj : m
h : ↑(PEquiv.symm f) j = some fj
b : m
n : b ≠ fj
⊢ (M i b * if j ∈ ↑f b then 1 else 0) = 0
[PROOFSTEP]
simp [h, ← f.eq_some_iff, n.symm]
[GOAL]
case some.h₁
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ ¬fj ∈ Finset.univ → (M i fj * if j ∈ ↑f fj then 1 else 0) = 0
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : m ≃ m
M : Matrix m n α
⊢ toMatrix (Equiv.toPEquiv f) * M = fun i => M (↑f i)
[PROOFSTEP]
ext i j
[GOAL]
case h.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : m ≃ m
M : Matrix m n α
i : m
j : n
⊢ (toMatrix (Equiv.toPEquiv f) * M) i j = M (↑f i) j
[PROOFSTEP]
rw [mul_matrix_apply, Equiv.toPEquiv_apply]
[GOAL]
k : Type u_1
l : Type u_2
m✝ : Type u_3
n✝ : Type u_4
α✝ : Type v
m : Type u_5
n : Type u_6
α : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : n ≃ n
M : Matrix m n α
i : m
j : n
⊢ (M * toMatrix (Equiv.toPEquiv f)) i j = submatrix M id (↑f.symm) i j
[PROOFSTEP]
rw [PEquiv.matrix_mul_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply, Matrix.submatrix_apply, id.def]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
⊢ toMatrix (PEquiv.trans f g) = toMatrix f * toMatrix g
[PROOFSTEP]
ext i j
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ toMatrix (PEquiv.trans f g) i j = (toMatrix f * toMatrix g) i j
[PROOFSTEP]
rw [mul_matrix_apply]
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ toMatrix (PEquiv.trans f g) i j = Option.casesOn (↑f i) 0 fun fi => toMatrix g fi j
[PROOFSTEP]
dsimp [toMatrix, PEquiv.trans]
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (if j ∈ Option.bind (↑f i) ↑g then 1 else 0) = Option.rec 0 (fun val => if j ∈ ↑g val then 1 else 0) (↑f i)
[PROOFSTEP]
cases f i
[GOAL]
case a.h.none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (if j ∈ Option.bind none ↑g then 1 else 0) = Option.rec 0 (fun val => if j ∈ ↑g val then 1 else 0) none
[PROOFSTEP]
simp
[GOAL]
case a.h.some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
val✝ : m
⊢ (if j ∈ Option.bind (some val✝) ↑g then 1 else 0) = Option.rec 0 (fun val => if j ∈ ↑g val then 1 else 0) (some val✝)
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
⊢ Function.Injective toMatrix
[PROOFSTEP]
classical
intro f g
refine' not_imp_not.1 _
simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]
intro i hi
use i
cases' hf : f i with fi
· cases' hg : g i with gi
  · rw [hf, hg] at hi
    exact (hi rfl).elim
  · use gi
    simp
· use fi
  simp [hf.symm, Ne.symm hi]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
⊢ Function.Injective toMatrix
[PROOFSTEP]
intro f g
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ toMatrix f = toMatrix g → f = g
[PROOFSTEP]
refine' not_imp_not.1 _
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ¬f = g → ¬toMatrix f = toMatrix g
[PROOFSTEP]
simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ∀ (x : m), ¬↑f x = ↑g x → ∃ x x_1, ¬(if x_1 ∈ ↑f x then 1 else 0) = if x_1 ∈ ↑g x then 1 else 0
[PROOFSTEP]
intro i hi
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
⊢ ∃ x x_1, ¬(if x_1 ∈ ↑f x then 1 else 0) = if x_1 ∈ ↑g x then 1 else 0
[PROOFSTEP]
use i
[GOAL]
case h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
⊢ ∃ x, ¬(if x ∈ ↑f i then 1 else 0) = if x ∈ ↑g i then 1 else 0
[PROOFSTEP]
cases' hf : f i with fi
[GOAL]
case h.none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ ↑g i then 1 else 0
[PROOFSTEP]
cases' hg : g i with gi
[GOAL]
case h.none.none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
hg : ↑g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0
[PROOFSTEP]
rw [hf, hg] at hi
[GOAL]
case h.none.none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬none = none
hf : ↑f i = none
hg : ↑g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0
[PROOFSTEP]
exact (hi rfl).elim
[GOAL]
case h.none.some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
gi : n
hg : ↑g i = some gi
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ some gi then 1 else 0
[PROOFSTEP]
use gi
[GOAL]
case h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
gi : n
hg : ↑g i = some gi
⊢ ¬(if gi ∈ none then 1 else 0) = if gi ∈ some gi then 1 else 0
[PROOFSTEP]
simp
[GOAL]
case h.some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
fi : n
hf : ↑f i = some fi
⊢ ∃ x, ¬(if x ∈ some fi then 1 else 0) = if x ∈ ↑g i then 1 else 0
[PROOFSTEP]
use fi
[GOAL]
case h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
fi : n
hf : ↑f i = some fi
⊢ ¬(if fi ∈ some fi then 1 else 0) = if fi ∈ ↑g i then 1 else 0
[PROOFSTEP]
simp [hf.symm, Ne.symm hi]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j : n
⊢ toMatrix (Equiv.toPEquiv (Equiv.swap i j)) =
    1 - toMatrix (single i i) - toMatrix (single j j) + toMatrix (single i j) + toMatrix (single j i)
[PROOFSTEP]
ext
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
⊢ toMatrix (Equiv.toPEquiv (Equiv.swap i j)) i✝ x✝ =
    (1 - toMatrix (single i i) - toMatrix (single j j) + toMatrix (single i j) + toMatrix (single j i)) i✝ x✝
[PROOFSTEP]
dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, one_apply]
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
⊢ (if x✝ ∈ some (if i✝ = i then j else if i✝ = j then i else i✝) then 1 else 0) =
    ((((if i✝ = x✝ then 1 else 0) - if x✝ ∈ if i✝ = i then some i else none then 1 else 0) -
          if x✝ ∈ if i✝ = j then some j else none then 1 else 0) +
        if x✝ ∈ if i✝ = i then some j else none then 1 else 0) +
      if x✝ ∈ if i✝ = j then some i else none then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : x✝ ∈ some j
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 1 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 1 = 1 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 1 = 1 - 1 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : x✝ ∈ some j
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 1 - 0 - 1 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 1 = 1 - 0 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 1 = 1 - 0 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : x✝ ∈ some j
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 0 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 1 = 0 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 1 = 0 - 1 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : x✝ ∈ some j
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 0 - 0 - 1 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 1 = 0 - 0 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 1 = 0 - 0 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : ¬x✝ ∈ some j
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 1 - 1 - 0 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 0 = 1 - 1 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 0 = 1 - 1 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : ¬x✝ ∈ some j
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 1 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 0 = 1 - 0 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 0 = 1 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : ¬x✝ ∈ some j
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 0 - 1 - 0 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 0 = 0 - 1 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 0 = 0 - 1 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : ¬x✝ ∈ some j
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 0 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 0 = 0 - 0 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 0 = 0 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 1 = 1 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 1 = 1 - 1 - 0 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 1 = 1 - 0 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 1 = 1 - 0 - 0 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 1 = 0 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 1 = 0 - 1 - 0 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 1 = 0 - 0 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 1 = 0 - 0 - 0 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 0 = 1 - 1 - 1 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 0 = 1 - 1 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 0 = 1 - 0 - 1 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 0 = 1 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 0 = 0 - 1 - 1 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 0 = 0 - 1 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 0 = 0 - 0 - 1 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 0 = 0 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : x✝ ∈ some i✝
h✝¹ : i✝ = x✝
h✝ : x✝ ∈ none
⊢ 1 = 1 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : x✝ ∈ some i✝
h✝¹ : i✝ = x✝
h✝ : ¬x✝ ∈ none
⊢ 1 = 1 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : x✝ ∈ some i✝
h✝¹ : ¬i✝ = x✝
h✝ : x✝ ∈ none
⊢ 1 = 0 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : x✝ ∈ some i✝
h✝¹ : ¬i✝ = x✝
h✝ : ¬x✝ ∈ none
⊢ 1 = 0 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : ¬x✝ ∈ some i✝
h✝¹ : i✝ = x✝
h✝ : x✝ ∈ none
⊢ 0 = 1 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : ¬x✝ ∈ some i✝
h✝¹ : i✝ = x✝
h✝ : ¬x✝ ∈ none
⊢ 0 = 1 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : ¬x✝ ∈ some i✝
h✝¹ : ¬i✝ = x✝
h✝ : x✝ ∈ none
⊢ 0 = 0 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : ¬x✝ ∈ some i✝
h✝¹ : ¬i✝ = x✝
h✝ : ¬x✝ ∈ none
⊢ 0 = 0 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq k
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
a : m
b : n
c : k
⊢ toMatrix (single a b) * toMatrix (single b c) = toMatrix (single a c)
[PROOFSTEP]
rw [← toMatrix_trans, single_trans_single]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : Semiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
⊢ toMatrix (single a b₁) * toMatrix (single b₂ c) = 0
[PROOFSTEP]
rw [← toMatrix_trans, single_trans_single_of_ne hb, toMatrix_bot]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : Fintype k
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : Semiring α
a : m
b : n
c : k
M : Matrix k l α
⊢ toMatrix (single a b) * (toMatrix (single b c) * M) = toMatrix (single a c) * M
[PROOFSTEP]
rw [← Matrix.mul_assoc, single_mul_single]


[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
x : α
⊢ x ∈ (fun a => f (↑E.symm a)) ((fun x => ↑E (T x)) x)
[PROOFSTEP]
simpa using h₁ x
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ (fun a => f (↑E.symm a)) a ∩ (fun a => f (↑E.symm a)) b
⊢ x ∈ (fun a => f (↑E.symm a)) ((fun a b x h => ↑E (I (↑E.symm a) (↑E.symm b) x h)) a b x h)
[PROOFSTEP]
simpa using h₂ (E.symm a) (E.symm b) x h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ (fun a => f (↑E.symm a)) a ∩ (fun a => f (↑E.symm a)) b
⊢ (fun a => f (↑E.symm a)) ((fun a b x h => ↑E (I (↑E.symm a) (↑E.symm b) x h)) a b x h) ⊆
    (fun a => f (↑E.symm a)) a ∩ (fun a => f (↑E.symm a)) b
[PROOFSTEP]
simpa using h₃ (E.symm a) (E.symm b) x h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F✝ : Ctop α σ
E : σ ≃ τ
F : Ctop α σ
a : τ
⊢ f (ofEquiv E F) a = f F (↑E.symm a)
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
a : τ
f✝ : σ → Set α
top✝ : α → σ
top_mem✝ : ∀ (x : α), x ∈ f✝ (top✝ x)
inter✝ : (a b : σ) → (x : α) → x ∈ f✝ a ∩ f✝ b → σ
inter_mem✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), x ∈ f✝ (inter✝ a b x h)
inter_sub✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), f✝ (inter✝ a b x h) ⊆ f✝ a ∩ f✝ b
⊢ f
      (ofEquiv E
        { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝,
          inter_sub := inter_sub✝ })
      a =
    f { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝, inter_sub := inter_sub✝ }
      (↑E.symm a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
T : TopologicalSpace α
F : Realizer α
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
[PROOFSTEP]
have := toTopsp_isTopologicalBasis F.F
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
T : TopologicalSpace α
F : Realizer α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
[PROOFSTEP]
rwa [F.eq] at this
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
[PROOFSTEP]
have := @mem_nhds_toTopsp _ _ F.F s a
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
[PROOFSTEP]
rwa [F.eq] at this
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ (¬a ∈ s → ∃ b, a ∈ f F.F b ∧ ∀ (z : α), z ∈ f F.F b → ¬z ∈ s) ↔
    (∀ (b : F.σ), a ∈ f F.F b → ∃ z, z ∈ f F.F b ∩ s) → a ∈ s
[PROOFSTEP]
haveI := Classical.propDecidable
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬a ∈ s → ∃ b, a ∈ f F.F b ∧ ∀ (z : α), z ∈ f F.F b → ¬z ∈ s) ↔
    (∀ (b : F.σ), a ∈ f F.F b → ∃ z, z ∈ f F.F b ∩ s) → a ∈ s
[PROOFSTEP]
rw [not_imp_comm]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬∃ b, a ∈ f F.F b ∧ ∀ (z : α), z ∈ f F.F b → ¬z ∈ s) → a ∈ s ↔
    (∀ (b : F.σ), a ∈ f F.F b → ∃ z, z ∈ f F.F b ∩ s) → a ∈ s
[PROOFSTEP]
simp [not_exists, not_and, not_forall, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
s : F.σ
a : α
m : a ∈ f F.F s
⊢ 𝓝 a ≤ 𝓟 (f F.F s)
[PROOFSTEP]
simpa using F.mem_nhds.2 ⟨s, m, Subset.refl _⟩
[GOAL]
α : Type u_1
β : Type u_2
σ✝ : Type u_3
τ : Type u_4
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
⊢ toTopsp F = T
[PROOFSTEP]
refine' eq_of_nhds_eq_nhds fun x ↦ _
[GOAL]
α : Type u_1
β : Type u_2
σ✝ : Type u_3
τ : Type u_4
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
x : α
⊢ 𝓝 x = 𝓝 x
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
β : Type u_2
σ✝ : Type u_3
τ : Type u_4
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x
[PROOFSTEP]
rw [mem_nhds_toTopsp, H]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s✝ : Set α
x✝ : ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s✝
s : F.σ
h : a ∈ f F.F s ∧ f F.F s ⊆ s✝
⊢ a ∈ f (Ctop.ofEquiv E F.F) (↑E s) ∧ f (Ctop.ofEquiv E F.F) (↑E s) ⊆ s✝
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s : Set α
x✝ : ∃ b, a ∈ f (Ctop.ofEquiv E F.F) b ∧ f (Ctop.ofEquiv E F.F) b ⊆ s
t : τ
h : a ∈ f (Ctop.ofEquiv E F.F) t ∧ f (Ctop.ofEquiv E F.F) t ⊆ s
⊢ a ∈ f F.F (↑E.symm t) ∧ f F.F (↑E.symm t) ⊆ s
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ f (ofEquiv F E).F s = f F.F (↑E.symm s)
[PROOFSTEP]
delta ofEquiv
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ f { σ := τ, F := Ctop.ofEquiv E F.F, eq := (_ : toTopsp (Ctop.ofEquiv E F.F) = inst✝) }.F s = f F.F (↑E.symm s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : Filter.Realizer f
x : F.σ
h : f ≠ ⊥
hF : CFilter.f F.F x ⊆ ∅
⊢ { a // a ∈ ∅ ∧ 𝓝 a ⊓ f ≠ ⊥ }
[PROOFSTEP]
suffices : f = ⊥
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : Filter.Realizer f
x : F.σ
h : f ≠ ⊥
hF : CFilter.f F.F x ⊆ ∅
this : f = ⊥
⊢ { a // a ∈ ∅ ∧ 𝓝 a ⊓ f ≠ ⊥ }
case this
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : Filter.Realizer f
x : F.σ
h : f ≠ ⊥
hF : CFilter.f F.F x ⊆ ∅
⊢ f = ⊥
[PROOFSTEP]
exact absurd this h
[GOAL]
case this
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : Filter.Realizer f
x : F.σ
h : f ≠ ⊥
hF : CFilter.f F.F x ⊆ ∅
⊢ f = ⊥
[PROOFSTEP]
rw [← F.eq, eq_bot_iff]
[GOAL]
case this
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : Filter.Realizer f
x : F.σ
h : f ≠ ⊥
hF : CFilter.f F.F x ⊆ ∅
⊢ CFilter.toFilter F.F ≤ ⊥
[PROOFSTEP]
exact λ s _ ↦ ⟨x, hF.trans s.empty_subset⟩


[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s' s : σ →₀ ℕ
x : MvPolynomial σ R
h : ¬s ≤ s'
⊢ ¬∃ d, s' = s + d
[PROOFSTEP]
rintro ⟨d, rfl⟩
[GOAL]
case intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
h : ¬s ≤ s + d
⊢ False
[PROOFSTEP]
exact h le_self_add
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ ↑(monomial i) r ∣ ↑(monomial j) s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
constructor
[GOAL]
case mp
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ ↑(monomial i) r ∣ ↑(monomial j) s → (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ↑(monomial j) s = ↑(monomial i) r * x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
rw [MvPolynomial.ext_iff] at hx
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
have hj := hx j
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hj : coeff j (↑(monomial j) s) = coeff j (↑(monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
have hi := hx i
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hj : coeff j (↑(monomial j) s) = coeff j (↑(monomial i) r * x)
hi : coeff i (↑(monomial j) s) = coeff i (↑(monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
classical
simp_rw [coeff_monomial, if_pos] at hj hi
simp_rw [coeff_monomial_mul'] at hi hj
split_ifs at hi hj  with hi hi
· exact ⟨Or.inr hi, _, hj⟩
·
  exact
    ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩
      -- Porting note: two goals remain at this point in Lean 4
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hj : coeff j (↑(monomial j) s) = coeff j (↑(monomial i) r * x)
hi : coeff i (↑(monomial j) s) = coeff i (↑(monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
simp_rw [coeff_monomial, if_pos] at hj hi
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi : (if j = i then s else 0) = coeff i (↑(monomial i) r * x)
hj : s = coeff j (↑(monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
simp_rw [coeff_monomial_mul'] at hi hj
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hj : s = if i ≤ j then r * coeff (j - i) x else 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
split_ifs at hi hj  with hi hi
[GOAL]
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi✝¹ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi✝ : j = i
hi : i ≤ j
hj : s = r * coeff (j - i) x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
exact ⟨Or.inr hi, _, hj⟩
[GOAL]
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi✝¹ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi✝ : j = i
hi : ¬i ≤ j
hj : s = 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
exact
  ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩
    -- Porting note: two goals remain at this point in Lean 4
[GOAL]
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi✝ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : ¬j = i
h✝ : i ≤ j
hj : s = r * coeff (j - i) x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
simp_all only [or_true, dvd_mul_right]
[GOAL]
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi✝ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : ¬j = i
h✝ : ¬i ≤ j
hj : s = 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
simp_all only [ite_self, le_refl, ite_true, dvd_mul_right]
[GOAL]
case mpr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s → ↑(monomial i) r ∣ ↑(monomial j) s
[PROOFSTEP]
rintro ⟨h | hij, d, rfl⟩
[GOAL]
case mpr.intro.inl.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
i j : σ →₀ ℕ
d : R
h : r * d = 0
⊢ ↑(monomial i) r ∣ ↑(monomial j) (r * d)
[PROOFSTEP]
simp_rw [h, monomial_zero, dvd_zero]
[GOAL]
case mpr.intro.inr.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
⊢ ↑(monomial i) r ∣ ↑(monomial j) (r * d)
[PROOFSTEP]
refine' ⟨monomial (j - i) d, _⟩
[GOAL]
case mpr.intro.inr.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
⊢ ↑(monomial j) (r * d) = ↑(monomial i) r * ↑(monomial (j - i)) d
[PROOFSTEP]
rw [monomial_mul, add_tsub_cancel_of_le hij]
[GOAL]
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ ↑(monomial i) 1 ∣ ↑(monomial j) 1 ↔ i ≤ j
[PROOFSTEP]
rw [monomial_dvd_monomial]
[GOAL]
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ (1 = 0 ∨ i ≤ j) ∧ 1 ∣ 1 ↔ i ≤ j
[PROOFSTEP]
simp_rw [one_ne_zero, false_or_iff, dvd_rfl, and_true_iff]
[GOAL]
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ X i ∣ X j ↔ i = j
[PROOFSTEP]
refine' monomial_one_dvd_monomial_one.trans _
[GOAL]
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ Finsupp.single i 1 ≤ Finsupp.single j 1 ↔ i = j
[PROOFSTEP]
simp_rw [Finsupp.single_le_iff, Nat.one_le_iff_ne_zero, Finsupp.single_apply_ne_zero, and_true_iff]
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ X i ∣ ↑(monomial j) r ↔ r = 0 ∨ ↑j i ≠ 0
[PROOFSTEP]
refine' monomial_dvd_monomial.trans _
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ ↑j i ≠ 0
[PROOFSTEP]
simp_rw [one_dvd, and_true_iff, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]


[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = x
[PROOFSTEP]
funext i
[GOAL]
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
i : σ
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x i = x i
[PROOFSTEP]
simp only [comap, AlgHom.id_apply, id.def, aeval_X]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) = id
[PROOFSTEP]
funext x
[GOAL]
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = id x
[PROOFSTEP]
exact comap_id_apply x
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (AlgHom.comp g f) x = comap f (comap g x)
[PROOFSTEP]
funext i
[GOAL]
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (AlgHom.comp g f) x i = comap f (comap g x) i
[PROOFSTEP]
trans aeval x (aeval (fun i => g (X i)) (f (X i)))
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (AlgHom.comp g f) x i = ↑(aeval x) (↑(aeval fun i => ↑g (X i)) (↑f (X i)))
[PROOFSTEP]
apply eval₂Hom_congr rfl rfl
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(AlgHom.comp g f) (X i) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
[PROOFSTEP]
rw [AlgHom.comp_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑g (↑f (X i)) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
[PROOFSTEP]
suffices g = aeval fun i => g (X i) by rw [← this]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
this : g = aeval fun i => ↑g (X i)
⊢ ↑g (↑f (X i)) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
[PROOFSTEP]
rw [← this]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ g = aeval fun i => ↑g (X i)
[PROOFSTEP]
exact aeval_unique g
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(aeval x) (↑(aeval fun i => ↑g (X i)) (↑f (X i))) = comap f (comap g x) i
[PROOFSTEP]
simp only [comap, aeval_eq_eval₂Hom, map_eval₂Hom, AlgHom.comp_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(eval₂Hom (RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R))) fun i =>
          ↑(eval₂Hom (algebraMap R R) x) (↑g (X i)))
      (↑f (X i)) =
    ↑(eval₂Hom (algebraMap R R) fun i => ↑(eval₂Hom (algebraMap R R) x) (↑g (X i))) (↑f (X i))
[PROOFSTEP]
refine' eval₂Hom_congr _ rfl rfl
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)) = algebraMap R R
[PROOFSTEP]
ext r
[GOAL]
case a
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
r : R
⊢ ↑(RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R))) r = ↑(algebraMap R R) r
[PROOFSTEP]
apply aeval_C
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
⊢ comap (AlgHom.comp g f) = comap f ∘ comap g
[PROOFSTEP]
funext x
[GOAL]
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (AlgHom.comp g f) x = (comap f ∘ comap g) x
[PROOFSTEP]
exact comap_comp_apply _ _ _
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
⊢ comap f x = x
[PROOFSTEP]
convert comap_id_apply x
[GOAL]
case h.e'_2.h.e'_5
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
⊢ f = AlgHom.id R (MvPolynomial σ R)
[PROOFSTEP]
ext1 φ
[GOAL]
case h.e'_2.h.e'_5.hf
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
φ : σ
⊢ ↑f (X φ) = ↑(AlgHom.id R (MvPolynomial σ R)) (X φ)
[PROOFSTEP]
simp [hf, AlgHom.id_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
x : τ → R
⊢ comap (rename f) x = x ∘ f
[PROOFSTEP]
funext
[GOAL]
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
x : τ → R
x✝ : σ
⊢ comap (rename f) x x✝ = (x ∘ f) x✝
[PROOFSTEP]
simp [rename_X, comap_apply, aeval_X]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
⊢ Function.LeftInverse (comap ↑(AlgEquiv.symm f)) (comap ↑f)
[PROOFSTEP]
intro x
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
⊢ comap (↑(AlgEquiv.symm f)) (comap (↑f) x) = x
[PROOFSTEP]
rw [← comap_comp_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
⊢ comap (AlgHom.comp ↑f ↑(AlgEquiv.symm f)) x = x
[PROOFSTEP]
apply comap_eq_id_of_eq_id
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
⊢ ∀ (φ : MvPolynomial τ R), ↑(AlgHom.comp ↑f ↑(AlgEquiv.symm f)) φ = φ
[PROOFSTEP]
intro
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
φ✝ : MvPolynomial τ R
⊢ ↑(AlgHom.comp ↑f ↑(AlgEquiv.symm f)) φ✝ = φ✝
[PROOFSTEP]
simp only [AlgHom.id_apply, AlgEquiv.comp_symm]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
⊢ Function.RightInverse (comap ↑(AlgEquiv.symm f)) (comap ↑f)
[PROOFSTEP]
intro x
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
⊢ comap (↑f) (comap (↑(AlgEquiv.symm f)) x) = x
[PROOFSTEP]
rw [← comap_comp_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
⊢ comap (AlgHom.comp ↑(AlgEquiv.symm f) ↑f) x = x
[PROOFSTEP]
apply comap_eq_id_of_eq_id
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
⊢ ∀ (φ : MvPolynomial σ R), ↑(AlgHom.comp ↑(AlgEquiv.symm f) ↑f) φ = φ
[PROOFSTEP]
intro
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
φ✝ : MvPolynomial σ R
⊢ ↑(AlgHom.comp ↑(AlgEquiv.symm f) ↑f) φ✝ = φ✝
[PROOFSTEP]
simp only [AlgHom.id_apply, AlgEquiv.symm_comp]