mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h✝ : p
⊢ a h✝ < 1

pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h✝ : ¬p
⊢ b h✝ < 1

Tactic:
;

Goal state after:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h✝ : p
⊢ a h✝ < 1

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h✝ : ¬p
⊢ b h✝ < 1
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case h
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
i : ι
hi : i ∈ f₁.support ∪ f₂.support
⊢ h i (f₁ i) ≤ h i (f₂ i)

Tactic:
exact hh _ hi <| hf _

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : A →ₐ[R] B
n : ℕ
f : A[X]
⊢ (↑R (lcoeff B n) ∘ₗ (mapAlgHom f✝).toLinearMap) f = (f✝.toLinearMap ∘ₗ ↑R (lcoeff A n)) f

Tactic:
;

Goal state after:
R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : A →ₐ[R] B
n : ℕ
f : A[X]
⊢ (↑R (lcoeff B n) ∘ₗ (mapAlgHom f✝).toLinearMap) f = (f✝.toLinearMap ∘ₗ ↑R (lcoeff A n)) f
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : 0 < f a
⊢ 0 < g a

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : 0 < f a
⊢ 0 < g a
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p = p'
a✝ : R[X]
⊢ (p.algEquivOfCompEqX q hpq hqp) a✝ = (p'.algEquivOfCompEqX q' hpq' hqp') a✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p = p'
a✝ : R[X]
⊢ (p.algEquivOfCompEqX q hpq hqp) a✝ = (p'.algEquivOfCompEqX q' hpq' hqp') a✝
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
x✝ : β
⊢ ¬y x✝ = 0 → y x✝ = 0 → ¬w x✝ = 0

Tactic:
;

Goal state after:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
x✝ : β
⊢ ¬y x✝ = 0 → y x✝ = 0 → ¬w x✝ = 0
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex x j_1 = toLex (update x i a) j_1
h : x j < update x i a j
⊢ x i < a

Tactic:
obtain rfl : j = i := by
    by_contra H
    rw [update_of_ne H] at h
    exact h.false

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
a : β j
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex x j_1 = toLex (update x j a) j_1
h : x j < update x j a j
⊢ x j < a
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : update x i a j < x j
⊢ a < x i

Tactic:
obtain rfl : j = i := by
    by_contra H
    rw [update_of_ne H] at h
    exact h.false

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
a : β j
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex (update x j a) j_1 = toLex x j_1
h : update x j a j < x j
⊢ a < x j
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : 0 < f a
⊢ 0 < g a

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : 0 < f a
⊢ 0 < g a
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g ↦ F a f g
⊢ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂

Tactic:
ext a
  simpa only [mem_neLocus] using! (hF a _).ne_iff

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (M a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective fun f ↦ F a f g
⊢ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂

Tactic:
ext a
  simpa only [mem_neLocus] using! (hF a _).ne_iff

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
⊢ eval₂ f g (C a) = f a

Tactic:
by
  rw [C_apply, eval₂_monomial, prod_zero_index, mul_one]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ (C (p.coeff 0)).coeff = p.coeff

Tactic:
;

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ (C (p.coeff 0)).coeff = p.coeff
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ (C (p.coeff 0)).coeff default = p.coeff default

Tactic:
;

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ (C (p.coeff 0)).coeff default = p.coeff default
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e

Tactic:
apply MvPolynomial.induction_on p
  · intro a' s a
    simp [C_mul_monomial, eval₂_monomial, f.map_mul]
  · intro p q ih_p ih_q
    simp [add_mul, eval₂_add, ih_p, ih_q]
  · intro p n ih s a
    exact
      calc (p * X n * monomial s a).eval₂ f g
        _ = (p * monomial (Finsupp.single n 1 + s) a).eval₂ f g := by
          rw [monomial_single_add, pow_one, mul_assoc]
        _ = (p * monomial (Finsupp.single n 1) 1).eval₂ f g * f a * s.prod fun n e => g n ^ e := by
          simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm,
            f.map_one]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_2
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ ∀ (x : σ),
    ((↑f).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) =
      ((↑g).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))

Tactic:
;

Goal state after:
case refine_2
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ ∀ (x : σ),
    ((↑f).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) =
      ((↑g).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f₁ : R →+* S₁
g₁ : σ → S₁
p₁ : MvPolynomial σ R
⊢ (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₁ g₁) p₁

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f₁ : R →+* S₁
g₁ : σ → S₁
p₁ : MvPolynomial σ R
⊢ (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₁ g₁) p₁
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
hp : p ∈ ⊤
⊢ p ∈ S

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
hp : p ∈ ⊤
⊢ p ∈ S
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case hnc
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬1 = 0

Tactic:
;

Goal state after:
case hnc
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬1 = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), coeff m p = coeff m q
a✝ : σ →₀ ℕ
⊢ p.coeff a✝ = q.coeff a✝

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), coeff m p = coeff m q
a✝ : σ →₀ ℕ
⊢ p.coeff a✝ = q.coeff a✝
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
⊢ (fun s a ↦ f a * s.prod fun n e ↦ g₁ n ^ e) C (p.coeff C) = (fun s a ↦ f a * s.prod fun n e ↦ g₂ n ^ e) C (p.coeff C)

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
⊢ (fun s a ↦ f a * s.prod fun n e ↦ g₁ n ^ e) C (p.coeff C) = (fun s a ↦ f a * s.prod fun n e ↦ g₂ n ^ e) C (p.coeff C)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
⊢ (f (p.coeff C) * C.prod fun n e ↦ g₁ n ^ e) = f (p.coeff C) * C.prod fun n e ↦ g₂ n ^ e

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
⊢ (f (p.coeff C) * C.prod fun n e ↦ g₁ n ^ e) = f (p.coeff C) * C.prod fun n e ↦ g₂ n ^ e
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
hi : i ∈ C.support
⊢ (fun n e ↦ g₁ n ^ e) i (C i) = (fun n e ↦ g₂ n ^ e) i (C i)

Tactic:
;

Goal state after:
case e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
hi : i ∈ C.support
⊢ (fun n e ↦ g₁ n ^ e) i (C i) = (fun n e ↦ g₂ n ^ e) i (C i)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
hi : i ∈ C.support
⊢ g₁ i ^ C i = g₂ i ^ C i

Tactic:
;

Goal state after:
case e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
hi : i ∈ C.support
⊢ g₁ i ^ C i = g₂ i ^ C i
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t ↦ eval₂ f g (q t)) p = eval₂ ((eval₂Hom f g).comp C) (⇑(eval₂Hom f g) ∘ q) p

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t ↦ eval₂ f g (q t)) p = eval₂ ((eval₂Hom f g).comp C) (⇑(eval₂Hom f g) ∘ q) p
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case e_f
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
a : R
⊢ f a = ((eval₂Hom f g).comp C) a

Tactic:
;

Goal state after:
case e_f
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
a : R
⊢ f a = ((eval₂Hom f g).comp C) a
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
j : σ →₀ ℕ
h : j + s ∈ (p * (monomial s) r).support
⊢ s ≤ j + s

Tactic:
exact le_add_left le_rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval₂Hom (RingHom.id R) (⇑(eval₂Hom (RingHom.id R) g) ∘ f)) p =
    eval₂ ((eval₂Hom (RingHom.id R) g).comp C) (⇑(eval₂Hom (RingHom.id R) g) ∘ f) p

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval₂Hom (RingHom.id R) (⇑(eval₂Hom (RingHom.id R) g) ∘ f)) p =
    eval₂ ((eval₂Hom (RingHom.id R) g).comp C) (⇑(eval₂Hom (RingHom.id R) g) ∘ f) p
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
a : R
⊢ (RingHom.id R) a = ((eval₂Hom (RingHom.id R) g).comp C) a

Tactic:
;

Goal state after:
case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
a : R
⊢ (RingHom.id R) a = ((eval₂Hom (RingHom.id R) g).comp C) a
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ (p.coeff.sum fun s a ↦ f a * s.prod fun n e ↦ g n ^ e) = ((map f) p).coeff.sum fun s a ↦ a * s.prod fun n e ↦ g n ^ e

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ (p.coeff.sum fun s a ↦ f a * s.prod fun n e ↦ g n ^ e) = ((map f) p).coeff.sum fun s a ↦ a * s.prod fun n e ↦ g n ^ e
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (a : R), k (eval₂ f g (C a)) = eval₂ k (⇑k ∘ g) ((map f) (C a))

Tactic:
intro r

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
r : R
⊢ k (eval₂ f g (C r)) = eval₂ k (⇑k ∘ g) ((map f) (C r))
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
r : R
⊢ (mapDomainAlgHom R R (mapDomain.addMonoidHom f))
      ((have __src := singleZeroRingHom;
        { toFun := ⇑(AddMonoidAlgebra.lsingle 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r) =
    (have __src := singleZeroRingHom;
      { toFun := ⇑(AddMonoidAlgebra.lsingle 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      r

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
r : R
⊢ (mapDomainAlgHom R R (mapDomain.addMonoidHom f))
      ((have __src := singleZeroRingHom;
        { toFun := ⇑(AddMonoidAlgebra.lsingle 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r) =
    (have __src := singleZeroRingHom;
      { toFun := ⇑(AddMonoidAlgebra.lsingle 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      r
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddLeftStrictMono (α i)
x✝³ x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (ofLex x✝³) a + (ofLex x✝²) a < (ofLex x✝³) a + (ofLex x✝¹) a

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddLeftStrictMono (α i)
x✝³ x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (ofLex x✝³) a + (ofLex x✝²) a < (ofLex x✝³) a + (ofLex x✝¹) a
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
i✝ : σ
m✝ : τ →₀ ℕ
⊢ coeff m✝ ((rename f) (X i✝)) = coeff m✝ ((aeval (X ∘ f)) (X i✝))

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
i✝ : σ
m✝ : τ →₀ ℕ
⊢ coeff m✝ ((rename f) (X i✝)) = coeff m✝ ((aeval (X ∘ f)) (X i✝))
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddRightStrictMono (α i)
f x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (ofLex x✝²) a + (ofLex f) a < (ofLex x✝¹) a + (ofLex f) a

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddRightStrictMono (α i)
f x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (ofLex x✝²) a + (ofLex f) a < (ofLex x✝¹) a + (ofLex f) a
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
⊢ ∀ (a : R), (map f) (eval₂ C g (C a)) = eval₂ C (⇑(map f) ∘ g) ((map f) (C a))

Tactic:
intro r

Goal state after:
case C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
r : R
⊢ (map f) (eval₂ C g (C r)) = eval₂ C (⇑(map f) ∘ g) ((map f) (C r))
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ (p.support.sup fun s ↦ toMultiset s) = p.support.sup fun s ↦ toMultiset s

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ (p.support.sup fun s ↦ toMultiset s) = p.support.sup fun s ↦ toMultiset s
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (a : R) (m : σ →₀ ℕ), coeff m ((map f) (C a)) = f (coeff m (C a))

Tactic:
intro r

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
r : R
⊢ ∀ (m : σ →₀ ℕ), coeff m ((map f) (C r)) = f (coeff m (C r))
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ ((p + q).support.sup fun s ↦ toMultiset s) ≤ (p.support.sup fun s ↦ toMultiset s) ⊔ q.support.sup fun s ↦ toMultiset s

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ ((p + q).support.sup fun s ↦ toMultiset s) ≤ (p.support.sup fun s ↦ toMultiset s) ⊔ q.support.sup fun s ↦ toMultiset s
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∑ i ∈ s, f i).support.sup fun s ↦ toMultiset s) ≤ s.sup fun i ↦ (f i).support.sup fun s ↦ toMultiset s

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∑ i ∈ s, f i).support.sup fun s ↦ toMultiset s) ≤ s.sup fun i ↦ (f i).support.sup fun s ↦ toMultiset s