internlm/Lean-Github huggingface dataset:
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X : Set α
⊢ X ⊆ (M.matroidOnUniv hM).E
Tactic:
simp [hM]
Proof state after:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X : Set α
⊢ X ⊆ (M.indepMatroidOnUniv hM).E
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X ⊆ M.cl X
Tactic:
simp_rw [← hI.cl_eq_cl, subset_def, hI.indep.mem_cl_iff']
Proof state after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ (x : α), x ∈ (M.matroidOnUniv hM).E ∧ ((M.matroidOnUniv hM).Indep (insert x I) → x ∈ I) → x ∈ M.cl X
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ (x : α), x ∈ (M.matroidOnUniv hM).E ∧ ((M.matroidOnUniv hM).Indep (insert x I) → x ∈ I) → x ∈ M.cl X
Tactic:
simp [M.clIndep_iff]
Proof state after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ (M.indepMatroidOnUniv hM).E, ((M.indepMatroidOnUniv hM).Indep (insert x I) → x ∈ I) → x ∈ M.cl X
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ (M.indepMatroidOnUniv hM).E, ((M.indepMatroidOnUniv hM).Indep (insert x I) → x ∈ I) → x ∈ M.cl X
Tactic:
refine fun e h ↦ by_contra fun heX ↦ ?_
Proof state after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
⊢ False
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
⊢ False
Tactic:
have heI : e ∉ I := not_mem_subset (hI.subset.trans (M.subset_cl_self X (by simp [hM]))) heX
Proof state after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
heI : e ∉ I
⊢ False
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
heI : e ∉ I
⊢ False
Tactic:
have heI' : e ∉ M.cl I := not_mem_subset (M.cl_subset_cl hI.subset) heX
Proof state after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
heI : e ∉ I
heI' : e ∉ M.cl I
⊢ False
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
heI : e ∉ I
heI' : e ∉ M.cl I
⊢ False
Tactic:
obtain ⟨a, haI, ha⟩ := h
Proof state after:
no goals
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
⊢ X ⊆ M.E
Tactic:
simp [hM]
Proof state after:
no goals
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ M.cl X ⊆ (M.matroidOnUniv hM).cl X
Tactic:
simp_rw [← hI.cl_eq_cl, subset_def, hI.indep.mem_cl_iff']
Proof state after:
case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ M.cl X, x ∈ (M.matroidOnUniv hM).E ∧ ((M.matroidOnUniv hM).Indep (insert x I) → x ∈ I)
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ M.cl X, x ∈ (M.matroidOnUniv hM).E ∧ ((M.matroidOnUniv hM).Indep (insert x I) → x ∈ I)
Tactic:
simp only [matroidOnUniv_E, mem_univ, matroidOnUniv_Indep, true_and]
Proof state after:
case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ M.cl X, x ∈ (M.indepMatroidOnUniv hM).E ∧ ((M.indepMatroidOnUniv hM).Indep (insert x I) → x ∈ I)
Theorem: Set.image_val_image_val_eq
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Set α
x : Set ↑s
⊢ ↑((fun x => ⟨f ↑x, ⋯⟩) '' x) = f '' ↑x
Tactic:
aesop
Proof state after:
no goals
Theorem: Set.Subset.eq_image_val
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
s x : Set α
hsx : x ⊆ s
⊢ x = ↑(s ↓∩ x)
Tactic:
simpa
Proof state after:
no goals
Theorem: Set.Subset.image_val_preimage_val_eq
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
s x : Set α
hsx : x ⊆ s
⊢ ↑(s ↓∩ x) = x
Tactic:
simpa
Proof state after:
no goals
Theorem: Polynomial.modByMonic_eq_zero_iff_quotient_eq_zero
Proof state before:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ p.modByMonic q = 0 ↔ (Ideal.Quotient.mk (Ideal.span {q})) p = 0
Tactic:
rw [Polynomial.modByMonic_eq_zero_iff_dvd hq, Ideal.Quotient.eq_zero_iff_dvd]
Proof state after:
no goals
Theorem: Polynomial.quotient_singleton_eq
Proof state before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
⊢ (Ideal.Quotient.mk (Ideal.span {p})) p = 0
Tactic:
rw [Ideal.Quotient.eq_zero_iff_dvd]
Proof state after:
no goals
Theorem: RingHom.list_map_sum
Proof state before:
A : Type v
B : Type w
inst✝¹ : Semiring A
inst✝ : Semiring B
φ : A →+* B
ι : Type u_1
f : ι → A
s : List ι
⊢ φ (List.map (fun x => f x) s).sum = (List.map (fun x => φ (f x)) s).sum
Tactic:
induction s with
| nil =>
  simp
| cons x xs ih =>
  simp [ih]
Proof state after:
no goals
Theorem: RingHom.list_map_sum
Proof state before:
case nil
A : Type v
B : Type w
inst✝¹ : Semiring A
inst✝ : Semiring B
φ : A →+* B
ι : Type u_1
f : ι → A
⊢ φ (List.map (fun x => f x) []).sum = (List.map (fun x => φ (f x)) []).sum
Tactic:
simp
Proof state after:
no goals
Theorem: RingHom.list_map_sum
Proof state before:
case cons
A : Type v
B : Type w
inst✝¹ : Semiring A
inst✝ : Semiring B
φ : A →+* B
ι : Type u_1
f : ι → A
x : ι
xs : List ι
ih : φ (List.map (fun x => f x) xs).sum = (List.map (fun x => φ (f x)) xs).sum
⊢ φ (List.map (fun x => f x) (x :: xs)).sum = (List.map (fun x => φ (f x)) (x :: xs)).sum
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: Lipmaa.Vars.finsupp_eq_ext
Proof state before:
f g : Vars →₀ ℕ
⊢ f = g ↔ f y = g y
Tactic:
rw [DFunLike.ext_iff]
Proof state after:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f y = g y
Theorem: Lipmaa.Vars.finsupp_eq_ext
Proof state before:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f y = g y
Tactic:
constructor
Proof state after:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f y = g y

case mpr
f g : Vars →₀ ℕ
⊢ f y = g y → ∀ (x : Vars), f x = g x
Theorem: Lipmaa.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f y = g y
Tactic:
intro h
Proof state after:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f y = g y
Theorem: Lipmaa.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f y = g y
Tactic:
simp_rw [h]
Proof state after:
no goals
Theorem: Lipmaa.Vars.finsupp_eq_ext
Proof state before:
case mpr
f g : Vars →₀ ℕ
⊢ f y = g y → ∀ (x : Vars), f x = g x
Tactic:
intro h x
Proof state after:
case mpr
f g : Vars →₀ ℕ
h : f y = g y
x : Vars
⊢ f x = g x
Theorem: Lipmaa.Vars.finsupp_eq_ext
Proof state before:
case mpr
f g : Vars →₀ ℕ
h : f y = g y
x : Vars
⊢ f x = g x
Tactic:
cases x <;> tauto
Proof state after:
no goals
Theorem: GGPR.Vars.finsupp_eq_ext
Proof state before:
f g : Vars →₀ ℕ
⊢ f = g ↔ f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ
Tactic:
rw [DFunLike.ext_iff]
Proof state after:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ
Theorem: GGPR.Vars.finsupp_eq_ext
Proof state before:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ
Tactic:
constructor
Proof state after:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ

case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ → ∀ (x : Vars), f x = g x
Theorem: GGPR.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ
Tactic:
intro h
Proof state after:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ
Theorem: GGPR.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ
Tactic:
simp_rw [h]
Proof state after:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ True ∧ True ∧ True ∧ True ∧ True
Theorem: GGPR.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ True ∧ True ∧ True ∧ True ∧ True
Tactic:
simp only [and_self]
Proof state after:
no goals
Theorem: GGPR.Vars.finsupp_eq_ext
Proof state before:
case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ → ∀ (x : Vars), f x = g x
Tactic:
intro h x
Proof state after:
case mpr
f g : Vars →₀ ℕ
h : f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ
x : Vars
⊢ f x = g x
Theorem: GGPR.Vars.finsupp_eq_ext
Proof state before:
case mpr
f g : Vars →₀ ℕ
h : f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ
x : Vars
⊢ f x = g x
Tactic:
cases x <;> tauto
Proof state after:
no goals
Theorem: GGPR.soundness
Proof state before:
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
⊢ AGMProofSystemInstantiation.soundness F GGPR ((Fin n_wit → F) × (Fin m → F))
    (fun stmt wit =>
      let t := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i));
      ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
                (List.map (fun i => Polynomial.C (wit.1 i) * v_wit i) (List.finRange n_wit)).sum) *
              (w_0 + (List.map (fun i => Polynomial.C (wit.2 i) * w_wit i) (List.finRange m)).sum)).modByMonic
          t =
        0)
    fun prover =>
    (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
      prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i))
Tactic:
unfold AGMProofSystemInstantiation.soundness AGMProofSystemInstantiation.verify AGMProofSystemInstantiation.proof_element_G1_as_poly AGMProofSystemInstantiation.proof_element_G2_as_poly
Proof state after:
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
⊢ ∀ (stmt : GGPR.Stmt) (prover : AGMProofSystemInstantiation.Prover F GGPR),
    ((∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0) ∧
        ∀ pfs ∈ GGPR.Identified_Proof_Elems,
          (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
                GGPR.ListSRSElements_G1).sum =
            (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
                GGPR.ListSRSElements_G2).sum) →
      (fun stmt wit =>
          let t := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i));
          ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
                    (List.map (fun i => Polynomial.C (wit.1 i) * v_wit i) (List.finRange n_wit)).sum) *
                  (w_0 + (List.map (fun i => Polynomial.C (wit.2 i) * w_wit i) (List.finRange m)).sum)).modByMonic
              t =
            0)
        stmt
        ((fun prover =>
            (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
              prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
          prover)
Theorem: MvPolynomial.optionEquivRight_X_some
Proof state before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ (optionEquivRight R S₁) (X (Option.some x)) = X x
Tactic:
unfold optionEquivRight AlgEquiv.ofAlgHom
Proof state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ { toFun := ⇑(aeval fun o => o.elim (C Polynomial.X) X),
        invFun := ⇑(aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)), left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
      (X (Option.some x)) =
    X x
Theorem: MvPolynomial.optionEquivRight_X_some
Proof state before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ { toFun := ⇑(aeval fun o => o.elim (C Polynomial.X) X),
        invFun := ⇑(aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)), left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
      (X (Option.some x)) =
    X x
Tactic:
simp only [AlgEquiv.coe_mk, aeval_X, Option.elim]
Proof state after:
no goals
Theorem: MvPolynomial.optionEquivRight_X_none
Proof state before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ (optionEquivRight R S₁) (X none) = C Polynomial.X
Tactic:
unfold optionEquivRight AlgEquiv.ofAlgHom
Proof state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ { toFun := ⇑(aeval fun o => o.elim (C Polynomial.X) X),
        invFun := ⇑(aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)), left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
      (X none) =
    C Polynomial.X
Theorem: MvPolynomial.optionEquivRight_X_none
Proof state before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ { toFun := ⇑(aeval fun o => o.elim (C Polynomial.X) X),
        invFun := ⇑(aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)), left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
      (X none) =
    C Polynomial.X
Tactic:
simp only [AlgEquiv.coe_mk, aeval_X, Option.elim]
Proof state after:
no goals
Theorem: MvPolynomial.optionEquivRight_C
Proof state before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ (optionEquivRight R S₁) (C r) = C (Polynomial.C r)
Tactic:
unfold optionEquivRight AlgEquiv.ofAlgHom
Proof state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ { toFun := ⇑(aeval fun o => o.elim (C Polynomial.X) X),
        invFun := ⇑(aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)), left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
      (C r) =
    C (Polynomial.C r)
Theorem: MvPolynomial.optionEquivRight_C
Proof state before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ { toFun := ⇑(aeval fun o => o.elim (C Polynomial.X) X),
        invFun := ⇑(aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)), left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
      (C r) =
    C (Polynomial.C r)
Tactic:
simp only [Option.elim, AlgEquiv.coe_mk, aeval_C]
Proof state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ (algebraMap R (MvPolynomial S₁ (Polynomial R))) r = C (Polynomial.C r)
Theorem: MvPolynomial.optionEquivRight_C
Proof state before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ (algebraMap R (MvPolynomial S₁ (Polynomial R))) r = C (Polynomial.C r)
Tactic:
rfl
Proof state after:
no goals
Theorem: to_MvPolynomial_Option_X
Proof state before:
F V : Type
inst✝ : Field F
⊢ (to_MvPolynomial_Option V) Polynomial.X = X none
Tactic:
simp [to_MvPolynomial_Option]
Proof state after:
no goals
Theorem: to_MvPolynomial_Option_C
Proof state before:
F V : Type
inst✝ : Field F
r : F
⊢ (to_MvPolynomial_Option V) (Polynomial.C r) = C r
Tactic:
simp [to_MvPolynomial_Option]
Proof state after:
no goals
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (⇑f ∘ a) p
Tactic:
simp only [eval₂, sum_def]
Proof state after:
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ f (∑ m ∈ p.support, (algebraMap R A) (coeff m p) * m.prod fun n e => a n ^ e) =
    ∑ m ∈ p.support, (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ f (∑ m ∈ p.support, (algebraMap R A) (coeff m p) * m.prod fun n e => a n ^ e) =
    ∑ m ∈ p.support, (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e
Tactic:
simp only [f.map_sum, f.map_mul, f.map_pow, eq_intCast, map_intCast, AlgHom.commutes]
Proof state after:
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ ∑ x ∈ p.support, (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e) =
    ∑ m ∈ p.support, (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ ∑ x ∈ p.support, (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e) =
    ∑ m ∈ p.support, (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e
Tactic:
congr
Proof state after:
case e_f
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ (fun x => (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e)) = fun m =>
    (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
case e_f
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ (fun x => (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e)) = fun m =>
    (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e
Tactic:
ext x
Proof state after:
case e_f.h
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e) =
    (algebraMap R B) (coeff x p) * x.prod fun n e => (⇑f ∘ a) n ^ e
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
case e_f.h
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e) =
    (algebraMap R B) (coeff x p) * x.prod fun n e => (⇑f ∘ a) n ^ e
Tactic:
congr
Proof state after:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (x.prod fun n e => a n ^ e) = x.prod fun n e => (⇑f ∘ a) n ^ e
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (x.prod fun n e => a n ^ e) = x.prod fun n e => (⇑f ∘ a) n ^ e
Tactic:
simp only [Function.comp_apply]
Proof state after:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (x.prod fun n e => a n ^ e) = x.prod fun n e => f (a n) ^ e
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (x.prod fun n e => a n ^ e) = x.prod fun n e => f (a n) ^ e
Tactic:
unfold prod
Proof state after:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (∏ a_1 ∈ x.support, (fun n e => a n ^ e) a_1 (x a_1)) = ∏ a_1 ∈ x.support, (fun n e => f (a n) ^ e) a_1 (x a_1)
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (∏ a_1 ∈ x.support, (fun n e => a n ^ e) a_1 (x a_1)) = ∏ a_1 ∈ x.support, (fun n e => f (a n) ^ e) a_1 (x a_1)
Tactic:
rw [f.map_prod]
Proof state after:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ ∏ x_1 ∈ x.support, f ((fun n e => a n ^ e) x_1 (x x_1)) = ∏ a_1 ∈ x.support, (fun n e => f (a n) ^ e) a_1 (x a_1)