[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
⊢ ↑(map f) (↑(rename g) p) = ↑(rename g) (↑(map f) p)
[PROOFSTEP]
apply
  MvPolynomial.induction_on p (fun a => by simp only [map_C, rename_C])
    (fun p q hp hq => by simp only [hp, hq, AlgHom.map_add, RingHom.map_add]) fun p n hp => by
    simp only [hp, rename_X, map_X, RingHom.map_mul, AlgHom.map_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
a : R
⊢ ↑(map f) (↑(rename g) (↑C a)) = ↑(rename g) (↑(map f) (↑C a))
[PROOFSTEP]
simp only [map_C, rename_C]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p q : MvPolynomial σ R
hp : ↑(map f) (↑(rename g) p) = ↑(rename g) (↑(map f) p)
hq : ↑(map f) (↑(rename g) q) = ↑(rename g) (↑(map f) q)
⊢ ↑(map f) (↑(rename g) (p + q)) = ↑(rename g) (↑(map f) (p + q))
[PROOFSTEP]
simp only [hp, hq, AlgHom.map_add, RingHom.map_add]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p : MvPolynomial σ R
n : σ
hp : ↑(map f) (↑(rename g) p) = ↑(rename g) (↑(map f) p)
⊢ ↑(map f) (↑(rename g) (p * X n)) = ↑(rename g) (↑(map f) (p * X n))
[PROOFSTEP]
simp only [hp, rename_X, map_X, RingHom.map_mul, AlgHom.map_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ ↑(rename g) (eval₂ C (X ∘ f) p) = ↑(rename (g ∘ f)) p
[PROOFSTEP]
simp only [rename, aeval_eq_eval₂Hom]
  -- porting note: the Lean 3 proof of this was very fragile and included a nonterminal `simp`.
      -- Hopefully this is less prone to breaking
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) (eval₂ C (X ∘ f) p) =
    ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p
[PROOFSTEP]
rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C (X ∘ f) p]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C)
      (↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) ∘ X ∘ f) p =
    ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p
[PROOFSTEP]
simp only [(· ∘ ·), eval₂Hom_X', coe_eval₂Hom]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C) (fun x => X (g (f x))) p =
    eval₂ (algebraMap R (MvPolynomial α R)) (fun x => X (g (f x))) p
[PROOFSTEP]
refine' eval₂Hom_congr _ rfl rfl
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C = algebraMap R (MvPolynomial α R)
[PROOFSTEP]
ext1
[GOAL]
case a
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
x✝ : R
⊢ ↑(RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C) x✝ =
    ↑(algebraMap R (MvPolynomial α R)) x✝
[PROOFSTEP]
simp only [comp_apply, RingHom.coe_comp, eval₂Hom_C]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ↑(rename f) (↑(monomial d) r) = ↑(monomial (Finsupp.mapDomain f d)) r
[PROOFSTEP]
rw [rename, aeval_monomial, monomial_eq (s := Finsupp.mapDomain f d), Finsupp.prod_mapDomain_index]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ (↑(algebraMap R (MvPolynomial τ R)) r * Finsupp.prod d fun i k => (X ∘ f) i ^ k) =
    ↑C r * Finsupp.prod d fun a m => X (f a) ^ m
[PROOFSTEP]
rfl
[GOAL]
case h_zero
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ), X b ^ 0 = 1
[PROOFSTEP]
exact fun n => pow_zero _
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ) (m₁ m₂ : ℕ), X b ^ (m₁ + m₂) = X b ^ m₁ * X b ^ m₂
[PROOFSTEP]
exact fun n i₁ i₂ => pow_add _ _ _
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : MvPolynomial σ R
⊢ ↑(rename f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
[PROOFSTEP]
simp only [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply, X_pow_eq_monomial, ←
  monomial_finsupp_sum_index]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : MvPolynomial σ R
⊢ (sum p fun s a => ↑(monomial (sum s fun a b => Finsupp.single (f a) b)) a) =
    sum p fun a => Finsupp.single (sum a fun a => Finsupp.single (f a))
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
⊢ Injective ↑(rename f)
[PROOFSTEP]
have : (rename f : MvPolynomial σ R → MvPolynomial τ R) = Finsupp.mapDomain (Finsupp.mapDomain f) :=
  funext (rename_eq f)
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
this : ↑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective ↑(rename f)
[PROOFSTEP]
rw [this]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
this : ↑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective (Finsupp.mapDomain (Finsupp.mapDomain f))
[PROOFSTEP]
exact Finsupp.mapDomain_injective (Finsupp.mapDomain_injective hf)
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
i : σ
⊢ ↑(AlgHom.comp (killCompl hf) (rename f)) (X i) = ↑(AlgHom.id R (MvPolynomial σ R)) (X i)
[PROOFSTEP]
dsimp
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
i : σ
⊢ ↑(killCompl hf) (↑(rename f) (X i)) = X i
[PROOFSTEP]
rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos, Equiv.ofInjective_symm_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
src✝ : MvPolynomial σ R →ₐ[R] MvPolynomial τ R := rename ↑f
p : MvPolynomial σ R
⊢ ↑(rename ↑f.symm) (↑(rename ↑f) p) = p
[PROOFSTEP]
rw [rename_rename, f.symm_comp_self, rename_id]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
src✝ : MvPolynomial σ R →ₐ[R] MvPolynomial τ R := rename ↑f
p : MvPolynomial τ R
⊢ ↑(rename ↑f) (↑(rename ↑f.symm) p) = p
[PROOFSTEP]
rw [rename_rename, f.self_comp_symm, rename_id]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ eval₂ f g (↑(rename k) p) = eval₂ f (g ∘ k) p
[PROOFSTEP]
apply MvPolynomial.induction_on p
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (a : R), eval₂ f g (↑(rename k) (↑C a)) = eval₂ f (g ∘ k) (↑C a)
[PROOFSTEP]
intros
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
a✝ : R
⊢ eval₂ f g (↑(rename k) (↑C a✝)) = eval₂ f (g ∘ k) (↑C a✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    eval₂ f g (↑(rename k) p) = eval₂ f (g ∘ k) p →
      eval₂ f g (↑(rename k) q) = eval₂ f (g ∘ k) q → eval₂ f g (↑(rename k) (p + q)) = eval₂ f (g ∘ k) (p + q)
[PROOFSTEP]
intros
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p p✝ q✝ : MvPolynomial σ R
a✝¹ : eval₂ f g (↑(rename k) p✝) = eval₂ f (g ∘ k) p✝
a✝ : eval₂ f g (↑(rename k) q✝) = eval₂ f (g ∘ k) q✝
⊢ eval₂ f g (↑(rename k) (p✝ + q✝)) = eval₂ f (g ∘ k) (p✝ + q✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂ f g (↑(rename k) p) = eval₂ f (g ∘ k) p → eval₂ f g (↑(rename k) (p * X n)) = eval₂ f (g ∘ k) (p * X n)
[PROOFSTEP]
intros
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p p✝ : MvPolynomial σ R
n✝ : σ
a✝ : eval₂ f g (↑(rename k) p✝) = eval₂ f (g ∘ k) p✝
⊢ eval₂ f g (↑(rename k) (p✝ * X n✝)) = eval₂ f (g ∘ k) (p✝ * X n✝)
[PROOFSTEP]
simp [*]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ↑(rename k) (eval₂ C (g ∘ k) p) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p)
[PROOFSTEP]
apply MvPolynomial.induction_on p
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (a : R), ↑(rename k) (eval₂ C (g ∘ k) (↑C a)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (↑C a))
[PROOFSTEP]
intros
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
a✝ : R
⊢ ↑(rename k) (eval₂ C (g ∘ k) (↑C a✝)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (↑C a✝))
[PROOFSTEP]
simp [*]
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    ↑(rename k) (eval₂ C (g ∘ k) p) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p) →
      ↑(rename k) (eval₂ C (g ∘ k) q) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) q) →
        ↑(rename k) (eval₂ C (g ∘ k) (p + q)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p + q))
[PROOFSTEP]
intros
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p✝ q✝ : MvPolynomial σ R
a✝¹ : ↑(rename k) (eval₂ C (g ∘ k) p✝) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p✝)
a✝ : ↑(rename k) (eval₂ C (g ∘ k) q✝) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) q✝)
⊢ ↑(rename k) (eval₂ C (g ∘ k) (p✝ + q✝)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p✝ + q✝))
[PROOFSTEP]
simp [*]
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    ↑(rename k) (eval₂ C (g ∘ k) p) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p) →
      ↑(rename k) (eval₂ C (g ∘ k) (p * X n)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p * X n))
[PROOFSTEP]
intros
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : ↑(rename k) (eval₂ C (g ∘ k) p✝) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p✝)
⊢ ↑(rename k) (eval₂ C (g ∘ k) (p✝ * X n✝)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p✝ * X n✝))
[PROOFSTEP]
simp [*]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ↑(rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) p
[PROOFSTEP]
apply MvPolynomial.induction_on p
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (a : R), ↑(rename (Prod.mk j)) (eval₂ C g (↑C a)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (↑C a)
[PROOFSTEP]
intros
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
a✝ : R
⊢ ↑(rename (Prod.mk j)) (eval₂ C g (↑C a✝)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (↑C a✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    ↑(rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) p →
      ↑(rename (Prod.mk j)) (eval₂ C g q) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) q →
        ↑(rename (Prod.mk j)) (eval₂ C g (p + q)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (p + q)
[PROOFSTEP]
intros
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
p✝ q✝ : MvPolynomial σ R
a✝¹ : ↑(rename (Prod.mk j)) (eval₂ C g p✝) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) p✝
a✝ : ↑(rename (Prod.mk j)) (eval₂ C g q✝) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) q✝
⊢ ↑(rename (Prod.mk j)) (eval₂ C g (p✝ + q✝)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (p✝ + q✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    ↑(rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) p →
      ↑(rename (Prod.mk j)) (eval₂ C g (p * X n)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (p * X n)
[PROOFSTEP]
intros
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : ↑(rename (Prod.mk j)) (eval₂ C g p✝) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) p✝
⊢ ↑(rename (Prod.mk j)) (eval₂ C g (p✝ * X n✝)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (p✝ * X n✝)
[PROOFSTEP]
simp [*]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝ : MvPolynomial σ R
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ eval₂ f g (↑(rename (Prod.mk i)) p) = eval₂ f (fun j => g (i, j)) p
[PROOFSTEP]
apply MvPolynomial.induction_on p
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝ : MvPolynomial σ R
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (a : R), eval₂ f g (↑(rename (Prod.mk i)) (↑C a)) = eval₂ f (fun j => g (i, j)) (↑C a)
[PROOFSTEP]
intros
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝ : MvPolynomial σ R
g : σ × τ → S
i : σ
p : MvPolynomial τ R
a✝ : R
⊢ eval₂ f g (↑(rename (Prod.mk i)) (↑C a✝)) = eval₂ f (fun j => g (i, j)) (↑C a✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝ : MvPolynomial σ R
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p q : MvPolynomial τ R),
    eval₂ f g (↑(rename (Prod.mk i)) p) = eval₂ f (fun j => g (i, j)) p →
      eval₂ f g (↑(rename (Prod.mk i)) q) = eval₂ f (fun j => g (i, j)) q →
        eval₂ f g (↑(rename (Prod.mk i)) (p + q)) = eval₂ f (fun j => g (i, j)) (p + q)
[PROOFSTEP]
intros
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝¹ : MvPolynomial σ R
g : σ × τ → S
i : σ
p p✝ q✝ : MvPolynomial τ R
a✝¹ : eval₂ f g (↑(rename (Prod.mk i)) p✝) = eval₂ f (fun j => g (i, j)) p✝
a✝ : eval₂ f g (↑(rename (Prod.mk i)) q✝) = eval₂ f (fun j => g (i, j)) q✝
⊢ eval₂ f g (↑(rename (Prod.mk i)) (p✝ + q✝)) = eval₂ f (fun j => g (i, j)) (p✝ + q✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝ : MvPolynomial σ R
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p : MvPolynomial τ R) (n : τ),
    eval₂ f g (↑(rename (Prod.mk i)) p) = eval₂ f (fun j => g (i, j)) p →
      eval₂ f g (↑(rename (Prod.mk i)) (p * X n)) = eval₂ f (fun j => g (i, j)) (p * X n)
[PROOFSTEP]
intros
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝¹ : MvPolynomial σ R
g : σ × τ → S
i : σ
p p✝ : MvPolynomial τ R
n✝ : τ
a✝ : eval₂ f g (↑(rename (Prod.mk i)) p✝) = eval₂ f (fun j => g (i, j)) p✝
⊢ eval₂ f g (↑(rename (Prod.mk i)) (p✝ * X n✝)) = eval₂ f (fun j => g (i, j)) (p✝ * X n✝)
[PROOFSTEP]
simp [*]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∃ s q, p = ↑(rename Subtype.val) q
[PROOFSTEP]
classical
apply induction_on p
· intro r
  exact ⟨∅, C r, by rw [rename_C]⟩
· rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
  refine' ⟨s ∪ t, ⟨_, _⟩⟩
  ·
    refine' rename (Subtype.map id _) p + rename (Subtype.map id _) q <;>
      simp (config := { contextual := true }) only [id.def, true_or_iff, or_true_iff, Finset.mem_union, forall_true_iff]
  · simp only [rename_rename, AlgHom.map_add]
    rfl
· rintro p n ⟨s, p, rfl⟩
  refine' ⟨insert n s, ⟨_, _⟩⟩
  · refine' rename (Subtype.map id _) p * X ⟨n, s.mem_insert_self n⟩
    simp (config := { contextual := true }) only [id.def, or_true_iff, Finset.mem_insert, forall_true_iff]
  · simp only [rename_rename, rename_X, Subtype.coe_mk, AlgHom.map_mul]
    rfl
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∃ s q, p = ↑(rename Subtype.val) q
[PROOFSTEP]
apply induction_on p
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (a : R), ∃ s q, ↑C a = ↑(rename Subtype.val) q
[PROOFSTEP]
intro r
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
r : R
⊢ ∃ s q, ↑C r = ↑(rename Subtype.val) q
[PROOFSTEP]
exact ⟨∅, C r, by rw [rename_C]⟩
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
r : R
⊢ ↑C r = ↑(rename Subtype.val) (↑C r)
[PROOFSTEP]
rw [rename_C]
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = ↑(rename Subtype.val) q) →
      (∃ s q_1, q = ↑(rename Subtype.val) q_1) → ∃ s q_1, p + q = ↑(rename Subtype.val) q_1
[PROOFSTEP]
rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
[GOAL]
case h_add.intro.intro.intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ∃ s_1 q_1, ↑(rename Subtype.val) p + ↑(rename Subtype.val) q = ↑(rename Subtype.val) q_1
[PROOFSTEP]
refine' ⟨s ∪ t, ⟨_, _⟩⟩
[GOAL]
case h_add.intro.intro.intro.intro.refine'_1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ MvPolynomial { x // x ∈ s ∪ t } R
[PROOFSTEP]
refine' rename (Subtype.map id _) p + rename (Subtype.map id _) q
[GOAL]
case h_add.intro.intro.intro.intro.refine'_1.refine'_1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ∀ (a : σ), a ∈ s → id a ∈ s ∪ t
[PROOFSTEP]
simp (config := { contextual := true }) only [id.def, true_or_iff, or_true_iff, Finset.mem_union, forall_true_iff]
[GOAL]
case h_add.intro.intro.intro.intro.refine'_1.refine'_2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ∀ (a : σ), a ∈ t → id a ∈ s ∪ t
[PROOFSTEP]
simp (config := { contextual := true }) only [id.def, true_or_iff, or_true_iff, Finset.mem_union, forall_true_iff]
[GOAL]
case h_add.intro.intro.intro.intro.refine'_2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ↑(rename Subtype.val) p + ↑(rename Subtype.val) q =
    ↑(rename Subtype.val)
      (↑(rename (Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ s ∪ t))) p +
        ↑(rename (Subtype.map id (_ : ∀ (a : σ), a ∈ t → a ∈ s ∪ t))) q)
[PROOFSTEP]
simp only [rename_rename, AlgHom.map_add]
[GOAL]
case h_add.intro.intro.intro.intro.refine'_2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ↑(rename Subtype.val) p + ↑(rename Subtype.val) q =
    ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ s ∪ t))) p +
      ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ t → a ∈ s ∪ t))) q
[PROOFSTEP]
rfl
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = ↑(rename Subtype.val) q) → ∃ s q, p * X n = ↑(rename Subtype.val) q
[PROOFSTEP]
rintro p n ⟨s, p, rfl⟩
[GOAL]
case h_X.intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∃ s_1 q, ↑(rename Subtype.val) p * X n = ↑(rename Subtype.val) q
[PROOFSTEP]
refine' ⟨insert n s, ⟨_, _⟩⟩
[GOAL]
case h_X.intro.intro.refine'_1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ MvPolynomial { x // x ∈ insert n s } R
[PROOFSTEP]
refine' rename (Subtype.map id _) p * X ⟨n, s.mem_insert_self n⟩
[GOAL]
case h_X.intro.intro.refine'_1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∀ (a : σ), a ∈ s → id a ∈ insert n s
[PROOFSTEP]
simp (config := { contextual := true }) only [id.def, or_true_iff, Finset.mem_insert, forall_true_iff]
[GOAL]
case h_X.intro.intro.refine'_2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(rename Subtype.val) p * X n =
    ↑(rename Subtype.val)
      (↑(rename (Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ insert n s))) p *
        X { val := n, property := (_ : n ∈ insert n s) })
[PROOFSTEP]
simp only [rename_rename, rename_X, Subtype.coe_mk, AlgHom.map_mul]
[GOAL]
case h_X.intro.intro.refine'_2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(rename Subtype.val) p * X n =
    ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ insert n s))) p * X n
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p₁ p₂ : MvPolynomial σ R
⊢ ∃ s q₁ q₂, p₁ = ↑(rename Subtype.val) q₁ ∧ p₂ = ↑(rename Subtype.val) q₂
[PROOFSTEP]
obtain ⟨s₁, q₁, rfl⟩ := exists_finset_rename p₁
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p₂ : MvPolynomial σ R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
⊢ ∃ s q₁_1 q₂, ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) q₁_1 ∧ p₂ = ↑(rename Subtype.val) q₂
[PROOFSTEP]
obtain ⟨s₂, q₂, rfl⟩ := exists_finset_rename p₂
[GOAL]
case intro.intro.intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ s q₁_1 q₂_1,
    ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) q₁_1 ∧ ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) q₂_1
[PROOFSTEP]
classical
use s₁ ∪ s₂
use rename (Set.inclusion <| s₁.subset_union_left s₂) q₁
use rename (Set.inclusion <| s₁.subset_union_right s₂) q₂
constructor
  -- porting note: was `<;> simp <;> rfl` but Lean couldn't infer the arguments
· rw [rename_rename (Set.inclusion <| s₁.subset_union_left s₂)]
  rfl
· rw [rename_rename (Set.inclusion <| s₁.subset_union_right s₂)]
  rfl
[GOAL]
case intro.intro.intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ s q₁_1 q₂_1,
    ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) q₁_1 ∧ ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) q₂_1
[PROOFSTEP]
use s₁ ∪ s₂
[GOAL]
case h
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ q₁_1 q₂_1,
    ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) q₁_1 ∧ ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) q₂_1
[PROOFSTEP]
use rename (Set.inclusion <| s₁.subset_union_left s₂) q₁
[GOAL]
case h
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ q₂_1,
    ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₁ ⊆ s₁ ∪ s₂))) q₁) ∧
      ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) q₂_1
[PROOFSTEP]
use rename (Set.inclusion <| s₁.subset_union_right s₂) q₂
[GOAL]
case h
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₁ ⊆ s₁ ∪ s₂))) q₁) ∧
    ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₂ ⊆ s₁ ∪ s₂))) q₂)
[PROOFSTEP]
constructor
  -- porting note: was `<;> simp <;> rfl` but Lean couldn't infer the arguments
[GOAL]
case h.left
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₁ ⊆ s₁ ∪ s₂))) q₁)
[PROOFSTEP]
rw [rename_rename (Set.inclusion <| s₁.subset_union_left s₂)]
[GOAL]
case h.left
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₁ = ↑(rename (Subtype.val ∘ inclusion (_ : s₁ ⊆ s₁ ∪ s₂))) q₁
[PROOFSTEP]
rfl
[GOAL]
case h.right
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₂ ⊆ s₁ ∪ s₂))) q₂)
[PROOFSTEP]
rw [rename_rename (Set.inclusion <| s₁.subset_union_right s₂)]
[GOAL]
case h.right
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₂ = ↑(rename (Subtype.val ∘ inclusion (_ : s₂ ⊆ s₁ ∪ s₂))) q₂
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∃ n f _hf q, p = ↑(rename f) q
[PROOFSTEP]
obtain ⟨s, q, rfl⟩ := exists_finset_rename p
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
⊢ ∃ n f _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
[PROOFSTEP]
let n := Fintype.card { x // x ∈ s }
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
⊢ ∃ n f _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
[PROOFSTEP]
let e := Fintype.equivFin { x // x ∈ s }
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ ∃ n f _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
[PROOFSTEP]
refine' ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, _⟩
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ ↑(rename Subtype.val) q = ↑(rename (Subtype.val ∘ ↑e.symm)) (↑(rename ↑e) q)
[PROOFSTEP]
rw [← rename_rename, rename_rename e]
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ ↑(rename Subtype.val) q = ↑(rename Subtype.val) (↑(rename (↑e.symm ∘ ↑e)) q)
[PROOFSTEP]
simp only [Function.comp, Equiv.symm_apply_apply, rename_rename]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p : MvPolynomial σ ℤ
⊢ eval₂ c (g ∘ f) p = eval₂ c g (↑(rename f) p)
[PROOFSTEP]
apply
  MvPolynomial.induction_on p (fun n => by simp only [eval₂_C, rename_C])
    (fun p q hp hq => by simp only [hp, hq, rename, eval₂_add, AlgHom.map_add]) fun p n hp => by
    simp only [eval₂_mul, hp, eval₂_X, comp_apply, map_mul, rename_X, eval₂_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p : MvPolynomial σ ℤ
n : ℤ
⊢ eval₂ c (g ∘ f) (↑C n) = eval₂ c g (↑(rename f) (↑C n))
[PROOFSTEP]
simp only [eval₂_C, rename_C]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p✝ p q : MvPolynomial σ ℤ
hp : eval₂ c (g ∘ f) p = eval₂ c g (↑(rename f) p)
hq : eval₂ c (g ∘ f) q = eval₂ c g (↑(rename f) q)
⊢ eval₂ c (g ∘ f) (p + q) = eval₂ c g (↑(rename f) (p + q))
[PROOFSTEP]
simp only [hp, hq, rename, eval₂_add, AlgHom.map_add]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p✝ p : MvPolynomial σ ℤ
n : σ
hp : eval₂ c (g ∘ f) p = eval₂ c g (↑(rename f) p)
⊢ eval₂ c (g ∘ f) (p * X n) = eval₂ c g (↑(rename f) (p * X n))
[PROOFSTEP]
simp only [eval₂_mul, hp, eval₂_X, comp_apply, map_mul, rename_X, eval₂_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (Finsupp.mapDomain f d) (↑(rename f) φ) = coeff d φ
[PROOFSTEP]
classical
apply
  φ.induction_on' (P := fun ψ => coeff (Finsupp.mapDomain f d) ((rename f) ψ) = coeff d ψ)
    -- Lean could no longer infer the motive
· intro u r
  rw [rename_monomial, coeff_monomial, coeff_monomial]
  simp only [(Finsupp.mapDomain_injective hf).eq_iff]
· intros
  simp only [*, AlgHom.map_add, coeff_add]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (Finsupp.mapDomain f d) (↑(rename f) φ) = coeff d φ
[PROOFSTEP]
apply
  φ.induction_on' (P := fun ψ => coeff (Finsupp.mapDomain f d) ((rename f) ψ) = coeff d ψ)
    -- Lean could no longer infer the motive
[GOAL]
case h1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ (u : σ →₀ ℕ) (a : R), coeff (Finsupp.mapDomain f d) (↑(rename f) (↑(monomial u) a)) = coeff d (↑(monomial u) a)
[PROOFSTEP]
intro u r
[GOAL]
case h1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d u : σ →₀ ℕ
r : R
⊢ coeff (Finsupp.mapDomain f d) (↑(rename f) (↑(monomial u) r)) = coeff d (↑(monomial u) r)
[PROOFSTEP]
rw [rename_monomial, coeff_monomial, coeff_monomial]
[GOAL]
case h1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d u : σ →₀ ℕ
r : R
⊢ (if Finsupp.mapDomain f u = Finsupp.mapDomain f d then r else 0) = if u = d then r else 0
[PROOFSTEP]
simp only [(Finsupp.mapDomain_injective hf).eq_iff]
[GOAL]
case h2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ (p q : MvPolynomial σ R),
    coeff (Finsupp.mapDomain f d) (↑(rename f) p) = coeff d p →
      coeff (Finsupp.mapDomain f d) (↑(rename f) q) = coeff d q →
        coeff (Finsupp.mapDomain f d) (↑(rename f) (p + q)) = coeff d (p + q)
[PROOFSTEP]
intros
[GOAL]
case h2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
p✝ q✝ : MvPolynomial σ R
a✝¹ : coeff (Finsupp.mapDomain f d) (↑(rename f) p✝) = coeff d p✝
a✝ : coeff (Finsupp.mapDomain f d) (↑(rename f) q✝) = coeff d q✝
⊢ coeff (Finsupp.mapDomain f d) (↑(rename f) (p✝ + q✝)) = coeff d (p✝ + q✝)
[PROOFSTEP]
simp only [*, AlgHom.map_add, coeff_add]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d (↑(rename f) φ) = 0
[PROOFSTEP]
classical
rw [rename_eq, ← not_mem_support_iff]
intro H
replace H := mapDomain_support H
rw [Finset.mem_image] at H
obtain ⟨u, hu, rfl⟩ := H
specialize h u rfl
simp at h hu
contradiction
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d (↑(rename f) φ) = 0
[PROOFSTEP]
rw [rename_eq, ← not_mem_support_iff]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ ¬d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
[PROOFSTEP]
intro H
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
⊢ False
[PROOFSTEP]
replace H := mapDomain_support H
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support
⊢ False
[PROOFSTEP]
rw [Finset.mem_image] at H
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : ∃ a, a ∈ φ.support ∧ Finsupp.mapDomain f a = d
⊢ False
[PROOFSTEP]
obtain ⟨u, hu, rfl⟩ := H
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0
⊢ False
[PROOFSTEP]
specialize h u rfl
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : coeff u φ = 0
⊢ False
[PROOFSTEP]
simp at h hu
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
h : coeff u φ = 0
hu : ¬↑φ u = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : coeff d (↑(rename f) φ) ≠ 0
⊢ ∃ u, Finsupp.mapDomain f u = d ∧ coeff u φ ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d (↑(rename f) φ) = 0
[PROOFSTEP]
apply coeff_rename_eq_zero _ _ _ h
[GOAL]
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ↑constantCoeff (↑(rename f) φ) = ↑constantCoeff φ
[PROOFSTEP]
apply φ.induction_on
[GOAL]
case h_C
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (a : R), ↑constantCoeff (↑(rename f) (↑C a)) = ↑constantCoeff (↑C a)
[PROOFSTEP]
intro a
[GOAL]
case h_C
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
a : R
⊢ ↑constantCoeff (↑(rename f) (↑C a)) = ↑constantCoeff (↑C a)
[PROOFSTEP]
simp only [constantCoeff_C, rename_C]
[GOAL]
case h_add
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p →
      ↑constantCoeff (↑(rename f) q) = ↑constantCoeff q → ↑constantCoeff (↑(rename f) (p + q)) = ↑constantCoeff (p + q)
[PROOFSTEP]
intro p q hp hq
[GOAL]
case h_add
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ p q : MvPolynomial σ R
hp : ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p
hq : ↑constantCoeff (↑(rename f) q) = ↑constantCoeff q
⊢ ↑constantCoeff (↑(rename f) (p + q)) = ↑constantCoeff (p + q)
[PROOFSTEP]
simp only [hp, hq, RingHom.map_add, AlgHom.map_add]
[GOAL]
case h_X
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p →
      ↑constantCoeff (↑(rename f) (p * X n)) = ↑constantCoeff (p * X n)
[PROOFSTEP]
intro p n hp
[GOAL]
case h_X
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ p : MvPolynomial σ R
n : σ
hp : ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p
⊢ ↑constantCoeff (↑(rename f) (p * X n)) = ↑constantCoeff (p * X n)
[PROOFSTEP]
simp only [hp, rename_X, constantCoeff_X, RingHom.map_mul, AlgHom.map_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
p : MvPolynomial σ R
f : σ → τ
inst✝ : DecidableEq τ
h : Injective f
⊢ support (↑(rename f) p) = Finset.image (Finsupp.mapDomain f) (support p)
[PROOFSTEP]
rw [rename_eq]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
p : MvPolynomial σ R
f : σ → τ
inst✝ : DecidableEq τ
h : Injective f
⊢ support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) (support p)
[PROOFSTEP]
exact Finsupp.mapDomain_support_of_injective (mapDomain_injective h) _


[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
ι : Type u_1
hι : Nonempty ι
f : ι → α
D : Directed r f
s : Finset ι
z x✝ : ι
⊢ x✝ ∈ 0 → r (f x✝) (f z)
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
s t : Set α
inst✝ : OrderedCancelCommMonoid α
hs : IsPwo s
ht : IsPwo t
⊢ IsPwo (s * t)
[PROOFSTEP]
rw [← image_mul_prod]
[GOAL]
α : Type u_1
s t : Set α
inst✝ : OrderedCancelCommMonoid α
hs : IsPwo s
ht : IsPwo t
⊢ IsPwo ((fun x => x.fst * x.snd) '' s ×ˢ t)
[PROOFSTEP]
exact (hs.prod ht).image_of_monotone (monotone_fst.mul' monotone_snd)
[GOAL]
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
⊢ min (_ : IsWf (s * t)) (_ : Set.Nonempty (s * t)) = min hs hsn * min ht htn
[PROOFSTEP]
refine' le_antisymm (IsWf.min_le _ _ (mem_mul.2 ⟨_, _, hs.min_mem _, ht.min_mem _, rfl⟩)) _
[GOAL]
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
⊢ min hs hsn * min ht htn ≤ min (_ : IsWf (s * t)) (_ : Set.Nonempty (s * t))
[PROOFSTEP]
rw [IsWf.le_min_iff]
[GOAL]
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
⊢ ∀ (b : α), b ∈ s * t → min hs hsn * min ht htn ≤ b
[PROOFSTEP]
rintro _ ⟨x, y, hx, hy, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
x y : α
hx : x ∈ s
hy : y ∈ t
⊢ min hs hsn * min ht htn ≤ (fun x x_1 => x * x_1) x y
[PROOFSTEP]
exact mul_le_mul' (hs.min_le _ hx) (ht.min_le _ hy)
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : Set.IsPwo s
ht : Set.IsPwo t
a : α
u : Set α
hu : Set.IsPwo u
x : α × α
⊢ x ∈ mulAntidiagonal hs ht a ↔ x.fst ∈ s ∧ x.snd ∈ t ∧ x.fst * x.snd = a
[PROOFSTEP]
simp only [mulAntidiagonal, Set.Finite.mem_toFinset, Set.mem_mulAntidiagonal]
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : Set.IsPwo s
ht : Set.IsPwo t
a : α
u : Set α
hu : Set.IsPwo u
x : α × α
⊢ Prod.swap x ∈ mulAntidiagonal hs ht a ↔ x ∈ mulAntidiagonal ht hs a
[PROOFSTEP]
simp only [mem_mulAntidiagonal, Prod.fst_swap, Prod.snd_swap, Set.swap_mem_mulAntidiagonal_aux, Set.mem_mulAntidiagonal]
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : Set.IsPwo s
ht : Set.IsPwo t
a✝ : α
u : Set α
hu : Set.IsPwo u
x : α × α
a : α
x✝ : a ∈ {a | Finset.Nonempty (mulAntidiagonal hs ht a)}
b : α × α
hb : b ∈ mulAntidiagonal hs ht a
⊢ a ∈ s * t
[PROOFSTEP]
rw [mem_mulAntidiagonal] at hb
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : Set.IsPwo s
ht : Set.IsPwo t
a✝ : α
u : Set α
hu : Set.IsPwo u
x : α × α
a : α
x✝ : a ∈ {a | Finset.Nonempty (mulAntidiagonal hs ht a)}
b : α × α
hb : b.fst ∈ s ∧ b.snd ∈ t ∧ b.fst * b.snd = a
⊢ a ∈ s * t
[PROOFSTEP]
exact ⟨b.1, b.2, hb⟩
[GOAL]
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
⊢ mulAntidiagonal (_ : Set.IsPwo s) (_ : Set.IsPwo t) (Set.IsWf.min hs hns * Set.IsWf.min ht hnt) =
    {(Set.IsWf.min hs hns, Set.IsWf.min ht hnt)}
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case a.mk
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
a b : α
⊢ (a, b) ∈ mulAntidiagonal (_ : Set.IsPwo s) (_ : Set.IsPwo t) (Set.IsWf.min hs hns * Set.IsWf.min ht hnt) ↔
    (a, b) ∈ {(Set.IsWf.min hs hns, Set.IsWf.min ht hnt)}
[PROOFSTEP]
simp only [mem_mulAntidiagonal, mem_singleton, Prod.ext_iff]
[GOAL]
case a.mk
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = Set.IsWf.min hs hns * Set.IsWf.min ht hnt ↔ a = Set.IsWf.min hs hns ∧ b = Set.IsWf.min ht hnt
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = Set.IsWf.min hs hns * Set.IsWf.min ht hnt → a = Set.IsWf.min hs hns ∧ b = Set.IsWf.min ht hnt
[PROOFSTEP]
rintro ⟨has, hat, hst⟩
[GOAL]
case a.mk.mp.intro.intro
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
a b : α
has : a ∈ s
hat : b ∈ t
hst : a * b = Set.IsWf.min hs hns * Set.IsWf.min ht hnt
⊢ a = Set.IsWf.min hs hns ∧ b = Set.IsWf.min ht hnt
[PROOFSTEP]
obtain rfl := (hs.min_le hns has).eq_of_not_lt fun hlt => (mul_lt_mul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst
[GOAL]
case a.mk.mp.intro.intro
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
b : α
hat : b ∈ t
has : Set.IsWf.min hs hns ∈ s
hst : Set.IsWf.min hs hns * b = Set.IsWf.min hs hns * Set.IsWf.min ht hnt
⊢ Set.IsWf.min hs hns = Set.IsWf.min hs hns ∧ b = Set.IsWf.min ht hnt
[PROOFSTEP]
exact ⟨rfl, mul_left_cancel hst⟩
[GOAL]
case a.mk.mpr
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
a b : α
⊢ a = Set.IsWf.min hs hns ∧ b = Set.IsWf.min ht hnt → a ∈ s ∧ b ∈ t ∧ a * b = Set.IsWf.min hs hns * Set.IsWf.min ht hnt
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case a.mk.mpr.intro
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
⊢ Set.IsWf.min hs hns ∈ s ∧
    Set.IsWf.min ht hnt ∈ t ∧ Set.IsWf.min hs hns * Set.IsWf.min ht hnt = Set.IsWf.min hs hns * Set.IsWf.min ht hnt
[PROOFSTEP]
exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩


[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ∈ (fun s t => filter ((fun x x_1 => x ⊆ x_1) s) (powerset t)) s t ↔ s ≤ u ∧ u ≤ t
[PROOFSTEP]
rw [mem_filter, mem_powerset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ⊆ t ∧ (fun x x_1 => x ⊆ x_1) s u ↔ s ≤ u ∧ u ≤ t
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ∈ (fun s t => filter ((fun x x_1 => x ⊆ x_1) s) (ssubsets t)) s t ↔ s ≤ u ∧ u < t
[PROOFSTEP]
rw [mem_filter, mem_ssubsets]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ⊂ t ∧ (fun x x_1 => x ⊆ x_1) s u ↔ s ≤ u ∧ u < t
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ∈ (fun s t => filter ((fun x x_1 => x ⊂ x_1) s) (powerset t)) s t ↔ s < u ∧ u ≤ t
[PROOFSTEP]
rw [mem_filter, mem_powerset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ⊆ t ∧ (fun x x_1 => x ⊂ x_1) s u ↔ s < u ∧ u ≤ t
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ∈ (fun s t => filter ((fun x x_1 => x ⊂ x_1) s) (ssubsets t)) s t ↔ s < u ∧ u < t
[PROOFSTEP]
rw [mem_filter, mem_ssubsets]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ⊂ t ∧ (fun x x_1 => x ⊂ x_1) s u ↔ s < u ∧ u < t
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Icc s t = image ((fun x x_1 => x ∪ x_1) s) (powerset (t \ s))
[PROOFSTEP]
ext u
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ u ∈ Icc s t ↔ u ∈ image ((fun x x_1 => x ∪ x_1) s) (powerset (t \ s))
[PROOFSTEP]
simp_rw [mem_Icc, mem_image, mem_powerset]
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u ≤ t ↔ ∃ a, a ⊆ t \ s ∧ s ∪ a = u
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u ≤ t → ∃ a, a ⊆ t \ s ∧ s ∪ a = u
[PROOFSTEP]
rintro ⟨hs, ht⟩
[GOAL]
case a.mp.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hs : s ≤ u
ht : u ≤ t
⊢ ∃ a, a ⊆ t \ s ∧ s ∪ a = u
[PROOFSTEP]
exact ⟨u \ s, sdiff_le_sdiff_right ht, sup_sdiff_cancel_right hs⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ (∃ a, a ⊆ t \ s ∧ s ∪ a = u) → s ≤ u ∧ u ≤ t
[PROOFSTEP]
rintro ⟨v, hv, rfl⟩
[GOAL]
case a.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
v : Finset α
hv : v ⊆ t \ s
⊢ s ≤ s ∪ v ∧ s ∪ v ≤ t
[PROOFSTEP]
exact ⟨le_sup_left, union_subset h <| hv.trans <| sdiff_subset _ _⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Ico s t = image ((fun x x_1 => x ∪ x_1) s) (ssubsets (t \ s))
[PROOFSTEP]
ext u
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ u ∈ Ico s t ↔ u ∈ image ((fun x x_1 => x ∪ x_1) s) (ssubsets (t \ s))
[PROOFSTEP]
simp_rw [mem_Ico, mem_image, mem_ssubsets]
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u < t ↔ ∃ a, a ⊂ t \ s ∧ s ∪ a = u
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u < t → ∃ a, a ⊂ t \ s ∧ s ∪ a = u
[PROOFSTEP]
rintro ⟨hs, ht⟩
[GOAL]
case a.mp.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hs : s ≤ u
ht : u < t
⊢ ∃ a, a ⊂ t \ s ∧ s ∪ a = u
[PROOFSTEP]
exact ⟨u \ s, sdiff_lt_sdiff_right ht hs, sup_sdiff_cancel_right hs⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ (∃ a, a ⊂ t \ s ∧ s ∪ a = u) → s ≤ u ∧ u < t
[PROOFSTEP]
rintro ⟨v, hv, rfl⟩
[GOAL]
case a.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
v : Finset α
hv : v ⊂ t \ s
⊢ s ≤ s ∪ v ∧ s ∪ v < t
[PROOFSTEP]
exact ⟨le_sup_left, sup_lt_of_lt_sdiff_left hv h⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ card (Icc s t) = 2 ^ (card t - card s)
[PROOFSTEP]
rw [← card_sdiff h, ← card_powerset, Icc_eq_image_powerset h, Finset.card_image_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Set.InjOn ((fun x x_1 => x ∪ x_1) s) ↑(powerset (t \ s))
[PROOFSTEP]
rintro u hu v hv (huv : s ⊔ u = s ⊔ v)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hu : u ∈ ↑(powerset (t \ s))
v : Finset α
hv : v ∈ ↑(powerset (t \ s))
huv : s ⊔ u = s ⊔ v
⊢ u = v
[PROOFSTEP]
rw [mem_coe, mem_powerset] at hu hv
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hu : u ⊆ t \ s
v : Finset α
hv : v ⊆ t \ s
huv : s ⊔ u = s ⊔ v
⊢ u = v
[PROOFSTEP]
rw [← (disjoint_sdiff.mono_right hu : Disjoint s u).sup_sdiff_cancel_left, ←
  (disjoint_sdiff.mono_right hv : Disjoint s v).sup_sdiff_cancel_left, huv]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ card (Ico s t) = 2 ^ (card t - card s) - 1
[PROOFSTEP]
rw [card_Ico_eq_card_Icc_sub_one, card_Icc_finset h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ card (Ioc s t) = 2 ^ (card t - card s) - 1
[PROOFSTEP]
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc_finset h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ card (Ioo s t) = 2 ^ (card t - card s) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc_finset h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ card (Iic s) = 2 ^ card s
[PROOFSTEP]
rw [Iic_eq_powerset, card_powerset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ card (Iio s) = 2 ^ card s - 1
[PROOFSTEP]
rw [Iio_eq_ssubsets, ssubsets, card_erase_of_mem (mem_powerset_self _), card_powerset]