mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
x✝ : x ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx : ↑f ⟨x, hfx⟩ = ↑g ⟨x, hgx⟩
this : ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain), ⟨c • x, ⋯⟩ = c • ⟨x, hfx⟩
⊢ σ c • ↑f ⟨x, hfx⟩ = σ c • ↑g ⟨x, hgx⟩

Tactic:
hx

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
x✝ : x ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx : ↑f ⟨x, hfx⟩ = ↑g ⟨x, hgx⟩
this : ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain), ⟨c • x, ⋯⟩ = c • ⟨x, hfx⟩
⊢ σ c • ↑g ⟨x, hgx⟩ = σ c • ↑g ⟨x, hgx⟩
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f : E →ₛₗ.[σ] F
x : ↥⊥.domain
y : ↥f.domain
h : ↑x = ↑y
hx : x = 0
hy : y = 0
⊢ 0 = ↑f 0

Tactic:
map_zero

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f : E →ₛₗ.[σ] F
x : ↥⊥.domain
y : ↥f.domain
h : ↑x = ↑y
hx : x = 0
hy : y = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
x : V
⊢ f x = 0 → f (g x) = 0

Tactic:
hx

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
x : V
hx : f x = 0
⊢ f (g x) = 0
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
x : V
hx : f x = 0
⊢ g 0 = 0

Tactic:
map_zero

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
x : V
hx : f x = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ finrank K V ≤ 1 ↔ ∃ v, ∀ (w : V), ∃ c, c • v = w

Tactic:
← rank_le_one_iff,

Goal state after:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ finrank K V ≤ 1 ↔ Module.rank K V ≤ 1
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
x✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) 0) * a✝) = 0

Tactic:
map_zero

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
x✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar 0 * a✝) = 0
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_assoc
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f (a✝ + b✝ + c✝) = liftFun R X f (a✝ + (b✝ + c✝))

Tactic:
change _ + _ + _ = _ + (_ + _)

Goal state after:
case add_assoc
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f a✝ + liftFun R X f b✝ + liftFun R X f c✝ = liftFun R X f a✝ + (liftFun R X f b✝ + liftFun R X f c✝)
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
h' : f + g = 0
x : E
this : f.domain = ⊤ ∧ g.domain = ⊤
⊢ x ∈ (-f).domain ↔ x ∈ g.domain

Tactic:
rw [neg_domain, this.1, this.2]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case a
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n

pp: case a
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n.minFac

Tactic:
hx

Goal state after:
case a
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n.minFac * (x + 2)

case a
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n.minFac
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case left
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
⊢ x ∈ f.domain → x ∈ g.domain

Tactic:
hx

Goal state after:
case left
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
⊢ x ∈ g.domain
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ ↑f ⟨x, hx⟩ = ↑g ⟨y, hy⟩

Tactic:
image_iff

Goal state after:
case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ (y, ↑f ⟨x, hx⟩) ∈ g.graph
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
⊢ x ∈ f.graph → x ∈ g.graph

Tactic:
hx

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : x ∈ f.graph
⊢ x ∈ g.graph
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
inst✝³ : Module S F
G : Type u_6
inst✝² : AddCommGroup G
inst✝¹ : Module T G
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
hadd : ↑v + ↑w ∈ map (LinearMap.fst R E F) g
hvw : (↑v + ↑w, valFromGraph hg hadd) ∈ g
hvw' : (↑v, valFromGraph hg ⋯) + (↑w, valFromGraph hg ⋯) ∈ g
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯

Tactic:
rw [Prod.mk_add_mk] at hvw'

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
inst✝³ : Module S F
G : Type u_6
inst✝² : AddCommGroup G
inst✝¹ : Module T G
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
hadd : ↑v + ↑w ∈ map (LinearMap.fst R E F) g
hvw : (↑v + ↑w, valFromGraph hg hadd) ∈ g
hvw' : (↑v + ↑w, valFromGraph hg ⋯ + valFromGraph hg ⋯) ∈ g
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
l : Filter α
a : α
β : Type u_1
inst✝ : PartialOrder β
f : α → β
h₁ : IsMinFilter f l a
h₂ : IsMaxFilter f l a
⊢ f =ᶠ[l] fun x ↦ f a

Tactic:
by
  filter_upwards [h₁, h₂] using by grind

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
⊢ x ∈ Ioo a c → x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
hx

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
⊢ x ∈ Ico a c → x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
hx

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
⊢ x ∈ Ioc a c → x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
hx

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

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

Tactic:
hx

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Icc a c
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

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

Tactic:
hx

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

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

Tactic:
hx

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ici a
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ #(p * q).toFinsupp.coeff.support = #(p.toFinsupp * q.toFinsupp).coeff.support

Tactic:
toFinsupp_mul

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ #(p.toFinsupp * q.toFinsupp).coeff.support = #(p.toFinsupp * q.toFinsupp).coeff.support
Module: Mathlib.Order.Filter.Extr

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

Tactic:
hx

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

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

Tactic:
hx

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
p : R[ℕ]
⊢ (p * AddMonoidAlgebra.single 0 a).coeff n = p.coeff n * a

Tactic:
exact p.coeff_mul_single_zero a n

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

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : Add A
inst✝² : Add B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
⊢ (f * g).coeff.support.sup degb ≤ f.coeff.support.sup degb + g.coeff.support.sup degb

Tactic:
grw [support_coeff_mul_subset, Finset.sup_add_le]
  rintro _fd fds _gd gds
  grw [degbm, ← Finset.le_sup fds, ← Finset.le_sup gds]

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

Goal state before:
pp: case refine_2
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)
n : ℕ
f : R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Tactic:
· exact degtm _ _

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid 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)
m : Multiset R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Tactic:
· exact degtm _ _

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

Goal state before:
pp: case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ p.coeff.support, b ≠ ap → (∑ x ∈ q.coeff.support, if b + x = ap + aq then p.coeff b * q.coeff x else 0) = 0

pp: case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.coeff.support → (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = 0

Tactic:
· refine fun a ha hne => Finset.sum_eq_zero (fun a' ha' => if_neg <| fun he => ?_)
    apply_fun D at he
    simp_rw [hadd] at he
    have := addLeftMono_of_addLeftStrictMono B
    exact (add_lt_add_of_lt_of_le (((Finset.le_sup ha).trans hp).lt_of_ne <| hD.ne_iff.2 hne)
      <| (Finset.le_sup ha').trans hq).ne he

Goal state after:
case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.coeff.support → (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ (p * q).coeff (ap + aq) = p.coeff ap * q.coeff aq

Tactic:
by
  classical
  simp_rw [coeff_mul, Finsupp.sum]
  rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl]
  · refine fun a ha hne => if_neg (fun he => ?_)
    apply_fun D at he; simp_rw [hadd] at he
    exact (add_lt_add_right (((Finset.le_sup ha).trans hq).lt_of_ne <| hD.ne_iff.2 hne) _).ne he
  · intro h; rw [if_pos rfl, Finsupp.notMem_support_iff.1 h, mul_zero]
  · refine fun a ha hne => Finset.sum_eq_zero (fun a' ha' => if_neg <| fun he => ?_)
    apply_fun D at he
    simp_rw [hadd] at he
    have := addLeftMono_of_addLeftStrictMono B
    exact (add_lt_add_of_lt_of_le (((Finset.le_sup ha).trans hp).lt_of_ne <| hD.ne_iff.2 hne)
      <| (Finset.le_sup ha').trans hq).ne he
  · refine fun h => Finset.sum_eq_zero (fun a _ => ite_eq_right_iff.mpr <| fun _ => ?_)
    rw [Finsupp.notMem_support_iff.mp h, zero_mul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ eval (↑n) (map f p) = f (eval (↑n) p)

Tactic:
induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]

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

Goal state before:
pp: case hbc
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ b < p.natDegree

Tactic:
exact lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt, zero_mul]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.natDegree < n
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:
simp only [← sum_single_index (h := fun (_ : α) m ↦ g m) (a := a) (b := f a) hg]
  apply single_le_sum _ (fun _ m ↦ h m)

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)) = ((algebraMap B C).comp (algebraMap A B)) (p.coeff 0)

Tactic:
RingHom.comp_apply

Goal state after:
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)) = (algebraMap B C) ((algebraMap A B) (p.coeff 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 ι
⊢ x i < a ∨ toLex x = toLex (update x i a) ↔ x i < a ∨ x i = a

Tactic:
toLex_inj,

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ x i < a ∨ x = update x i a ↔ x i < a ∨ x i = 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 ι
⊢ a < x i ∨ toLex (update x i a) = toLex x ↔ a < x i ∨ a = x i

Tactic:
toLex_inj,

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ a < x i ∨ update x i a = x ↔ a < x i ∨ a = x i
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
n : ℕ
⊢ C a * X s ^ n = (monomial (Finsupp.single s n)) a

Tactic:
rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]

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₁
p : MvPolynomial σ R
x : σ →₀ ℕ
⊢ coeff x ((map f) p) ≠ 0 → coeff x p ≠ 0

Tactic:
hx

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : coeff x ((map f) p) ≠ 0
⊢ coeff x p ≠ 0
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₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : coeff x p = 0
⊢ f 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : coeff x p = 0
⊢ 0 = 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case H₂
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ⇑f
x : σ →₀ ℕ
⊢ coeff x p ≠ 0 → coeff x ((map f) p) ≠ 0

Tactic:
hx

Goal state after:
case H₂
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ⇑f
x : σ →₀ ℕ
hx : coeff x p ≠ 0
⊢ coeff x ((map f) p) ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
⊢ x ∈ coeffsIn σ M → ∀ n ∈ coeffsIn σ N, x * n ∈ coeffsIn σ (M * N)

Tactic:
hx

Goal state after:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
⊢ ∀ n ∈ coeffsIn σ N, x * n ∈ coeffsIn σ (M * N)
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
⊢ x ∈ (p - ((monomial d) c - (monomial d') c)).support → x ∈ p.support.erase d ∪ {d'}

Tactic:
hx

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
⊢ x ∈ p.support.erase d ∪ {d'}