mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ antidiagonal (single a n) =
    map ({ toFun := single a, inj' := ⋯ }.prodMap { toFun := single a, inj' := ⋯ }) (antidiagonal n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ embDomain f y ∈ Set.range (embDomain f)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case refine_4
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ embDomain f (comapDomain (⇑f) v ⋯) = v

Tactic:
rw [embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
      (isLowerSet_range_embDomain f (le_iff_exists_add'.mpr ⟨u, h.symm⟩) (by simp)))]

Goal state after:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
⊢ image (Prod.map (embDomain f) (embDomain f)) (antidiagonal y) = antidiagonal (embDomain f y)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
⊢ image
      (fun x ↦
        match x with
        | ((x, y), z, w) => (x.sumElim z, y.sumElim w))
      (antidiagonal x ×ˢ antidiagonal y) =
    antidiagonal (x.sumElim y)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁴ : Zero α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedCancelAddMonoid β
inst✝ : AddLeftStrictMono β
f : ι →₀ α
g : ι → α → β
h : ∀ i ∈ f.support, 0 < g i (f i)
hf : f ≠ 0
⊢ f.support.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a b : α
⊢ single i a ≤ single i b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a : α
⊢ 0 ≤ single i a ↔ 0 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a : α
⊢ single i a ≤ 0 ↔ a ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : 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
⊢ f₁.sum h ≤ f₂.sum h

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q r✝ : R[X]
r : R
p : A[X]
⊢ ((C.comp (algebraMap R A)) r * p).toFinsupp = (p * (C.comp (algebraMap R A)) r).toFinsupp

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q r✝ : R[X]
r : R
p : A[X]
⊢ (r • p).toFinsupp = ((C.comp (algebraMap R A)) r * p).toFinsupp

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p q r✝ : R[X]
r : R
⊢ (toFinsuppIso R).toFun ((algebraMap R R[X]) r) = (algebraMap R R[ℕ]) r

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
p q r : R[X]
inst✝ : Nontrivial A
⊢ ⊥ ≠ ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (f a) p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ embDomain f g₁ ≤ embDomain f g₂ ↔ g₁ ≤ g₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ embDomain f g₁ < embDomain f g₂ ↔ g₁ < g₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι → κ
h : Function.Injective f
g₁ g₂ : ι →₀ α
⊢ mapDomain f g₁ ≤ mapDomain f g₂ ↔ g₁ ≤ g₂

Tactic:
by

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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) (f X) p = f p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
f : ι → κ
h : Function.Injective f
g₁ g₂ : ι →₀ α
⊢ mapDomain f g₁ < mapDomain f g₂ ↔ g₁ < g₂

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p q r : R[X]
f : A →ₐ[R] B
⊢ ∀ (r : R), (↑↑(mapRingHom f.toRingHom)).toFun ((algebraMap R A[X]) r) = (algebraMap R B[X]) r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g₁ g₂ : ι →₀ α
h : g₁ ≤ g₂
⊢ ∀ i ∈ g₁.support ∪ g₂.support, single (f i) 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
⊢ Monotone (mapDomain f)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : 0 ≤ g
⊢ 0 ≤ mapDomain f g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : g ≤ 0
⊢ mapDomain f g ≤ 0

Tactic:
by

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
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : B →ₐ[R] C
g : A →ₐ[R] B
⊢ (mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g)

Tactic:
by

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
⊢ mapAlgHom f = eval₂AlgHom (CAlgHom.comp f) X ⋯

Tactic:
by

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
p : A[X]
n : ℕ
⊢ ((mapAlgHom f) p).coeff n = f (p.coeff n)

Tactic:
by

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 : ℕ
⊢ ↑R (lcoeff B n) ∘ₗ (mapAlgHom f).toLinearMap = f.toLinearMap ∘ₗ ↑R (lcoeff A n)

Tactic:
by

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 : ℕ
a : A
⊢ (mapAlgHom f) ((monomial n) a) = (monomial n) (f a)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p q r : R[X]
f : A ≃ₐ[R] B
⊢ (mapAlgHom ↑f).comp (mapAlgHom ↑f.symm) = AlgHom.id R B[X]

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p q r : R[X]
f : A ≃ₐ[R] B
⊢ (mapAlgHom ↑f.symm).comp (mapAlgHom ↑f) = AlgHom.id R A[X]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
⊢ (single a (f a)).sum g ≤ f.sum g

Tactic:
by

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
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
⊢ (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : M → N
hg : g 0 = 0
h : 0 ≤ fun x ↦ g x
a : α
⊢ g (f a) ≤ f.sum fun x m ↦ g m

Tactic:
by

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

Goal state before:
pp: R : Type u
B : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring B
inst✝ : Algebra R B
P : R[X]
b : B
⊢ eval b (map (algebraMap R B) P) = (aeval b) P

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
f g : ι →₀ α
inst✝ : IsBotZeroClass α
⊢ ∀ (a : ι →₀ α), 0 ≤ a

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
⊢ (mapAlg R S) p = map (algebraMap R S) p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
⊢ f + g = 0 ↔ f = 0 ∧ g = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
p : A[X]
⊢ (mapAlg A C) p = (mapAlg B C) ((mapAlg A B) p)

Tactic:
by

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

Goal state before:
pp: A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
p : A[X]
⊢ (algebraMap B C) ((algebraMap A B) (p.coeff 0)) = ((mapAlg A C) p).coeff 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s : Finset ι
hf : f.support ⊆ s
⊢ f ≤ g ↔ ∀ i ∈ s, f i ≤ g i

Tactic:
by

Goal state after:
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 : a ∈ f.support
⊢ a ∈ g.support

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
i : ι
x : α
f : ι →₀ α
⊢ (∀ i_1 ∈ {i}, (single i x) i_1 ≤ f i_1) ↔ x ≤ f i

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
x✝ : R[X]
⊢ ((aeval p).comp (aeval q)) x✝ = (AlgHom.id R R[X]) x✝

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
x✝ : R[X]
⊢ ((aeval q).comp (aeval p)) x✝ = (AlgHom.id R R[X]) x✝

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
⊢ R[X] ≃ₐ[R] R[X]

Tactic:
by

Goal state after:
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.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'
⊢ p = p'

Tactic:
by

Goal state after:
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'
⊢ p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a✝ b✝ : R✝
n : ℕ
inst✝⁷ : CommSemiring R✝
inst✝⁶ : Semiring A
inst✝⁵ : CommSemiring A'
inst✝⁴ : Semiring B
inst✝³ : Algebra R✝ A
inst✝² : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
⊢ (C a * X + C b).comp (C ⅟a * (X - C b)) = X

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a✝ b✝ : R✝
n : ℕ
inst✝⁷ : CommSemiring R✝
inst✝⁶ : Semiring A
inst✝⁵ : CommSemiring A'
inst✝⁴ : Semiring B
inst✝³ : Algebra R✝ A
inst✝² : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
⊢ (C ⅟a * (X - C b)).comp (C a * X + C b) = X

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
⊢ single i (a - b) = single i a - single i b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f1 f2 : ι →₀ α
⊢ (f1 - f2).support ⊆ f1.support

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
⊢ (algEquivCMulXAddC a b).symm = algEquivCMulXAddC (⅟a) (-⅟a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : DecidableEq ι
f1 f2 : ι →₀ α
⊢ f1.support \ f2.support ⊆ (f1 - f2).support

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R✝
n : ℕ
inst✝⁶ : CommSemiring R✝
inst✝⁵ : Semiring A
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B
inst✝² : Algebra R✝ A
inst✝¹ : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝ : CommRing R
t : R
⊢ (X + C t).comp (X - C t) = X

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R✝
n : ℕ
inst✝⁶ : CommSemiring R✝
inst✝⁵ : Semiring A
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B
inst✝² : Algebra R✝ A
inst✝¹ : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝ : CommRing R
t : R
⊢ (X - C t).comp (X + C t) = X

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
t t' : R
⊢ algEquivAevalXAddC t = algEquivAevalXAddC t' ↔ t = t'

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
t : R
⊢ (algEquivAevalXAddC t).symm = algEquivAevalXAddC (-t)

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R✝
n : ℕ
inst✝⁶ : CommSemiring R✝
inst✝⁵ : Semiring A
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B
inst✝² : Algebra R✝ A
inst✝¹ : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝ : CommRing R
⊢ (-X).comp (-X) = X

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
⊢ mapDomain f (f1 - f2) = mapDomain f f1 - mapDomain f f2

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p : R[X]
⊢ (p.comp (-X)).comp (-X) = p

Tactic:
by

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
x : A
⊢ (aeval (f x)) X = (f.comp (aeval x)) X

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι ↪ κ
f1 f2 : ι →₀ α
⊢ embDomain f (f1 - f2) = embDomain f f1 - embDomain f f2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊓ g).support = f.support ∩ g.support

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
⊢ φ p = eval₂ (algebraMap R A) (φ X) p

Tactic:
by

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 : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ∀ (a : R), (aeval (f x)) (C a) = f ((aeval x) (C a))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊔ g).support = f.support ∪ g.support

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsBotZeroClass α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support

Tactic:
by

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 : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    (aeval (f x)) (C a * X ^ n) = f ((aeval x) (C a * X ^ n)) →
      (aeval (f x)) (C a * X ^ (n + 1)) = f ((aeval x) (C a * X ^ (n + 1)))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
u : ι →₀ ℕ
i : ι
h : u i ≠ 0
⊢ u - single i 1 + single i 1 = u

Tactic:
by

Goal state after:
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✝ : β
⊢ x✝ ∈ ↑y.support → x✝ ∈ ↑(y + w).support

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ↪ β
⊢ IsLowerSet (Set.range (embDomain f))

Tactic:
by

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 : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ (aeval (f x)) p = f ((aeval x) p)

Tactic:
by

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝ : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ Pi.Lex r (fun {i} x1 x2 ↦ x1 < x2) x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : (i : ι) → LT (β i)
r : ι → ι → Prop
inst✝ : Std.Irrefl r
x y : (i : ι) → β i
⊢ Pi.Lex r (fun {i} x1 x2 ↦ x1 < x2) x y ↔ x default < y default

Tactic:
by

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), Std.Trichotomous s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex r s a b
hba : ¬Pi.Lex r s b a
h✝ : ∃ a_1, a a_1 ≠ b a_1
i : ι := wf.min {i | a i ≠ b i} h✝
j : ι
hr : r j i
h : ¬a j = b j
⊢ j ∈ {i | a i ≠ b i}

Tactic:
by

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), Std.Trichotomous s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex r s a b
hba : ¬Pi.Lex r s b a
⊢ a = b

Tactic:
by

Goal state after: