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

Goal state before:
pp: case add_compat_left
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f b✝ + liftFun R X f c✝ = liftFun R X f (b✝ + c✝)

pp: case add_compat_right
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)

pp: case mul_compat_left
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

pp: case mul_compat_right
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)

Tactic:
rfl

Goal state after:
case add_compat_right
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)

case mul_compat_left
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

case mul_compat_right
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_compat_right
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ + liftFun R X f b✝ = liftFun R X f (c✝ + b✝)

pp: case mul_compat_left
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

pp: case mul_compat_right
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)

Tactic:
rfl

Goal state after:
case mul_compat_left
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

case mul_compat_right
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mul_compat_left
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f b✝ * liftFun R X f c✝ = liftFun R X f (b✝ * c✝)

pp: case mul_compat_right
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)

Tactic:
rfl

Goal state after:
case mul_compat_right
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mul_compat_right
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
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ * liftFun R X f b✝ = liftFun R X f (c✝ * b✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.mk
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
x✝ : FreeAlgebra R X
a✝¹ : Pre R X
y✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.liftOn (Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝) (liftFun R X f) ⋯ =
    (Quot.mk (Rel R X) a✝¹).liftOn (liftFun R X f) ⋯ * (Quot.mk (Rel R X) a✝).liftOn (liftFun R X f) ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.mk
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
x✝ : FreeAlgebra R X
a✝¹ : Pre R X
y✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.liftOn (Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝) (liftFun R X f) ⋯ =
    (Quot.mk (Rel R X) a✝¹).liftOn (liftFun R X f) ⋯ + (Quot.mk (Rel R X) a✝).liftOn (liftFun R X f) ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case hz
E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑⟨x', hx'⟩ + ↑⟨c • x, ?m.146⟩ = ↑⟨x' + c • x, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: 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
x✝ : X
⊢ (liftAux R f) (Quot.mk (Rel R X) (Pre.of x✝)) = f x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.add
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = F (Quot.mk (Rel R X) a)
hb : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
⊢ (liftAux R (⇑F ∘ ι R)) (fa + fb) = F (fa + fb)

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.mul
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = F (Quot.mk (Rel R X) a)
hb : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
⊢ (liftAux R (⇑F ∘ ι R)) (fa * fb) = F (fa * fb)

Tactic:
grind

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ (p.sum fun e a ↦ (RingHom.id R) a * x ^ e) = p.sum fun e a ↦ a * x ^ e

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: 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
⊢ liftAux R f = { toFun := liftAux R, invFun := fun F ↦ ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
⊢ { toFun := liftAux R, invFun := fun F ↦ ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ }.symm F = ⇑F ∘ ι R

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: 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
x✝ : X
⊢ ({ toFun := liftAux R, invFun := fun F ↦ ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f)
      (Quot.mk (Rel R X) (Pre.of x✝)) =
    f x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: 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
x : X
⊢ ({ toFun := liftAux R, invFun := fun F ↦ ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f) (Quot.mk (Rel R X) (Pre.of x)) =
    f x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: 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
g : FreeAlgebra R X →ₐ[R] A
⊢ ⇑g ∘ ι R = f ↔ { toFun := liftAux R, invFun := fun F ↦ ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ }.symm g = f

Tactic:
rfl

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

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : y ∈ image (fun x_1 ↦ x * x_1) f.coeff.support
⊢ ∃ a ∈ f.coeff.support, x * a = y

Tactic:
grind

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

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : y ∈ image (fun x_1 ↦ x_1 * x) f.coeff.support
⊢ ∃ a ∈ f.coeff.support, a * x = y

Tactic:
grind

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ (C.comp f) a * X ^ n = C (f a) * X ^ n

Tactic:
rfl

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

Goal state before:
pp: case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 + 1 → 0 + 1 < p → ¬0 + 1 ∣ p
l : 0 + 1 < p
d : 0 + 1 ∣ p
⊢ 0 + 1 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
l : E →ₛₗ.[σ] F
hl : l ∈ c
x : ↥l.domain
⊢ ↑x = ↑⟨↑x, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
p : ℕ
inst✝ : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * e
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
⊢ 0 < p

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
p : ℕ
inst✝ : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * e
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = 1 * p

Tactic:
grind

Goal state after:
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 : E →ₗ.[R] F
x y : E
x' y' : F
hx : (x, x') ∈ f.graph
hy : (y, y') ∈ f.graph
hxy : x = y
⊢ x' = y'

Tactic:
grind

Goal state after:
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 : E →ₗ.[R] F
x y : E × F
hx : x ∈ f.graph
hy : y ∈ f.graph
hxy : x.1 = y.1
⊢ x.2 = y.2

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr
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 : E →ₗ.[R] F
x : E
h : ∃ y, (x, y) ∈ f.graph
⊢ x ∈ f.domain

Tactic:
grind

Goal state after:
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 : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
⊢ y = ↑f ⟨x, hx⟩ ↔ (x, y) ∈ f.graph

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
hp : CharP R 0
inst✝ : CharZero R
⊢ 1 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
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 : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : ↑f ⟨x, hx⟩ = y
⊢ (x, ↑f ⟨x, hx⟩) ∈ f.graph

Tactic:
exact f.mem_graph ⟨x, hx⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr
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 : E →ₗ.[R] F
y : F
h : ∃ x, (x, y) ∈ f.graph
⊢ y ∈ Set.range ↑f

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
this : CharP R 0
⊢ max 0 1 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
⊢ ExpChar R (ringExpChar R)

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists R
  rwa [ringExpChar.eq R q]

Goal state after:
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
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ ↑f ⟨x, hx✝⟩ = ↑f ⟨y, hx⟩

Tactic:
simp [hxy]

Goal state after:
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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (g.toLinearPMapAux ?hc) x = valFromGraph hg ⋯

Tactic:
rfl

Goal state after:
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
⊢ ∀ (a_1 : α), f a ≤ f a_1 → f a_1 ≤ f a → f a_1 = f a

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
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
r : R
a✝ : M
⊢ (Finsupp.single 1 ((algebraMap R A) r)) a✝ = ((algebraMap R A[M]) r).coeff a✝

Tactic:
rfl

Goal state after:
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 : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
y : ↥f.inverse.domain
x : ↥f.domain
hxy : ↑f x = ↑y
this : (↑f x, ↑x) ∈ f.inverse.graph
⊢ ↑f.inverse y = ↑x

Tactic:
grind

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
n : ℕ
⊢ (r • p).coeff n = r • p.coeff n

Tactic:
rfl

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:
classical
  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.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬n ∉ p.degree
hn : p.degree = some n
⊢ some n = ↑(WithBot.unbotD 0 (some n))

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
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)
s : Finset ι
f : ι → R[A]
⊢ ∑ i ∈ s, (f i).coeff.support.inf degt = (Multiset.map ((fun f ↦ f.coeff.support.inf degt) ∘ fun i ↦ f i) s.val).sum

Tactic:
rfl

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : n < 1 + p.natDegree
⊢ p.coeff n = p.coeff n

Tactic:
rfl

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

Goal state before:
pp: case mpr
m : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑m

Tactic:
rfl

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

Goal state before:
pp: case mpr
m : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑m

Tactic:
rfl

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : (p ^ n).natDegree ≤ n * p.natDegree
⊢ (p ^ n * p).natDegree ≤ (n + 1) * p.natDegree

Tactic:
Nat.succ_mul,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : (p ^ n).natDegree ≤ n * p.natDegree
⊢ (p ^ n * p).natDegree ≤ n * p.natDegree + p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| ((monomial p.natDegree) p.leadingCoeff + erase p.natDegree p - q).degree

Tactic:
← hq,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| ((monomial p.natDegree) p.leadingCoeff + erase p.natDegree p -
      ((monomial q.natDegree) q.leadingCoeff + erase q.natDegree q)).degree
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑2 = 2

Tactic:
rfl

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

Goal state before:
pp: R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑3 = 3

Tactic:
rfl

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

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

Tactic:
nontriviality
  rw [leadingCoeff_pow'] <;> simp

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

Goal state before:
pp: case h_of
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' : AddMonoidAlgebra R ℕ →+* S := ⋯
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := ⋯
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
⊢ ((↑f').comp (AddMonoidAlgebra.of R ℕ)) (Multiplicative.ofAdd 1) =
    ((↑g').comp (AddMonoidAlgebra.of R ℕ)) (Multiplicative.ofAdd 1)

Tactic:
simpa using! h₂

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
M : ↥R[x] → Prop
a : ↥R[x]
f : ∀ (p : R[X]), M ⟨(aeval x) p, ⋯⟩
p : R[X]
hp : (aeval x) p = ↑a
⊢ M a

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

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
x✝¹ x✝ : ↥R[x]
p : A
hp : p ∈ R[x]
q : A
hq : q ∈ R[x]
⊢ ⟨p, hp⟩ * ⟨q, hq⟩ = ⟨q, hq⟩ * ⟨p, hp⟩

Tactic:
obtain ⟨p', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hp

Goal state after:
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
x✝¹ x✝ : ↥R[x]
q : A
hq : q ∈ R[x]
p' : R[X]
hp : (aeval x).toRingHom p' ∈ R[x]
⊢ ⟨(aeval x).toRingHom p', hp⟩ * ⟨q, hq⟩ = ⟨q, hq⟩ * ⟨(aeval x).toRingHom p', hp⟩
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ f.coeff 0 = f.coeff Zero.zero

Tactic:
rfl

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 : R
⊢ AddMonoidAlgebra.single 0 ((algebraMap R A) r) = (algebraMap R (AddMonoidAlgebra A ℕ)) r

Tactic:
rfl

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:
rfl

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:
rfl

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
  simp +contextual [subset_iff]

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
⊢ y ∈ Set.range (embDomain f)

Tactic:
rw [mem_range_embDomain_iff]

Goal state after:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
⊢ ↑y.support ⊆ Set.range ⇑f