[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
⊢ bind₁ X = AlgHom.id R (MvPolynomial σ R)
[PROOFSTEP]
ext1 i
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
i : σ
⊢ ↑(bind₁ X) (X i) = ↑(AlgHom.id R (MvPolynomial σ R)) (X i)
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
x : R
⊢ ↑(bind₁ f) (↑C x) = ↑C x
[PROOFSTEP]
simp [bind₁, algebraMap_eq]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ bind₂ C = RingHom.id (MvPolynomial σ R)
[PROOFSTEP]
ext : 2
[GOAL]
case hC.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
x✝ : R
⊢ ↑(RingHom.comp (bind₂ C) C) x✝ = ↑(RingHom.comp (RingHom.id (MvPolynomial σ R)) C) x✝
[PROOFSTEP]
simp
[GOAL]
case hX.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(bind₂ C) (X i✝)) = coeff m✝ (↑(RingHom.id (MvPolynomial σ R)) (X i✝))
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
φ : MvPolynomial σ R
⊢ ↑join₂ (↑(map f) φ) = ↑(bind₂ f) φ
[PROOFSTEP]
simp only [join₂, bind₂, eval₂Hom_map_hom, RingHom.id_comp]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
p : MvPolynomial σ R
⊢ ↑(aeval id) (↑(rename f) p) = ↑(aeval f) p
[PROOFSTEP]
rw [aeval_rename, Function.comp.left_id]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
φ : MvPolynomial σ R
⊢ ↑(bind₁ g) (↑(bind₁ f) φ) = ↑(bind₁ fun i => ↑(bind₁ g) (f i)) φ
[PROOFSTEP]
simp [bind₁, ← comp_aeval]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
⊢ AlgHom.comp (bind₁ g) (bind₁ f) = bind₁ fun i => ↑(bind₁ g) (f i)
[PROOFSTEP]
ext1
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
i✝ : σ
⊢ ↑(AlgHom.comp (bind₁ g) (bind₁ f)) (X i✝) = ↑(bind₁ fun i => ↑(bind₁ g) (f i)) (X i✝)
[PROOFSTEP]
apply bind₁_bind₁
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
⊢ RingHom.comp (bind₂ g) (bind₂ f) = bind₂ (RingHom.comp (bind₂ g) f)
[PROOFSTEP]
ext : 2
[GOAL]
case hC.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (bind₂ g) (bind₂ f)) C) x✝ = ↑(RingHom.comp (bind₂ (RingHom.comp (bind₂ g) f)) C) x✝
[PROOFSTEP]
simp
[GOAL]
case hX.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(RingHom.comp (bind₂ g) (bind₂ f)) (X i✝)) = coeff m✝ (↑(bind₂ (RingHom.comp (bind₂ g) f)) (X i✝))
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
⊢ AlgHom.comp (rename g) (bind₁ f) = bind₁ fun i => ↑(rename g) (f i)
[PROOFSTEP]
ext1 i
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
i : σ
⊢ ↑(AlgHom.comp (rename g) (bind₁ f)) (X i) = ↑(bind₁ fun i => ↑(rename g) (f i)) (X i)
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ ↑(map g) (↑(bind₂ f) φ) = ↑(bind₂ (RingHom.comp (map g) f)) φ
[PROOFSTEP]
simp only [bind₂, eval₂_comp_right, coe_eval₂Hom, eval₂_map]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (map g) f) (↑(map g) ∘ X) φ = eval₂ (RingHom.comp (map g) f) X φ
[PROOFSTEP]
congr 1 with : 1
[GOAL]
case e_g.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
x✝ : σ
⊢ (↑(map g) ∘ X) x✝ = X x✝
[PROOFSTEP]
simp only [Function.comp_apply, map_X]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
⊢ AlgHom.comp (bind₁ f) (rename g) = bind₁ (f ∘ g)
[PROOFSTEP]
ext1 i
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
i : σ
⊢ ↑(AlgHom.comp (bind₁ f) (rename g)) (X i) = ↑(bind₁ (f ∘ g)) (X i)
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : S →+* MvPolynomial σ T
g : R →+* S
φ : MvPolynomial σ R
⊢ ↑(bind₂ f) (↑(map g) φ) = ↑(bind₂ (RingHom.comp f g)) φ
[PROOFSTEP]
simp [bind₂]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
⊢ RingHom.comp (map f) C = RingHom.comp C f
[PROOFSTEP]
ext1
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
x✝ : R
⊢ ↑(RingHom.comp (map f) C) x✝ = ↑(RingHom.comp C f) x✝
[PROOFSTEP]
apply map_C
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑f (↑(bind₁ g) φ) = ↑(eval₂Hom (RingHom.comp f C) fun i => ↑f (g i)) φ
[PROOFSTEP]
rw [bind₁, map_aeval, algebraMap_eq]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(map f) (↑(bind₁ g) φ) = ↑(bind₁ fun i => ↑(map f) (g i)) (↑(map f) φ)
[PROOFSTEP]
rw [hom_bind₁, map_comp_C, ← eval₂Hom_map_hom]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(eval₂Hom C fun i => ↑(map f) (g i)) (↑(map f) φ) = ↑(bind₁ fun i => ↑(map f) (g i)) (↑(map f) φ)
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → S
⊢ RingHom.comp (eval₂Hom f g) C = f
[PROOFSTEP]
ext1 r
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → S
r : R
⊢ ↑(RingHom.comp (eval₂Hom f g) C) r = ↑f r
[PROOFSTEP]
exact eval₂_C f g r
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : τ → S
h : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(eval₂Hom f g) (↑(bind₁ h) φ) = ↑(eval₂Hom f fun i => ↑(eval₂Hom f g) (h i)) φ
[PROOFSTEP]
rw [hom_bind₁, eval₂Hom_comp_C]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : Algebra R S
f : τ → S
g : σ → MvPolynomial τ R
⊢ AlgHom.comp (aeval f) (bind₁ g) = aeval fun i => ↑(aeval f) (g i)
[PROOFSTEP]
ext1
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : Algebra R S
f : τ → S
g : σ → MvPolynomial τ R
i✝ : σ
⊢ ↑(AlgHom.comp (aeval f) (bind₁ g)) (X i✝) = ↑(aeval fun i => ↑(aeval f) (g i)) (X i✝)
[PROOFSTEP]
apply aeval_bind₁
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
⊢ RingHom.comp (eval₂Hom f g) (bind₂ h) = eval₂Hom (RingHom.comp (eval₂Hom f g) h) g
[PROOFSTEP]
ext : 2
[GOAL]
case hC.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (eval₂Hom f g) (bind₂ h)) C) x✝ =
    ↑(RingHom.comp (eval₂Hom (RingHom.comp (eval₂Hom f g) h) g) C) x✝
[PROOFSTEP]
simp
[GOAL]
case hX
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
i✝ : σ
⊢ ↑(RingHom.comp (eval₂Hom f g) (bind₂ h)) (X i✝) = ↑(eval₂Hom (RingHom.comp (eval₂Hom f g) h) g) (X i✝)
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
d : σ →₀ ℕ
r : R
⊢ ↑(bind₁ f) (↑(monomial d) r) = ↑C r * ∏ i in d.support, f i ^ ↑d i
[PROOFSTEP]
simp only [monomial_eq, AlgHom.map_mul, bind₁_C_right, Finsupp.prod, AlgHom.map_prod, AlgHom.map_pow, bind₁_X_right]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
r : R
⊢ ↑(bind₂ f) (↑(monomial d) r) = ↑f r * ↑(monomial d) 1
[PROOFSTEP]
simp only [monomial_eq, RingHom.map_mul, bind₂_C_right, Finsupp.prod, map_prod, map_pow, bind₂_X_right, C_1, one_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
⊢ ↑(bind₂ f) (↑(monomial d) 1) = ↑(monomial d) 1
[PROOFSTEP]
rw [bind₂_monomial, f.map_one, one_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ vars (↑(bind₁ f) φ) ⊆ Finset.biUnion (vars φ) fun i => vars (f i)
[PROOFSTEP]
calc
  (bind₁ f φ).vars = (φ.support.sum fun x : σ →₀ ℕ => (bind₁ f) (monomial x (coeff x φ))).vars := by
    rw [← AlgHom.map_sum, ← φ.as_sum]
  _ ≤ φ.support.biUnion fun i : σ →₀ ℕ => ((bind₁ f) (monomial i (coeff i φ))).vars := (vars_sum_subset _ _)
  _ = φ.support.biUnion fun d : σ →₀ ℕ => vars (C (coeff d φ) * ∏ i in d.support, f i ^ d i) := by
    simp only [bind₁_monomial]
  _ ≤ φ.support.biUnion fun d : σ →₀ ℕ => d.support.biUnion fun i => vars (f i) :=
    ?_
      -- proof below
  _ ≤ φ.vars.biUnion fun i : σ => vars (f i) :=
    ?_
      -- proof below
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ vars (↑(bind₁ f) φ) = vars (∑ x in support φ, ↑(bind₁ f) (↑(monomial x) (coeff x φ)))
[PROOFSTEP]
rw [← AlgHom.map_sum, ← φ.as_sum]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (Finset.biUnion (support φ) fun i => vars (↑(bind₁ f) (↑(monomial i) (coeff i φ)))) =
    Finset.biUnion (support φ) fun d => vars (↑C (coeff d φ) * ∏ i in d.support, f i ^ ↑d i)
[PROOFSTEP]
simp only [bind₁_monomial]
[GOAL]
case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (Finset.biUnion (support φ) fun d => vars (↑C (coeff d φ) * ∏ i in d.support, f i ^ ↑d i)) ≤
    Finset.biUnion (support φ) fun d => Finset.biUnion d.support fun i => vars (f i)
[PROOFSTEP]
apply Finset.biUnion_mono
[GOAL]
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ∀ (a : σ →₀ ℕ),
    a ∈ support φ → vars (↑C (coeff a φ) * ∏ i in a.support, f i ^ ↑a i) ⊆ Finset.biUnion a.support fun i => vars (f i)
[PROOFSTEP]
intro d _hd
[GOAL]
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ support φ
⊢ vars (↑C (coeff d φ) * ∏ i in d.support, f i ^ ↑d i) ⊆ Finset.biUnion d.support fun i => vars (f i)
[PROOFSTEP]
calc
  vars (C (coeff d φ) * ∏ i : σ in d.support, f i ^ d i) ≤
      (C (coeff d φ)).vars ∪ (∏ i : σ in d.support, f i ^ d i).vars :=
    vars_mul _ _
  _ ≤ (∏ i : σ in d.support, f i ^ d i).vars := by
    simp only [Finset.empty_union, vars_C, Finset.le_iff_subset, Finset.Subset.refl]
  _ ≤ d.support.biUnion fun i : σ => vars (f i ^ d i) := (vars_prod _)
  _ ≤ d.support.biUnion fun i : σ => (f i).vars := ?_
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ support φ
⊢ vars (↑C (coeff d φ)) ∪ vars (∏ i in d.support, f i ^ ↑d i) ≤ vars (∏ i in d.support, f i ^ ↑d i)
[PROOFSTEP]
simp only [Finset.empty_union, vars_C, Finset.le_iff_subset, Finset.Subset.refl]
[GOAL]
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ support φ
⊢ (Finset.biUnion d.support fun i => vars (f i ^ ↑d i)) ≤ Finset.biUnion d.support fun i => vars (f i)
[PROOFSTEP]
apply Finset.biUnion_mono
[GOAL]
case calc_1.h.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ support φ
⊢ ∀ (a : σ), a ∈ d.support → vars (f a ^ ↑d a) ⊆ vars (f a)
[PROOFSTEP]
intro i _hi
[GOAL]
case calc_1.h.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ support φ
i : σ
_hi : i ∈ d.support
⊢ vars (f i ^ ↑d i) ⊆ vars (f i)
[PROOFSTEP]
apply vars_pow
[GOAL]
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (Finset.biUnion (support φ) fun d => Finset.biUnion d.support fun i => vars (f i)) ≤
    Finset.biUnion (vars φ) fun i => vars (f i)
[PROOFSTEP]
intro j
[GOAL]
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
⊢ (j ∈ Finset.biUnion (support φ) fun d => Finset.biUnion d.support fun i => vars (f i)) →
    j ∈ Finset.biUnion (vars φ) fun i => vars (f i)
[PROOFSTEP]
simp_rw [Finset.mem_biUnion]
[GOAL]
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
⊢ (∃ a, a ∈ support φ ∧ ∃ a_1, a_1 ∈ a.support ∧ j ∈ vars (f a_1)) → ∃ a, a ∈ vars φ ∧ j ∈ vars (f a)
[PROOFSTEP]
rintro ⟨d, hd, ⟨i, hi, hj⟩⟩
[GOAL]
case calc_2.intro.intro.intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
d : σ →₀ ℕ
hd : d ∈ support φ
i : σ
hi : i ∈ d.support
hj : j ∈ vars (f i)
⊢ ∃ a, a ∈ vars φ ∧ j ∈ vars (f a)
[PROOFSTEP]
exact ⟨i, (mem_vars _).mpr ⟨d, hd, hi⟩, hj⟩
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
h : j ∈ vars (↑(bind₁ f) φ)
⊢ ∃ i, i ∈ vars φ ∧ j ∈ vars (f i)
[PROOFSTEP]
classical simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne.def] using vars_bind₁ f φ h
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
h : j ∈ vars (↑(bind₁ f) φ)
⊢ ∃ i, i ∈ vars φ ∧ j ∈ vars (f i)
[PROOFSTEP]
simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne.def] using vars_bind₁ f φ h
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1605153}, Functor.mapConst = Functor.map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1605153
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
rfl
  -- porting note: I guess `map_const` no longer has a default implementation?
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α : Type ?u.1605153} (x : MvPolynomial α R), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ : Type ?u.1605153
x✝ : MvPolynomial α✝ R
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp [(· <$> ·)]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β γ : Type ?u.1605153} (g : α → β) (h : β → γ) (x : MvPolynomial α R), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ γ✝ : Type ?u.1605153
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : MvPolynomial α✝ R
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
simp [(· <$> ·)]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (x : MvPolynomial α R) (y : MvPolynomial β R),
    (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Seq.seq (Function.const β✝ <$> x✝) fun x => y✝
[PROOFSTEP]
simp [SeqLeft.seqLeft, Seq.seq, (· <$> ·), bind₁_rename]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ ↑(bind₁ fun a => ↑(bind₁ fun x => X a) y✝) x✝ = ↑(bind₁ ((fun y => ↑(rename y) y✝) ∘ Function.const β✝)) x✝
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (x : MvPolynomial α R) (y : MvPolynomial β R),
    (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝
[PROOFSTEP]
simp [SeqRight.seqRight, Seq.seq, (· <$> ·), bind₁_rename]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ ↑(bind₁ fun x => y✝) x✝ = ↑(bind₁ (Function.const α✝ y✝)) x✝
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (g : α → β) (x : MvPolynomial α R), (Seq.seq (pure g) fun x_1 => x) = g <$> x
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
g✝ : α✝ → β✝
x✝ : MvPolynomial α✝ R
⊢ (Seq.seq (pure g✝) fun x => x✝) = g✝ <$> x✝
[PROOFSTEP]
simp [(· <$> ·), pure, Seq.seq]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (f : α → β) (x : MvPolynomial α R),
    (do
        let a ← x
        pure (f a)) =
      f <$> x
[PROOFSTEP]
aesop
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (f : MvPolynomial (α → β) R) (x : MvPolynomial α R),
    (do
        let x_1 ← f
        x_1 <$> x) =
      Seq.seq f fun x_1 => x
[PROOFSTEP]
aesop
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (x : α) (f : α → MvPolynomial β R), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
x✝ : α✝
f✝ : α✝ → MvPolynomial β✝ R
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
simp [pure, bind]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β γ : Type ?u.1607152} (x : MvPolynomial α R) (f : α → MvPolynomial β R) (g : β → MvPolynomial γ R),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ γ✝ : Type ?u.1607152
x✝ : MvPolynomial α✝ R
f✝ : α✝ → MvPolynomial β✝ R
g✝ : β✝ → MvPolynomial γ✝ R
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
simp [bind, ← bind₁_comp_bind₁]


[GOAL]
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ r • s • x = s • r • x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s • x).re = (s • r • x).re
[PROOFSTEP]
simp [smul_re, smul_im, smul_comm]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s • x).im = (s • r • x).im
[PROOFSTEP]
simp [smul_re, smul_im, smul_comm]
[GOAL]
R : Type u_1
S : Type u_2
inst✝³ : SMul R S
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s) • x = r • s • x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝³ : SMul R S
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ ((r • s) • x).re = (r • s • x).re
[PROOFSTEP]
simp [smul_re, smul_im, smul_assoc]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝³ : SMul R S
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ ((r • s) • x).im = (r • s • x).im
[PROOFSTEP]
simp [smul_re, smul_im, smul_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ MulOpposite.op r • x = r • x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ (MulOpposite.op r • x).re = (r • x).re
[PROOFSTEP]
simp [smul_re, smul_im, op_smul_eq_smul]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ (MulOpposite.op r • x).im = (r • x).im
[PROOFSTEP]
simp [smul_re, smul_im, op_smul_eq_smul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ 1 • x = x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ (1 • x).re = x.re
[PROOFSTEP]
simp [smul_re, smul_im, one_smul]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ (1 • x).im = x.im
[PROOFSTEP]
simp [smul_re, smul_im, one_smul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ (r * s) • x = r • s • x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ ((r * s) • x).re = (r • s • x).re
[PROOFSTEP]
simp [smul_re, smul_im, mul_smul]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ ((r * s) • x).im = (r • s • x).im
[PROOFSTEP]
simp [smul_re, smul_im, mul_smul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ r • 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ (r • 0).re = 0.re
[PROOFSTEP]
simp [smul_re, smul_im, smul_zero]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ (r • 0).im = 0.im
[PROOFSTEP]
simp [smul_re, smul_im, smul_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ r • (x + y) = r • x + r • y
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).re = (r • x + r • y).re
[PROOFSTEP]
simp [smul_re, smul_im, smul_add]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).im = (r • x + r • y).im
[PROOFSTEP]
simp [smul_re, smul_im, smul_add]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ (r + s) • x = r • x + s • x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).re = (r • x + s • x).re
[PROOFSTEP]
simp [smul_re, smul_im, add_smul]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).im = (r • x + s • x).im
[PROOFSTEP]
simp [smul_re, smul_im, add_smul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ 0 • r = 0
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ (0 • r).re = 0.re
[PROOFSTEP]
simp [smul_re, smul_im, zero_smul]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ (0 • r).im = 0.im
[PROOFSTEP]
simp [smul_re, smul_im, zero_smul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x✝ : (fun x => ℂ) r
xr xi : ℝ
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r *
      { re := xr, im := xi } =
    { re := xr, im := xi } *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x✝ : (fun x => ℂ) r
xr xi : ℝ
⊢ (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        { re := xr, im := xi }).re =
    ({ re := xr, im := xi } *
        ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r).re
[PROOFSTEP]
simp [smul_re, smul_im, Algebra.commutes]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x✝ : (fun x => ℂ) r
xr xi : ℝ
⊢ (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        { re := xr, im := xi }).im =
    ({ re := xr, im := xi } *
        ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r).im
[PROOFSTEP]
simp [smul_re, smul_im, Algebra.commutes]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x : (fun x => ℂ) r
⊢ r • x =
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r *
      x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x : (fun x => ℂ) r
⊢ (r • x).re =
    (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        x).re
[PROOFSTEP]
simp [smul_re, smul_im, Algebra.smul_def]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x : (fun x => ℂ) r
⊢ (r • x).im =
    (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        x).im
[PROOFSTEP]
simp [smul_re, smul_im, Algebra.smul_def]
[GOAL]
R : Type u_1
S : Type u_2
r : ℝ
x : ℂ
⊢ star (r • x) = star r • star x
[PROOFSTEP]
simp only [star_def, star_trivial, real_smul, map_mul, conj_ofReal]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : ↑f I = ↑g I
⊢ f = g
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case H.mk
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : ↑f I = ↑g I
x y : ℝ
⊢ ↑f { re := x, im := y } = ↑g { re := x, im := y }
[PROOFSTEP]
simp only [mk_eq_add_mul_I, AlgHom.map_add, AlgHom.map_coe_real_complex, AlgHom.map_mul, h]
[GOAL]
R : Type u_1
S : Type u_2
z z' : ℂ
⊢ (fun z => ![z.re, z.im]) (z + z') = (fun z => ![z.re, z.im]) z + (fun z => ![z.re, z.im]) z'
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
c : ℝ
z : ℂ
⊢ AddHom.toFun
      { toFun := fun z => ![z.re, z.im],
        map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) }
      (c • z) =
    ↑(RingHom.id ℝ) c •
      AddHom.toFun
        { toFun := fun z => ![z.re, z.im],
          map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) }
        z
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
z : ℂ
⊢ (fun c => ↑(c 0) + c 1 • I)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun z => ![z.re, z.im],
                map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) },
            map_smul' :=
              (_ : ∀ (c : ℝ) (z : ℂ), ![c * z.re - 0 * z.im, c * z.im + 0 * z.re] = c • ![z.re, z.im]) }.toAddHom
        z) =
    z
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun z => ![z.re, z.im],
              map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) },
          map_smul' :=
            (_ : ∀ (c : ℝ) (z : ℂ), ![c * z.re - 0 * z.im, c * z.im + 0 * z.re] = c • ![z.re, z.im]) }.toAddHom
      ((fun c => ↑(c 0) + c 1 • I) c) =
    c
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
i : Fin 2
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun z => ![z.re, z.im],
              map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) },
          map_smul' :=
            (_ : ∀ (c : ℝ) (z : ℂ), ![c * z.re - 0 * z.im, c * z.im + 0 * z.re] = c • ![z.re, z.im]) }.toAddHom
      ((fun c => ↑(c 0) + c 1 • I) c) i =
    c i
[PROOFSTEP]
fin_cases i
[GOAL]
case h.head
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun z => ![z.re, z.im],
              map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) },
          map_smul' :=
            (_ : ∀ (c : ℝ) (z : ℂ), ![c * z.re - 0 * z.im, c * z.im + 0 * z.re] = c • ![z.re, z.im]) }.toAddHom
      ((fun c => ↑(c 0) + c 1 • I) c) { val := 0, isLt := (_ : 0 < 2) } =
    c { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp
[GOAL]
case h.tail.head
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun z => ![z.re, z.im],
              map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) },
          map_smul' :=
            (_ : ∀ (c : ℝ) (z : ℂ), ![c * z.re - 0 * z.im, c * z.im + 0 * z.re] = c • ![z.re, z.im]) }.toAddHom
      ((fun c => ↑(c 0) + c 1 • I) c) { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    c { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
i j : Fin 2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] i)) j = ↑(Finsupp.single i 1) j
[PROOFSTEP]
fin_cases i
[GOAL]
case head
R : Type u_1
S : Type u_2
j : Fin 2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) })) j =
    ↑(Finsupp.single { val := 0, isLt := (_ : 0 < 2) } 1) j
[PROOFSTEP]
fin_cases j
[GOAL]
case tail.head
R : Type u_1
S : Type u_2
j : Fin 2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) })) j =
    ↑(Finsupp.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) j
[PROOFSTEP]
fin_cases j
[GOAL]
case head.head
R : Type u_1
S : Type u_2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) })) { val := 0, isLt := (_ : 0 < 2) } =
    ↑(Finsupp.single { val := 0, isLt := (_ : 0 < 2) } 1) { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
  Fin.one_eq_zero_iff, Ne.def, not_false_iff, I_re, Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same,
  Fin.zero_eq_one_iff]
[GOAL]
case head.tail.head
R : Type u_1
S : Type u_2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }))
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑(Finsupp.single { val := 0, isLt := (_ : 0 < 2) } 1) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
  Fin.one_eq_zero_iff, Ne.def, not_false_iff, I_re, Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same,
  Fin.zero_eq_one_iff]
[GOAL]
case tail.head.head
R : Type u_1
S : Type u_2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }))
      { val := 0, isLt := (_ : 0 < 2) } =
    ↑(Finsupp.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
  Fin.one_eq_zero_iff, Ne.def, not_false_iff, I_re, Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same,
  Fin.zero_eq_one_iff]
[GOAL]
case tail.head.tail.head
R : Type u_1
S : Type u_2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }))
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑(Finsupp.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
  Fin.one_eq_zero_iff, Ne.def, not_false_iff, I_re, Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same,
  Fin.zero_eq_one_iff]
[GOAL]
R : Type u_1
S : Type u_2
⊢ finrank ℝ ℂ = 2
[PROOFSTEP]
rw [finrank_eq_card_basis basisOneI, Fintype.card_fin]
[GOAL]
R : Type u_1
S : Type u_2
⊢ Module.rank ℝ ℂ = 2
[PROOFSTEP]
simp [← finrank_eq_rank, finrank_real_complex]
[GOAL]
R : Type u_1
S : Type u_2
⊢ Cardinal.lift (Module.rank ℝ ℂ) = 2
[PROOFSTEP]
rw [← finrank_eq_rank, finrank_real_complex, Cardinal.lift_natCast, Nat.cast_ofNat]
[GOAL]
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ Cardinal.lift (Module.rank ℝ E) = Cardinal.lift (2 * Module.rank ℂ E)
[PROOFSTEP]
rw [← lift_rank_mul_lift_rank ℝ ℂ E, Complex.rank_real_complex']
[GOAL]
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ 2 * Cardinal.lift (Module.rank ℂ E) = Cardinal.lift (2 * Module.rank ℂ E)
[PROOFSTEP]
simp only [Cardinal.lift_id']
[GOAL]
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ FiniteDimensional.finrank ℝ E = 2 * FiniteDimensional.finrank ℂ E
[PROOFSTEP]
rw [← FiniteDimensional.finrank_mul_finrank ℝ ℂ E, Complex.finrank_real_complex]
[GOAL]
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Star E
inst✝¹ : Module ℂ E
inst✝ : StarModule ℂ E
r : ℝ
a : E
⊢ star (r • a) = star r • star a
[PROOFSTEP]
rw [← smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]
[GOAL]
⊢ ∀ (r : ℝ) (x : ℂ),
    AddHom.toFun { toFun := fun x => x.re, map_add' := add_re } (r • x) =
      ↑(RingHom.id ℝ) r • AddHom.toFun { toFun := fun x => x.re, map_add' := add_re } x
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (r : ℝ) (x : ℂ),
    AddHom.toFun { toFun := fun x => x.im, map_add' := add_im } (r • x) =
      ↑(RingHom.id ℝ) r • AddHom.toFun { toFun := fun x => x.im, map_add' := add_im } x
[PROOFSTEP]
simp
[GOAL]
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) = ↑Matrix.of ![![1, 0], ![0, -1]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
i j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) i j = ↑Matrix.of ![![1, 0], ![0, -1]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 0, isLt := (_ : 0 < 2) } j =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      j =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 0, isLt := (_ : 0 < 2) }
      { val := 0, isLt := (_ : 0 < 2) } =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [LinearMap.toMatrix_apply]
[GOAL]
case a.h.head.tail.head
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [LinearMap.toMatrix_apply]
[GOAL]
case a.h.tail.head.head
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 0, isLt := (_ : 0 < 2) } =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [LinearMap.toMatrix_apply]
[GOAL]
case a.h.tail.head.tail.head
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [LinearMap.toMatrix_apply]
[GOAL]
f : ℂ →ₐ[ℝ] ℂ
⊢ f = AlgHom.id ℝ ℂ ∨ f = ↑conjAe
[PROOFSTEP]
refine' (eq_or_eq_neg_of_sq_eq_sq (f I) I <| by rw [← map_pow, I_sq, map_neg, map_one]).imp _ _
[GOAL]
f : ℂ →ₐ[ℝ] ℂ
⊢ ↑f I ^ 2 = I ^ 2
[PROOFSTEP]
rw [← map_pow, I_sq, map_neg, map_one]
[GOAL]
case refine'_1
f : ℂ →ₐ[ℝ] ℂ
⊢ ↑f I = I → f = AlgHom.id ℝ ℂ
[PROOFSTEP]
refine' fun h => algHom_ext _
[GOAL]
case refine'_2
f : ℂ →ₐ[ℝ] ℂ
⊢ ↑f I = -I → f = ↑conjAe
[PROOFSTEP]
refine' fun h => algHom_ext _
[GOAL]
case refine'_1
f : ℂ →ₐ[ℝ] ℂ
h : ↑f I = I
⊢ ↑f I = ↑(AlgHom.id ℝ ℂ) I
case refine'_2 f : ℂ →ₐ[ℝ] ℂ h : ↑f I = -I ⊢ ↑f I = ↑↑conjAe I
[PROOFSTEP]
exacts [h, conj_I.symm ▸ h]
[GOAL]
src✝ : ℂ ≃ ℝ × ℝ := equivRealProd
⊢ ∀ (x y : ℂ),
    Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (x + y) =
      Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          x +
        Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          y
[PROOFSTEP]
simp
[GOAL]
src✝ : ℂ ≃+ ℝ × ℝ := equivRealProdAddHom
r : ℝ
c : ℂ
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : ℂ), Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (r • c) =
    ↑(RingHom.id ℝ) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : ℂ), Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        c
[PROOFSTEP]
simp [equivRealProdAddHom, (Prod.smul_def), smul_eq_mul]
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
⊢ ↑(algebraMap ℝ A) 1 + 0 • I' = 1
[PROOFSTEP]
rw [RingHom.map_one, zero_smul, add_zero]
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
⊢ ↑(algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    (↑(algebraMap ℝ A) x₁ + y₁ • I') * (↑(algebraMap ℝ A) x₂ + y₂ • I')
[PROOFSTEP]
rw [add_mul, mul_add, mul_add, add_comm _ (y₁ • I' * y₂ • I'), add_add_add_comm]
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
⊢ ↑(algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    ↑(algebraMap ℝ A) x₁ * ↑(algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I' +
      (↑(algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * ↑(algebraMap ℝ A) x₂)
[PROOFSTEP]
congr 1
  -- equate "real" and "imaginary" parts
[GOAL]
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
⊢ ↑(algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = ↑(algebraMap ℝ A) x₁ * ↑(algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I'
[PROOFSTEP]
let inst : SMulCommClass ℝ A A := by
  infer_instance
    -- porting note: added
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
⊢ SMulCommClass ℝ A A
[PROOFSTEP]
infer_instance
  -- porting note: added
[GOAL]
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
inst : SMulCommClass ℝ A A := inferInstance
⊢ ↑(algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = ↑(algebraMap ℝ A) x₁ * ↑(algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I'
[PROOFSTEP]
rw [smul_mul_smul, hf, smul_neg, ← Algebra.algebraMap_eq_smul_one, ← sub_eq_add_neg, ← RingHom.map_mul, ←
  RingHom.map_sub]
[GOAL]
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
⊢ (x₁ * y₂ + y₁ * x₂) • I' = ↑(algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * ↑(algebraMap ℝ A) x₂
[PROOFSTEP]
rw [Algebra.smul_def, Algebra.smul_def, Algebra.smul_def, ← Algebra.right_comm _ x₂, ← mul_assoc, ← add_mul, ←
  RingHom.map_mul, ← RingHom.map_mul, ← RingHom.map_add]
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ ↑(liftAux I' hI') I = I'
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
F : ℂ →ₐ[ℝ] A
⊢ ↑F I * ↑F I = -1
[PROOFSTEP]
rw [← F.map_mul, I_mul_I, AlgHom.map_neg, AlgHom.map_one]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : { x // x ∈ skewAdjoint A }
⊢ -I • ↑a ∈ selfAdjoint A
[PROOFSTEP]
simp only [neg_smul, neg_mem_iff, selfAdjoint.mem_iff, star_smul, star_def, conj_I, star_val_eq, smul_neg, neg_neg]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a b : { x // x ∈ skewAdjoint A }
⊢ (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b) =
    (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
      (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b
[PROOFSTEP]
ext
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a b : { x // x ∈ skewAdjoint A }
⊢ ↑((fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b)) =
    ↑((fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
        (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b)
[PROOFSTEP]
simp only [AddSubgroup.coe_add, smul_add, AddMemClass.mk_add_mk]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ℝ
b : { x // x ∈ skewAdjoint A }
⊢ AddHom.toFun
      { toFun := fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) },
        map_add' :=
          (_ :
            ∀ (a b : { x // x ∈ skewAdjoint A }),
              (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b) =
                (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
                  (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b) }
      (a • b) =
    ↑(RingHom.id ℝ) a •
      AddHom.toFun
        { toFun := fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) },
          map_add' :=
            (_ :
              ∀ (a b : { x // x ∈ skewAdjoint A }),
                (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b) =
                  (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
                    (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b) }
        b
[PROOFSTEP]
ext
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ℝ
b : { x // x ∈ skewAdjoint A }
⊢ ↑(AddHom.toFun
        { toFun := fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) },
          map_add' :=
            (_ :
              ∀ (a b : { x // x ∈ skewAdjoint A }),
                (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b) =
                  (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
                    (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b) }
        (a • b)) =
    ↑(↑(RingHom.id ℝ) a •
        AddHom.toFun
          { toFun := fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) },
            map_add' :=
              (_ :
                ∀ (a b : { x // x ∈ skewAdjoint A }),
                  (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b) =
                    (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
                      (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b) }
          b)
[PROOFSTEP]
simp only [neg_smul, skewAdjoint.val_smul, AddSubgroup.coe_mk, RingHom.id_apply, selfAdjoint.val_smul, smul_neg,
  neg_inj]
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ℝ
b : { x // x ∈ skewAdjoint A }
⊢ I • a • ↑b = a • I • ↑b
[PROOFSTEP]
rw [smul_comm]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : { x // x ∈ skewAdjoint A }
⊢ I • ↑(↑negISMul a) = ↑a
[PROOFSTEP]
simp only [smul_smul, skewAdjoint.negISMul_apply_coe, neg_smul, smul_neg, I_mul_I, one_smul, neg_neg]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℜ a) = 2⁻¹ • (a + star a)
[PROOFSTEP]
unfold realPart
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑(selfAdjointPart ℝ) a) = 2⁻¹ • (a + star a)
[PROOFSTEP]
simp only [selfAdjointPart_apply_coe, invOf_eq_inv]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℑ a) = -I • 2⁻¹ • (a - star a)
[PROOFSTEP]
unfold imaginaryPart
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑(LinearMap.comp skewAdjoint.negISMul (skewAdjointPart ℝ)) a) = -I • 2⁻¹ • (a - star a)
[PROOFSTEP]
simp only [LinearMap.coe_comp, Function.comp_apply, skewAdjoint.negISMul_apply_coe, skewAdjointPart_apply_coe,
  invOf_eq_inv, neg_smul]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℜ a) + I • ↑(↑ℑ a) = a
[PROOFSTEP]
simpa only [smul_smul, realPart_apply_coe, imaginaryPart_apply_coe, neg_smul, I_mul_I, one_smul, neg_sub,
  add_add_sub_cancel, smul_sub, smul_add, neg_sub_neg, invOf_eq_inv] using invOf_two_smul_add_invOf_two_smul ℝ a
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑ℜ (I • a) = -↑ℑ a
[PROOFSTEP]
ext
  -- Porting note: was
    -- simp [smul_comm I, smul_sub, sub_eq_add_neg, add_comm]
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℜ (I • a)) = ↑(-↑ℑ a)
[PROOFSTEP]
rw [realPart_apply_coe, AddSubgroupClass.coe_neg, imaginaryPart_apply_coe, neg_smul, neg_neg, smul_comm I, star_smul,
  star_def, conj_I, smul_sub, neg_smul, sub_eq_add_neg]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑ℑ (I • a) = ↑ℜ a
[PROOFSTEP]
ext
  -- Porting note: was
    -- simp [smul_comm I, smul_smul I]
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℑ (I • a)) = ↑(↑ℜ a)
[PROOFSTEP]
rw [realPart_apply_coe, imaginaryPart_apply_coe, smul_comm]
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ 2⁻¹ • -I • (I • a - star (I • a)) = 2⁻¹ • (a + star a)
[PROOFSTEP]
simp [← smul_assoc]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ↑ℜ (z • a) = z.re • ↑ℜ a - z.im • ↑ℑ a
[PROOFSTEP]
conv_lhs => rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℜ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℜ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℜ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ↑ℜ ((↑z.re + ↑z.im * I) • a) = z.re • ↑ℜ a - z.im • ↑ℑ a
[PROOFSTEP]
simp [-re_add_im, add_smul, ← smul_smul, sub_eq_add_neg]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ↑ℑ (z • a) = z.re • ↑ℑ a + z.im • ↑ℜ a
[PROOFSTEP]
conv_lhs => rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℑ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℑ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℑ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ↑ℑ ((↑z.re + ↑z.im * I) • a) = z.re • ↑ℑ a + z.im • ↑ℜ a
[PROOFSTEP]
simp [-re_add_im, add_smul, ← smul_smul]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq α
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) → i ∈ s
[PROOFSTEP]
simp (config := { contextual := true }) [mem_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq β
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) → i ∈ t
[PROOFSTEP]
simp (config := { contextual := true }) [mem_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq α
ht : Finset.Nonempty t
⊢ image Prod.fst (s ×ˢ t) = s
[PROOFSTEP]
ext i
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq α
ht : Finset.Nonempty t
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s
[PROOFSTEP]
simp [mem_image, ht.bex]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq β
ht : Finset.Nonempty s
⊢ image Prod.snd (s ×ˢ t) = t
[PROOFSTEP]
ext i
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq β
ht : Finset.Nonempty s
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) ↔ i ∈ t
[PROOFSTEP]
simp [mem_image, ht.bex]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
⊢ ↑(map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (t ×ˢ s)) = ↑(s ×ˢ t)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
⊢ (fun a => ↑{ toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } a) '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
[PROOFSTEP]
exact Set.image_swap_prod _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ ↑(image Prod.swap (t ×ˢ s)) = ↑(s ×ˢ t)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ Prod.swap '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
[PROOFSTEP]
exact Set.image_swap_prod _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
x✝ : α × β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ↔ (x, y) ∈ Finset.biUnion s fun a => image (fun b => (a, b)) t
[PROOFSTEP]
simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk.inj_iff, and_left_comm, exists_and_left,
  exists_eq_right, exists_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
x✝ : α × β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ↔ (x, y) ∈ Finset.biUnion t fun b => image (fun a => (a, b)) s
[PROOFSTEP]
simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk.inj_iff, and_left_comm, exists_and_left,
  exists_eq_right, exists_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ Finset.biUnion (s ×ˢ t) f = Finset.biUnion s fun a => Finset.biUnion t fun b => f (a, b)
[PROOFSTEP]
classical simp_rw [product_eq_biUnion, biUnion_biUnion, image_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ Finset.biUnion (s ×ˢ t) f = Finset.biUnion s fun a => Finset.biUnion t fun b => f (a, b)
[PROOFSTEP]
simp_rw [product_eq_biUnion, biUnion_biUnion, image_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) = filter p s ×ˢ filter q t
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a✝ : α
b✝ : β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a, b) ∈ filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ↔ (a, b) ∈ filter p s ×ˢ filter q t
[PROOFSTEP]
simp [mem_filter, mem_product, decide_eq_true_eq, and_comm, and_left_comm, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
p : α → Prop
inst✝ : DecidablePred p
⊢ filter (fun x => p x.fst) (s ×ˢ t) = filter p s ×ˢ t
[PROOFSTEP]
simpa using filter_product p fun _ => true
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
q : β → Prop
inst✝ : DecidablePred q
⊢ filter (fun x => q x.snd) (s ×ˢ t) = s ×ˢ filter q t
[PROOFSTEP]
simpa using filter_product (fun _ : α => true) q
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card (filter (fun x => p x.fst = q x.snd) (s ×ˢ t)) =
    card (filter p s) * card (filter q t) + card (filter (fun x => ¬p x) s) * card (filter (fun x => ¬q x) t)
[PROOFSTEP]
classical
rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_eq]
· apply congr_arg
  ext ⟨a, b⟩
  simp only [filter_union_right, mem_filter, mem_product]
  constructor <;> intro h <;> use h.1
  · simp only [h.2, Function.comp_apply, Decidable.em, and_self]
  · revert h
    simp only [Function.comp_apply, and_imp]
    rintro _ _ (_ | _) <;> simp [*]
· apply Finset.disjoint_filter_filter'
  exact (disjoint_compl_right.inf_left _).inf_right _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card (filter (fun x => p x.fst = q x.snd) (s ×ˢ t)) =
    card (filter p s) * card (filter q t) + card (filter (fun x => ¬p x) s) * card (filter (fun x => ¬q x) t)
[PROOFSTEP]
rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card (filter (fun x => p x.fst = q x.snd) (s ×ˢ t)) =
    card (filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ∪ filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t))
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun x => p x.fst = q x.snd) (s ×ˢ t) =
    filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ∪ filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t)
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case h.a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a, b) ∈ filter (fun x => p x.fst = q x.snd) (s ×ˢ t) ↔
    (a, b) ∈ filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ∪ filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t)
[PROOFSTEP]
simp only [filter_union_right, mem_filter, mem_product]
[GOAL]
case h.a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a ∈ s ∧ b ∈ t) ∧ p a = q b ↔ (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
[PROOFSTEP]
constructor
[GOAL]
case h.a.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a ∈ s ∧ b ∈ t) ∧ p a = q b → (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
[PROOFSTEP]
intro h
[GOAL]
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b) → (a ∈ s ∧ b ∈ t) ∧ p a = q b
[PROOFSTEP]
intro h
[GOAL]
case h.a.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ p a = q b
⊢ (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
[PROOFSTEP]
use h.1
[GOAL]
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
⊢ (a ∈ s ∧ b ∈ t) ∧ p a = q b
[PROOFSTEP]
use h.1
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ p a = q b
⊢ p a ∧ q b ∨ ¬p a ∧ ¬q b
[PROOFSTEP]
simp only [h.2, Function.comp_apply, Decidable.em, and_self]
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
⊢ p a = q b
[PROOFSTEP]
revert h
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b) → p a = q b
[PROOFSTEP]
simp only [Function.comp_apply, and_imp]
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ a ∈ s → b ∈ t → p a ∧ q b ∨ ¬p a ∧ ¬q b → p a = q b
[PROOFSTEP]
rintro _ _ (_ | _)
[GOAL]
case right.inl
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝² : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
a✝¹ : a ∈ s
a✝ : b ∈ t
h✝ : p a ∧ q b
⊢ p a = q b
[PROOFSTEP]
simp [*]
[GOAL]
case right.inr
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a✝² : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
a✝¹ : a ∈ s
a✝ : b ∈ t
h✝ : ¬p a ∧ ¬q b
⊢ p a = q b
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ _root_.Disjoint (filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t)) (filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t))
[PROOFSTEP]
apply Finset.disjoint_filter_filter'
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ _root_.Disjoint (fun x => p x.fst ∧ q x.snd) fun x => ¬p x.fst ∧ ¬q x.snd
[PROOFSTEP]
exact (disjoint_compl_right.inf_left _).inf_right _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, nonempty_product, not_and_or, not_nonempty_iff_eq_empty, not_nonempty_iff_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a✝ : α
b : β
a : α
⊢ {a} ×ˢ t = map { toFun := Prod.mk a, inj' := (_ : Function.Injective (Prod.mk a)) } t
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a✝ : α
b : β
a x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := (_ : Function.Injective (Prod.mk a)) } t
[PROOFSTEP]
simp [and_left_comm, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b✝ b : β
⊢ s ×ˢ {b} = map { toFun := fun i => (i, b), inj' := (_ : Function.Injective fun a => (a, b)) } s
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b✝ b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ map { toFun := fun i => (i, b), inj' := (_ : Function.Injective fun a => (a, b)) } s
[PROOFSTEP]
simp [and_left_comm, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a✝ : α
b✝ : β
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}
[PROOFSTEP]
simp only [product_singleton, Function.Embedding.coeFn_mk, map_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ (s ∪ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∪ s' ×ˢ t
[PROOFSTEP]
simp only [or_and_right, mem_union, mem_product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t ∪ t') ↔ (x, y) ∈ s ×ˢ t ∪ s ×ˢ t'
[PROOFSTEP]
simp only [and_or_left, mem_union, mem_product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ (s ∩ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∩ s' ×ˢ t
[PROOFSTEP]
simp only [← and_and_right, mem_inter, mem_product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t ∩ t') ↔ (x, y) ∈ s ×ˢ t ∩ s ×ˢ t'
[PROOFSTEP]
simp only [← and_and_left, mem_inter, mem_product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ∩ s' ×ˢ t' ↔ (x, y) ∈ (s ∩ s') ×ˢ (t ∩ t')
[PROOFSTEP]
simp only [and_assoc, and_left_comm, mem_inter, mem_product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
⊢ _root_.Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ _root_.Disjoint s s' ∨ _root_.Disjoint t t'
[PROOFSTEP]
simp_rw [← disjoint_coe, coe_product, Set.disjoint_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ x ∈ diag s ↔ x.fst ∈ s ∧ x.fst = x.snd
[PROOFSTEP]
simp (config := { contextual := true }) [diag]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ x ∈ offDiag s ↔ x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd
[PROOFSTEP]
simp [offDiag, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ card (diag s) = card s
[PROOFSTEP]
suffices diag s = s.image fun a => (a, a) by
  rw [this]
  apply card_image_of_injOn
  exact fun x1 _ x2 _ h3 => (Prod.mk.inj h3).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ card (diag s) = card s
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ card (image (fun a => (a, a)) s) = card s
[PROOFSTEP]
apply card_image_of_injOn
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ Set.InjOn (fun a => (a, a)) ↑s
[PROOFSTEP]
exact fun x1 _ x2 _ h3 => (Prod.mk.inj h3).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ diag s = image (fun a => (a, a)) s
[PROOFSTEP]
ext ⟨a₁, a₂⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ diag s ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s
[PROOFSTEP]
rw [mem_diag]
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd → (a₁, a₂) ∈ image (fun a => (a, a)) s
[PROOFSTEP]
intro h
[GOAL]
case a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ image (fun a => (a, a)) s → (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
[PROOFSTEP]
intro h
[GOAL]
case a.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
⊢ (a₁, a₂) ∈ image (fun a => (a, a)) s
[PROOFSTEP]
rw [Finset.mem_image] at *
[GOAL]
case a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂) ∈ image (fun a => (a, a)) s
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
[PROOFSTEP]
rw [Finset.mem_image] at *
[GOAL]
case a.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
⊢ ∃ a, a ∈ s ∧ (a, a) = (a₁, a₂)
[PROOFSTEP]
use a₁
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
⊢ a₁ ∈ s ∧ (a₁, a₁) = (a₁, a₂)
[PROOFSTEP]
simpa using h
[GOAL]
case a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : ∃ a, a ∈ s ∧ (a, a) = (a₁, a₂)
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
[PROOFSTEP]
rcases h with ⟨a, h1, h2⟩
[GOAL]
case a.mk.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
[PROOFSTEP]
have h := Prod.mk.inj h2
[GOAL]
case a.mk.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
[PROOFSTEP]
rw [← h.1, ← h.2]
[GOAL]
case a.mk.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a, a).fst ∈ s ∧ (a, a).fst = (a, a).snd
[PROOFSTEP]
use h1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ card (diag s) + card (offDiag s) = card s * card s
[PROOFSTEP]
rw [← card_product, diag, offDiag]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ card (filter (fun a => a.fst = a.snd) (s ×ˢ s)) + card (filter (fun a => a.fst ≠ a.snd) (s ×ˢ s)) = card (s ×ˢ s)
[PROOFSTEP]
conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| card (s ×ˢ s)
[PROOFSTEP]
rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| card (s ×ˢ s)
[PROOFSTEP]
rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| card (s ×ˢ s)
[PROOFSTEP]
rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card (diag s) + card (offDiag s) = card s * card s
⊢ card (offDiag s) = card s * card s - card s
[PROOFSTEP]
conv_rhs => {rw [← s.diag_card]}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card (diag s) + card (offDiag s) = card s * card s
| card s * card s - card s
[PROOFSTEP]
{rw [← s.diag_card]}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card (diag s) + card (offDiag s) = card s * card s
| card s * card s - card s
[PROOFSTEP]
{rw [← s.diag_card]}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card (diag s) + card (offDiag s) = card s * card s
| card s * card s - card s
[PROOFSTEP]
rw [← s.diag_card]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card (diag s) + card (offDiag s) = card s * card s
⊢ card (offDiag s) = card (diag s) * card (diag s) - card (diag s)
[PROOFSTEP]
simp only [diag_card] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card s + card (offDiag s) = card s * card s
⊢ card (offDiag s) = card s * card s - card s
[PROOFSTEP]
rw [tsub_eq_of_eq_add_rev]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card s + card (offDiag s) = card s * card s
⊢ card s * card s = card s + card (offDiag s)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ diag s ∪ offDiag s = s ×ˢ s
[PROOFSTEP]
conv_rhs => rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| s ×ˢ s
[PROOFSTEP]
rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| s ×ˢ s
[PROOFSTEP]
rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| s ×ˢ s
[PROOFSTEP]
rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ s ×ˢ s \ diag s = offDiag s
[PROOFSTEP]
rw [← diag_union_offDiag, union_comm, union_sdiff_self, sdiff_eq_self_of_disjoint (disjoint_diag_offDiag _).symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ s ×ˢ s \ offDiag s = diag s
[PROOFSTEP]
rw [← diag_union_offDiag, union_sdiff_self, sdiff_eq_self_of_disjoint (disjoint_diag_offDiag _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x✝ x : α × α
⊢ x ∈ diag (s ∩ t) ↔ x ∈ diag s ∩ diag t
[PROOFSTEP]
simpa only [mem_diag, mem_inter] using and_and_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ ↑(offDiag (s ∩ t)) = ↑(offDiag s ∩ offDiag t)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ Set.offDiag (↑s ∩ ↑t) = Set.offDiag ↑s ∩ Set.offDiag ↑t
[PROOFSTEP]
exact Set.offDiag_inter _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ diag (s ∪ t) = diag s ∪ diag t
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
i j : α
⊢ (i, j) ∈ diag (s ∪ t) ↔ (i, j) ∈ diag s ∪ diag t
[PROOFSTEP]
simp only [mem_diag, mem_union, or_and_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
h : _root_.Disjoint s t
⊢ ↑(offDiag (s ∪ t)) = ↑(offDiag s ∪ offDiag t ∪ s ×ˢ t ∪ t ×ˢ s)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
h : _root_.Disjoint s t
⊢ Set.offDiag (↑s ∪ ↑t) = Set.offDiag ↑s ∪ Set.offDiag ↑t ∪ ↑s ×ˢ ↑t ∪ ↑t ×ˢ ↑s
[PROOFSTEP]
exact Set.offDiag_union (disjoint_coe.2 h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
⊢ offDiag {a} = ∅
[PROOFSTEP]
simp [← Finset.card_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
⊢ diag {a} = {(a, a)}
[PROOFSTEP]
rw [← product_sdiff_offDiag, offDiag_singleton, sdiff_empty, singleton_product_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
⊢ diag (insert a s) = insert (a, a) (diag s)
[PROOFSTEP]
rw [insert_eq, insert_eq, diag_union, diag_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
has : ¬a ∈ s
⊢ offDiag (insert a s) = offDiag s ∪ {a} ×ˢ s ∪ s ×ˢ {a}
[PROOFSTEP]
rw [insert_eq, union_comm, offDiag_union (disjoint_singleton_right.2 has), offDiag_singleton, union_empty,
  union_right_comm]


[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ #(AddMonoidAlgebra R ℕ) = max #R ℵ₀
[PROOFSTEP]
rw [AddMonoidAlgebra, mk_finsupp_lift_of_infinite, lift_uzero, max_comm]
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ max (#R) (lift #ℕ) = max #R ℵ₀
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Semiring R
⊢ #R[X] ≤ max #R ℵ₀
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u
inst✝ : Semiring R
h✝ : Subsingleton R
⊢ #R[X] ≤ max #R ℵ₀
[PROOFSTEP]
exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
[GOAL]
case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀
[PROOFSTEP]
exact cardinal_mk_eq_max.le


[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
⊢ ↑i 0 = ↑i b ^ N * eval (↑i a * bi) (Polynomial.map i 0)
[PROOFSTEP]
simp only [eval_zero, RingHom.map_zero, mul_zero, Polynomial.map_zero]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ DenomsClearable a b N (↑C r * X ^ n) i
[PROOFSTEP]
refine' ⟨r * a ^ n * b ^ (N - n), bi, bu, _⟩
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i (r * a ^ n * b ^ (N - n)) = ↑i b ^ N * eval (↑i a * bi) (Polynomial.map i (↑C r * X ^ n))
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, eval_mul, eval_pow, eval_C]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i (r * a ^ n * b ^ (N - n)) = ↑i b ^ N * (↑i r * eval (↑i a * bi) X ^ n)
[PROOFSTEP]
rw [RingHom.map_mul, RingHom.map_mul, RingHom.map_pow, RingHom.map_pow, eval_X, mul_comm]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n) * (↑i r * ↑i a ^ n) = ↑i b ^ N * (↑i r * (↑i a * bi) ^ n)
[PROOFSTEP]
rw [← tsub_add_cancel_of_le nN]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n + n - n) * (↑i r * ↑i a ^ n) = ↑i b ^ (N - n + n) * (↑i r * (↑i a * bi) ^ n)
[PROOFSTEP]
conv_lhs => rw [← mul_one (i a), ← bu]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
| ↑i b ^ (N - n + n - n) * (↑i r * ↑i a ^ n)
[PROOFSTEP]
rw [← mul_one (i a), ← bu]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
| ↑i b ^ (N - n + n - n) * (↑i r * ↑i a ^ n)
[PROOFSTEP]
rw [← mul_one (i a), ← bu]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
| ↑i b ^ (N - n + n - n) * (↑i r * ↑i a ^ n)
[PROOFSTEP]
rw [← mul_one (i a), ← bu]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n + n - n) * (↑i r * (↑i a * (bi * ↑i b)) ^ n) = ↑i b ^ (N - n + n) * (↑i r * (↑i a * bi) ^ n)
[PROOFSTEP]
simp [mul_assoc, mul_comm, mul_left_comm, pow_add, mul_pow]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
bi : K
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * ↑i b = 1
Hf : ↑i Df = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * ↑i b = 1
Hg : ↑i Dg = ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g)
⊢ ↑i (Df + Dg) = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i (f + g))
[PROOFSTEP]
rw [RingHom.map_add, Polynomial.map_add, eval_add, mul_add, Hf, Hg]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
bi : K
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * ↑i b = 1
Hf : ↑i Df = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * ↑i b = 1
Hg : ↑i Dg = ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g)
⊢ ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f) + ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g) =
    ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f) + ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i g)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.e_a.e_a
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
bi : K
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * ↑i b = 1
Hf : ↑i Df = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * ↑i b = 1
Hg : ↑i Dg = ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g)
⊢ bg = bf
[PROOFSTEP]
refine' @inv_unique K _ (i b) bg bf _ _
[GOAL]
case e_a.e_a.e_a.e_a.refine'_1
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
bi : K
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * ↑i b = 1
Hf : ↑i Df = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * ↑i b = 1
Hg : ↑i Dg = ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g)
⊢ ↑i b * bg = 1
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
case e_a.e_a.e_a.e_a.refine'_2
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
bi : K
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * ↑i b = 1
Hf : ↑i Df = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * ↑i b = 1
Hg : ↑i Dg = ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g)
⊢ ↑i b * bf = 1
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ 1 ≤ ↑b ^ natDegree f * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
[PROOFSTEP]
obtain ⟨ev, bi, bu, hF⟩ :=
  denomsClearable_natDegree (b := b) (algebraMap ℤ K) f a
    (by
      rw [eq_intCast, one_div_mul_cancel]
      rw [Int.cast_ne_zero]
      exact b0.ne.symm)
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ ?m.165182 * ↑(algebraMap ℤ K) b = 1
[PROOFSTEP]
rw [eq_intCast, one_div_mul_cancel]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ ↑b ≠ 0
[PROOFSTEP]
rw [Int.cast_ne_zero]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ b ≠ 0
[PROOFSTEP]
exact b0.ne.symm
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
⊢ 1 ≤ ↑b ^ natDegree f * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
[PROOFSTEP]
obtain Fa := _root_.congr_arg abs hF
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |↑(algebraMap ℤ K) ev| =
    |↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ natDegree f * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
[PROOFSTEP]
rw [eq_one_div_of_mul_eq_one_left bu, eq_intCast, eq_intCast, abs_mul] at Fa
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = |↑b ^ natDegree f| * |eval (↑(algebraMap ℤ K) a * (1 / ↑b)) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ natDegree f * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
[PROOFSTEP]
rw [abs_of_pos (pow_pos (Int.cast_pos.mpr b0) _ : 0 < (b : K) ^ _), one_div, eq_intCast] at Fa
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ natDegree f * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
[PROOFSTEP]
rw [div_eq_mul_inv, ← Fa, ← Int.cast_abs, ← Int.cast_one, Int.cast_le]
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ |ev|
[PROOFSTEP]
refine' Int.le_of_lt_add_one ((lt_add_iff_pos_left 1).mpr (abs_pos.mpr fun F0 => fab _))
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
[PROOFSTEP]
rw [eq_one_div_of_mul_eq_one_left bu, F0, one_div, eq_intCast, Int.cast_zero, zero_eq_mul] at hF
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) b ^ natDegree f = 0 ∨
    eval (↑(algebraMap ℤ K) a * (↑(algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
[PROOFSTEP]
cases' hF with hF hF
[GOAL]
case intro.intro.intro.inl
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF : ↑(algebraMap ℤ K) b ^ natDegree f = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
[PROOFSTEP]
exact (not_le.mpr b0 (le_of_eq (Int.cast_eq_zero.mp (pow_eq_zero hF)))).elim
[GOAL]
case intro.intro.intro.inr
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF : eval (↑(algebraMap ℤ K) a * (↑(algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
[PROOFSTEP]
rwa [div_eq_mul_inv]