mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case single_one_right
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
g : N →* O
m✝ : M
a✝ : O
⊢ ((mapDomainAlgHom R A (g.comp f)) (single m✝ 1)).coeff a✝ =
    (((mapDomainAlgHom R A g).comp (mapDomainAlgHom R A f)) (single m✝ 1)).coeff a✝

pp: case single_one_left
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
g : N →* O
x✝ : A
a✝ : O
⊢ (((mapDomainAlgHom R A (g.comp f)).comp singleOneAlgHom) x✝).coeff a✝ =
    ((((mapDomainAlgHom R A g).comp (mapDomainAlgHom R A f)).comp singleOneAlgHom) x✝).coeff a✝

Tactic:
<;>

Goal state after:
case single_one_right
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
g : N →* O
m✝ : M
a✝ : O
⊢ ((mapDomainAlgHom R A (g.comp f)) (single m✝ 1)).coeff a✝ =
    (((mapDomainAlgHom R A g).comp (mapDomainAlgHom R A f)) (single m✝ 1)).coeff a✝

case single_one_left
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
g : N →* O
x✝ : A
a✝ : O
⊢ (((mapDomainAlgHom R A (g.comp f)).comp singleOneAlgHom) x✝).coeff a✝ =
    ((((mapDomainAlgHom R A g).comp (mapDomainAlgHom R A f)).comp singleOneAlgHom) x✝).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case single_one_right
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
m✝ a✝ : M
⊢ ((mapAlgHom M (AlgHom.id R A)) (single m✝ 1)).coeff a✝ = ((AlgHom.id R A[M]) (single m✝ 1)).coeff a✝

pp: case single_one_left
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
x✝ : A
a✝ : M
⊢ (((mapAlgHom M (AlgHom.id R A)).comp singleOneAlgHom) x✝).coeff a✝ =
    (((AlgHom.id R A[M]).comp singleOneAlgHom) x✝).coeff a✝

Tactic:
<;>

Goal state after:
case single_one_right
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
m✝ a✝ : M
⊢ ((mapAlgHom M (AlgHom.id R A)) (single m✝ 1)).coeff a✝ = ((AlgHom.id R A[M]) (single m✝ 1)).coeff a✝

case single_one_left
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
x✝ : A
a✝ : M
⊢ (((mapAlgHom M (AlgHom.id R A)).comp singleOneAlgHom) x✝).coeff a✝ =
    (((AlgHom.id R A[M]).comp singleOneAlgHom) x✝).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case single_one_right
R : Type u_1
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Monoid M
f : A →ₐ[R] B
g : B →ₐ[R] C
m✝ a✝ : M
⊢ ((mapAlgHom M (g.comp f)) (single m✝ 1)).coeff a✝ = (((mapAlgHom M g).comp (mapAlgHom M f)) (single m✝ 1)).coeff a✝

pp: case single_one_left
R : Type u_1
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Monoid M
f : A →ₐ[R] B
g : B →ₐ[R] C
x✝ : A
a✝ : M
⊢ (((mapAlgHom M (g.comp f)).comp singleOneAlgHom) x✝).coeff a✝ =
    ((((mapAlgHom M g).comp (mapAlgHom M f)).comp singleOneAlgHom) x✝).coeff a✝

Tactic:
<;>

Goal state after:
case single_one_right
R : Type u_1
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Monoid M
f : A →ₐ[R] B
g : B →ₐ[R] C
m✝ a✝ : M
⊢ ((mapAlgHom M (g.comp f)) (single m✝ 1)).coeff a✝ = (((mapAlgHom M g).comp (mapAlgHom M f)) (single m✝ 1)).coeff a✝

case single_one_left
R : Type u_1
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Monoid M
f : A →ₐ[R] B
g : B →ₐ[R] C
x✝ : A
a✝ : M
⊢ (((mapAlgHom M (g.comp f)).comp singleOneAlgHom) x✝).coeff a✝ =
    ((((mapAlgHom M g).comp (mapAlgHom M f)).comp singleOneAlgHom) x✝).coeff a✝
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case inl
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
x✝ : x ∈ univ
h✝ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

pp: case inr
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
x✝ : x ∈ univ
h✝ : b ≤ x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
x✝ : x ∈ univ
h✝ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

case inr
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
x✝ : x ∈ univ
h✝ : b ≤ x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ (List.map (fun f ↦ f.coeff.support.inf degt) l).sum ≤ l.prod.coeff.support.inf degt

Tactic:
refine OrderDual.ofDual_le_ofDual.mpr ?_

Goal state after:
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ Quot.lift (fun l ↦ List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ l) ⋯ (Multiset.map degt l.prod.coeff.support.val) ≤
    List.foldr (fun x1 x2 ↦ x1 + x2) 0 (List.map (fun f ↦ f.coeff.support.inf degt) l)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.degree = ↑n ↔ p.natDegree = n

Tactic:
rw [degree_eq_natDegree hp]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑p.natDegree = ↑n ↔ p.natDegree = n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ p.degree ≤ q.degree

Tactic:
rw [degree_eq_natDegree hp]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ ↑p.natDegree ≤ q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
⊢ p.degree ≤ q.degree

Tactic:
by_cases hp : p = 0
  · rw [hp, degree_zero]
    exact bot_le
  · rw [degree_eq_natDegree hp]
    exact le_degree_of_ne_zero h

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
⊢ (C a).degree ≤ 0

Tactic:
by
  by_cases h : a = 0
  · rw [h, C_0]
    exact bot_le
  · rw [degree_C h]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
a : A
r : R
hr : r = 0
⊢ supDegree D (single a r) = ⊥

pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
a : A
r : R
hr : ¬r = 0
⊢ supDegree D (single a r) = D a

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
a : A
r : R
hr : r = 0
⊢ supDegree D (single a r) = ⊥

case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
a : A
r : R
hr : ¬r = 0
⊢ supDegree D (single a r) = D a
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ {n}.max = ↑n

Tactic:
max_singleton,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case pos
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : i = d
h✝ : i < d
⊢ ↑(d.choose i) - 1 = ↑(d.choose i)

pp: case neg
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : i = d
h✝ : ¬i < d
⊢ ↑(d.choose i) - 1 = 0

pp: case pos
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : ¬i = d
h✝ : i < d
⊢ ↑(d.choose i) - 0 = ↑(d.choose i)

pp: case neg
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : ¬i = d
h✝ : ¬i < d
⊢ ↑(d.choose i) - 0 = 0

Tactic:
<;>

Goal state after:
case pos
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : i = d
h✝ : i < d
⊢ ↑(d.choose i) - 1 = ↑(d.choose i)

case neg
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : i = d
h✝ : ¬i < d
⊢ ↑(d.choose i) - 1 = 0

case pos
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : ¬i = d
h✝ : i < d
⊢ ↑(d.choose i) - 0 = ↑(d.choose i)

case neg
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : ¬i = d
h✝ : ¬i < d
⊢ ↑(d.choose i) - 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).degree = p.degree

Tactic:
unfold degree; rw [support_neg]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
p q : R[X]
h : (p + q).degree ≤ p.degree
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree

pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
h : (p + q).degree ≤ q.degree
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree

Tactic:
<;>

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
p q : R[X]
h : (p + q).degree ≤ p.degree
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree

case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
h : (p + q).degree ≤ q.degree
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun i ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : ¬φ.coeff i ≠ 0
⊢ φ.coeff i = r * 0

Tactic:
Classical.not_not

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun i ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : φ.coeff i = 0
⊢ φ.coeff i = r * 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
h : n✝ = n
⊢ a = p.coeff n✝ + (a - p.coeff n)

pp: case neg
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
h : ¬n✝ = n
⊢ p.coeff n✝ = p.coeff n✝ + 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
h : n✝ = n
⊢ a = p.coeff n✝ + (a - p.coeff n)

case neg
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
h : ¬n✝ = n
⊢ p.coeff n✝ = p.coeff n✝ + 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case ofNat
R : Type u_1
inst✝ : Ring R
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).coeff 0 = ↑(Int.ofNat a✝)

pp: case negSucc
R : Type u_1
inst✝ : Ring R
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).coeff 0 = ↑(Int.negSucc a✝)

Tactic:
<;>

Goal state after:
case ofNat
R : Type u_1
inst✝ : Ring R
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).coeff 0 = ↑(Int.ofNat a✝)

case negSucc
R : Type u_1
inst✝ : Ring R
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).coeff 0 = ↑(Int.negSucc a✝)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
hq : q ≠ 0
⊢ p.natDegree < q.natDegree

Tactic:
rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree ≤ ↑p.natDegree

pp: case h₂
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ q.degree ≤ ↑q.natDegree

Tactic:
<;>

Goal state after:
case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree ≤ ↑p.natDegree

case h₂
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ q.degree ≤ ↑q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: case inl.inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
⊢ (0 ^ 0).natDegree = 0 * natDegree 0

pp: case inl.inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
n : ℕ
hn : n ≠ 0
⊢ (0 ^ n).natDegree = n * natDegree 0

Tactic:
<;>

Goal state after:
case inl.inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
⊢ (0 ^ 0).natDegree = 0 * natDegree 0

case inl.inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
n : ℕ
hn : n ≠ 0
⊢ (0 ^ n).natDegree = n * natDegree 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
hr : r = 0
⊢ (C r * p).leadingCoeff = r

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
hr : ¬r = 0
⊢ (C r * p).leadingCoeff = r

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
hr : r = 0
⊢ (C r * p).leadingCoeff = r

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
hr : ¬r = 0
⊢ (C r * p).leadingCoeff = r
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ

Tactic:
have h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0 := by rwa [pow_succ', ← ih h₁] at h

Goal state after:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
i : ℕ
a✝ : Nontrivial R
⊢ (X + C r).leadingCoeff ^ i = 1

pp: R : Type u
inst✝ : Semiring R
r : R
i : ℕ
a✝ : Nontrivial R
⊢ (X + C r).leadingCoeff ^ i ≠ 0

Tactic:
<;>

Goal state after:
R : Type u
inst✝ : Semiring R
r : R
i : ℕ
a✝ : Nontrivial R
⊢ (X + C r).leadingCoeff ^ i = 1

R : Type u
inst✝ : Semiring R
r : R
i : ℕ
a✝ : Nontrivial R
⊢ (X + C r).leadingCoeff ^ i ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case ha
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p q : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D p ≠ 0

pp: case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p q : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D q ≠ 0

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p q : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D p ≠ 0

case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p q : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D q ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.coeff.support.Nonempty
⊢ infDegree (WithTop.some ∘ D) s = ↑(infDegree D s)

Tactic:
unfold AddMonoidAlgebra.infDegree
  rw [← Finset.coe_inf' hs, Finset.inf'_eq_inf]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
⊢ f = g

Tactic:
set f' := f.comp (toFinsuppIso R).symm.toRingHom with hf'
  set g' := g.comp (toFinsuppIso R).symm.toRingHom with hg'
  have A : f' = g' := by
    ext
    · simp [f', g', h₁, RingEquiv.toRingHom_eq_coe]
    simpa using! h₂
  have B : f = f'.comp (toFinsuppIso R) := by
    rw [hf', RingHom.comp_assoc]
    ext x
    simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply,
      RingHom.coe_comp, RingEquiv.coe_toRingHom]
  have C' : g = g'.comp (toFinsuppIso R) := by
    rw [hg', RingHom.comp_assoc]
    ext x
    simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply,
      RingHom.coe_comp, RingEquiv.coe_toRingHom]
  rw [B, C', A]

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 1 ≤ a
hb : 1 ≤ b
h✝ : p
⊢ 1 ≤ a

pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 1 ≤ a
hb : 1 ≤ b
h✝ : ¬p
⊢ 1 ≤ b

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 1 ≤ a
hb : 1 ≤ b
h✝ : p
⊢ 1 ≤ a

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 1 ≤ a
hb : 1 ≤ b
h✝ : ¬p
⊢ 1 ≤ b
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : a ≤ 1
hb : b ≤ 1
h✝ : p
⊢ a ≤ 1

pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : a ≤ 1
hb : b ≤ 1
h✝ : ¬p
⊢ b ≤ 1

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : a ≤ 1
hb : b ≤ 1
h✝ : p
⊢ a ≤ 1

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : a ≤ 1
hb : b ≤ 1
h✝ : ¬p
⊢ b ≤ 1
Module: Mathlib.Algebra.Notation.Lemmas

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

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

Tactic:
<;>

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

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 1 < a
hb : 1 < b
h✝ : ¬p
⊢ 1 < b
Module: Mathlib.Algebra.Notation.Lemmas

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

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

Tactic:
<;>

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

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : a < 1
hb : b < 1
h✝ : ¬p
⊢ b < 1
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case hC
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
x✝ : A
n✝ : ℕ
⊢ ((((mapAlgHom f).comp (mapAlgHom g)).comp CAlgHom) x✝).coeff n✝ = (((mapAlgHom (f.comp g)).comp CAlgHom) x✝).coeff n✝

pp: case hX
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
n✝ : ℕ
⊢ (((mapAlgHom f).comp (mapAlgHom g)) X).coeff n✝ = ((mapAlgHom (f.comp g)) X).coeff n✝

Tactic:
<;>

Goal state after:
case hC
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
x✝ : A
n✝ : ℕ
⊢ ((((mapAlgHom f).comp (mapAlgHom g)).comp CAlgHom) x✝).coeff n✝ = (((mapAlgHom (f.comp g)).comp CAlgHom) x✝).coeff n✝

case hX
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
n✝ : ℕ
⊢ (((mapAlgHom f).comp (mapAlgHom g)) X).coeff n✝ = ((mapAlgHom (f.comp g)) X).coeff n✝
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case refine_1
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
⊢ (aeval p).comp (aeval q) = AlgHom.id R R[X]

pp: case refine_2
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
⊢ (aeval q).comp (aeval p) = AlgHom.id R R[X]

Tactic:
<;>

Goal state after:
case refine_1
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
⊢ (aeval p).comp (aeval q) = AlgHom.id R R[X]

case refine_2
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
⊢ (aeval q).comp (aeval p) = AlgHom.id R R[X]
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
f : R[X]
G : Type u_3
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G R A
g : G
x : A
⊢ (aeval (g • x)) f = g • (aeval x) f

Tactic:
rw [← MulSemiringAction.toAlgHom_apply R, aeval_algHom_apply, MulSemiringAction.toAlgHom_apply]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r p * r - eval r p * r = 0

pp: R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ Commute r r

Tactic:
<;>

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r p * r - eval r p * r = 0

R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ Commute r r