mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝ : X
⊢ (⇑(((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X)) (FreeMonoid.lift (ι R))).comp
            ((lift R) fun x ↦ (MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))) ∘
        ι R)
      x✝ =
    (⇑(AlgHom.id R (FreeAlgebra R X)) ∘ ι R) x✝

Tactic:
;

Goal state after:
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : X
⊢ (⇑(((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X)) (FreeMonoid.lift (ι R))).comp
            ((lift R) fun x ↦ (MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))) ∘
        ι R)
      x✝ =
    (⇑(AlgHom.id R (FreeAlgebra R X)) ∘ ι R) x✝
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : FreeAlgebra R X
hx : x ∈ ⊤
⊢ x ∈ S

Tactic:
;

Goal state after:
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : FreeAlgebra R X
hx : x ∈ ⊤
⊢ x ∈ S
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:
;

Goal state after:
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
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsRightCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (f * single x r).coeff.support ↔ a✝ ∈ Finset.map (mulRightEmbedding x) f.coeff.support

Tactic:
;

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsRightCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (f * single x r).coeff.support ↔ a✝ ∈ Finset.map (mulRightEmbedding x) f.coeff.support
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsRightCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
⊢ (f * single x r).coeff.support = Finset.map (mulRightEmbedding x) f.coeff.support

Tactic:
classical ext; simp [support_coeff_mul_single_eq_image f hr (.all x)]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R
n✝ : ℕ
⊢ (((mapRingHom f).comp C) x✝).coeff n✝ = ((C.comp f) x✝).coeff n✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R
n✝ : ℕ
⊢ (((mapRingHom f).comp C) x✝).coeff n✝ = ((C.comp f) x✝).coeff n✝
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsLeftCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (single x r * f).coeff.support ↔ a✝ ∈ Finset.map (mulLeftEmbedding x) f.coeff.support

Tactic:
;

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsLeftCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (single x r * f).coeff.support ↔ a✝ ∈ Finset.map (mulLeftEmbedding x) f.coeff.support
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n a✝ : ℕ
k : ℕ := a✝
h✝¹ : ¬n < k * k
h✝ : ¬k ∣ n
⊢ n.sqrt - a✝ < n.sqrt + 2 - a✝

Tactic:
;

Goal state after:
n a✝ : ℕ
k : ℕ := a✝
h✝¹ : ¬n < k * k
h✝ : ¬k ∣ n
⊢ n.sqrt - a✝ < n.sqrt + 2 - a✝
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n a✝ : ℕ
k : ℕ := a✝
h✝¹ : ¬n < k * k
h✝ : ¬k ∣ n
⊢ ¬n < k * k

Tactic:
;

Goal state after:
n a✝ : ℕ
k : ℕ := a✝
h✝¹ : ¬n < k * k
h✝ : ¬k ∣ n
⊢ ¬n < k * k
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✝ : F
⊢ x✝ ∈ Submodule.map (LinearMap.snd R E F) f.graph ↔ x✝ ∈ f.toFun.range

Tactic:
;

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 : E →ₗ.[R] F
x✝ : F
⊢ x✝ ∈ Submodule.map (LinearMap.snd R E F) f.graph ↔ x✝ ∈ f.toFun.range
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ x = 0

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ x = 0
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
⊢ ↑0 = 0

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
⊢ ↑0 = 0
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: m p : ℕ
pp : Prime p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p

Tactic:
;

Goal state after:
m p : ℕ
pp : Prime p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p

Tactic:
;

Goal state after:
m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).left
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x

Tactic:
exact CharP.cast_eq_zero_iff R (ringChar R)

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

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬0 < 0

Tactic:
;

Goal state after:
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬0 < 0
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : n < 2
h1 : n = n.minFac
⊢ minFac 1 ≤ 1 / minFac 1

Tactic:
minFac_one,

Goal state after:
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = n.minFac
⊢ 1 ≤ 1 / 1
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
⊢ n.minFac = 1 ↔ n = 1

Tactic:
by
  constructor
  · intro h
    by_contra hn
    have := minFac_prime hn
    rw [h] at this
    exact not_prime_one this
  · rintro rfl
    simp [minFac, minFacAux]

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

Goal state after:
case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
this : CharP R 0
⊢ max 0 1 = 1
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.toLinearPMap x = valFromGraph hg ⋯

Tactic:
classical
  change (if hg : _ then g.toLinearPMapAux hg else 0) x = _
  rw [dif_pos]
  · rfl
  · exact hg

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✝⁵ : Semiring R
inst✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : M →ₙ* A
x✝ : M
⊢ ((fun F ↦ F.toMulHom.comp (ofMagma R M))
        ((fun f ↦
            let __AddMonoidHom := (liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom;
            { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
          f))
      x✝ =
    f x✝

Tactic:
;

Goal state after:
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✝⁵ : Semiring R
inst✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : M →ₙ* A
x✝ : M
⊢ ((fun F ↦ F.toMulHom.comp (ofMagma R M))
        ((fun f ↦
            let __AddMonoidHom := (liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom;
            { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
          f))
      x✝ =
    f x✝
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✝⁵ : Semiring R
inst✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
F : R[M] →ₙₐ[R] A
x✝ : M
⊢ (((fun f ↦
                let __AddMonoidHom :=
                  (liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom;
                { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
              ((fun F ↦ F.toMulHom.comp (ofMagma R M)) F)).toMulHom.comp
        (ofMagma R M))
      x✝ =
    (F.toMulHom.comp (ofMagma R M)) x✝

Tactic:
;

Goal state after:
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✝⁵ : Semiring R
inst✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
F : R[M] →ₙₐ[R] A
x✝ : M
⊢ (((fun f ↦
                let __AddMonoidHom :=
                  (liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom;
                { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
              ((fun F ↦ F.toMulHom.comp (ofMagma R M)) F)).toMulHom.comp
        (ofMagma R M))
      x✝ =
    (F.toMulHom.comp (ofMagma R M)) x✝
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
f : A[M]
a✝ : M
⊢ ((singleOneRingHom.comp (algebraMap R A)) r * f).coeff a✝ = (f * (singleOneRingHom.comp (algebraMap R A)) r).coeff a✝

Tactic:
;

Goal state after:
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
f : A[M]
a✝ : M
⊢ ((singleOneRingHom.comp (algebraMap R A)) r * f).coeff a✝ = (f * (singleOneRingHom.comp (algebraMap R A)) r).coeff a✝
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 : A[M]
a✝ : M
⊢ (r • a).coeff a✝ = ((singleOneRingHom.comp (algebraMap R A)) r * a).coeff a✝

Tactic:
;

Goal state after:
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 : A[M]
a✝ : M
⊢ (r • a).coeff a✝ = ((singleOneRingHom.comp (algebraMap R A)) r * a).coeff a✝
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
⊢ ((↑↑singleOneRingHom).toFun ((algebraMap R A) r)).coeff a✝ = ((algebraMap R A[M]) r).coeff a✝

Tactic:
;

Goal state after:
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
⊢ ((↑↑singleOneRingHom).toFun ((algebraMap R A) r)).coeff a✝ = ((algebraMap R A[M]) r).coeff a✝
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:
;

Goal state after:
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✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: 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
inst✝ : Subsingleton M
a : A
a✝ : M
⊢ ((uniqueAlgEquiv R M).symm a).coeff a✝ = (single 1 a).coeff a✝

Tactic:
;

Goal state after:
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
inst✝ : Subsingleton M
a : A
a✝ : M
⊢ ((uniqueAlgEquiv R M).symm a).coeff a✝ = (single 1 a).coeff a✝
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✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* A
x✝ : M
⊢ ((fun f ↦ (↑f).comp (of R M)) ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) f)) x✝ = f x✝

Tactic:
;

Goal state after:
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✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* A
x✝ : M
⊢ ((fun f ↦ (↑f).comp (of R M)) ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) f)) x✝ = f x✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case single_one_right
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✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
F : R[M] →ₐ[R] A
m✝ : M
⊢ ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) ((fun f ↦ (↑f).comp (of R M)) F)) (single m✝ 1) = F (single m✝ 1)

Tactic:
;

Goal state after:
case single_one_right
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✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
F : R[M] →ₐ[R] A
m✝ : M
⊢ ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) ((fun f ↦ (↑f).comp (of R M)) F)) (single m✝ 1) = F (single m✝ 1)
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✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
x✝ : R
a✝ : N
⊢ ((mapDomainRingEquiv A e).toFun ((algebraMap R A[M]) x✝)).coeff a✝ = ((algebraMap R A[N]) x✝).coeff a✝

Tactic:
;

Goal state after:
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✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
x✝ : R
a✝ : N
⊢ ((mapDomainRingEquiv A e).toFun ((algebraMap R A[M]) x✝)).coeff a✝ = ((algebraMap R A[N]) x✝).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
m : M
x✝ : A
a✝ : N
⊢ (((domCongr R A e).toLinearMap ∘ₗ lsingle m) x✝).coeff a✝ = ((lsingle (e m)) x✝).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
m : M
x✝ : A
a✝ : N
⊢ (((domCongr R A e).toLinearMap ∘ₗ lsingle m) x✝).coeff a✝ = ((lsingle (e m)) x✝).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: 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
a✝¹ : A[M]
a✝ : M
⊢ ((domCongr R A (MulEquiv.refl M)) a✝¹).coeff a✝ = (AlgEquiv.refl a✝¹).coeff a✝

Tactic:
;

Goal state after:
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
a✝¹ : A[M]
a✝ : M
⊢ ((domCongr R A (MulEquiv.refl M)) a✝¹).coeff a✝ = (AlgEquiv.refl a✝¹).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
x✝ : R
a✝ : N
⊢ (((mapDomainRingHom A f).comp (algebraMap R A[M])) x✝).coeff a✝ = ((algebraMap R A[N]) x✝).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
x✝ : R
a✝ : N
⊢ (((mapDomainRingHom A f).comp (algebraMap R A[M])) x✝).coeff a✝ = ((algebraMap R A[N]) x✝).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_7
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Monoid M
f : R →+* S
x✝ : R
a✝ : M
⊢ (((mapRingHom M f).comp (algebraMap R R[M])) x✝).coeff a✝ = (((algebraMap S S[M]).comp f) x✝).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_7
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Monoid M
f : R →+* S
x✝ : R
a✝ : M
⊢ (((mapRingHom M f).comp (algebraMap R R[M])) x✝).coeff a✝ = (((algebraMap S S[M]).comp f) x✝).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

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

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
f : A →ₐ[R] B
m : M
a : A
a✝ : M
⊢ ((mapAlgHom M f) (single m a)).coeff a✝ = (single m (f a)).coeff a✝
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
q : R[X]
n : ℕ
p : R[ℕ]
⊢ ({ toFinsupp := p } * q).coeff n = ∑ x ∈ antidiagonal n, { toFinsupp := p }.coeff x.1 * q.coeff x.2

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
q : R[X]
n : ℕ
p : R[ℕ]
⊢ ({ toFinsupp := p } * q).coeff n = ∑ x ∈ antidiagonal n, { toFinsupp := p }.coeff x.1 * q.coeff x.2
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: 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
e₁ : A ≃ₐ[R] B
e₂ : B ≃ₐ[R] C
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M (e₁.trans e₂)) a✝¹).coeff a✝ = (((mapAlgEquiv R M e₁).trans (mapAlgEquiv R M e₂)) a✝¹).coeff a✝

Tactic:
;

Goal state after:
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
e₁ : A ≃ₐ[R] B
e₂ : B ≃ₐ[R] C
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M (e₁.trans e₂)) a✝¹).coeff a✝ = (((mapAlgEquiv R M e₁).trans (mapAlgEquiv R M e₂)) a✝¹).coeff a✝
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✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra R C
inst✝¹ : Monoid M
inst✝ : Monoid N
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M 1) a✝¹).coeff a✝ = (1 a✝¹).coeff a✝

Tactic:
;

Goal state after:
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✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra R C
inst✝¹ : Monoid M
inst✝ : Monoid N
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M 1) a✝¹).coeff a✝ = (1 a✝¹).coeff a✝
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✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra R C
inst✝¹ : Monoid M
inst✝ : Monoid N
x y : A ≃ₐ[R] A
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M (x * y)) a✝¹).coeff a✝ = ((mapAlgEquiv R M x * mapAlgEquiv R M y) a✝¹).coeff a✝

Tactic:
;

Goal state after:
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✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra R C
inst✝¹ : Monoid M
inst✝ : Monoid N
x y : A ≃ₐ[R] A
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M (x * y)) a✝¹).coeff a✝ = ((mapAlgEquiv R M x * mapAlgEquiv R M y) a✝¹).coeff a✝
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
⊢ IsMaxOn D (↑s) (Function.invFun D (D a))

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
⊢ IsMaxOn D (↑s) (Function.invFun D (D a))
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
a✝ : α
⊢ a✝ ∈ ↑s → a✝ ∈ {x | (fun x ↦ D x ≤ D a) x}

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
a✝ : α
⊢ a✝ ∈ ↑s → a✝ ∈ {x | (fun x ↦ D x ≤ D a) x}