mathlib-initiative/mathlib-tactics huggingface dataset:
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
t' : R
a : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun (t' • a) =
    (MonoidHom.id R) t' •
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun a

Tactic:
by

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)
⊢ (↑x, ↑g.toLinearPMap x) ∈ g

Tactic:
by

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
a₁ a₂ : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun (a₁ * a₂) =
    (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun a₁ *
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun a₂

Tactic:
by

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
⊢ (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) =
    f

Tactic:
by

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 : R[M] →ₙₐ[R] A
⊢ (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) =
    F

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
h : IsMinOn f s a
⊢ f a ∈ lowerBounds (f '' s)

Tactic:
by

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
f : A[M]
⊢ (singleOneRingHom.comp (algebraMap R A)) r * f = f * (singleOneRingHom.comp (algebraMap R A)) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
⊢ IsGLB {x | ∃ x_1 ∈ s, f x_1 = x} (f a)

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
h : IsMaxOn f s a
⊢ f a ∈ upperBounds (f '' s)

Tactic:
by

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

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
⊢ f =ᶠ[l] fun x ↦ f a

Tactic:
by

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
⊢ (↑↑singleOneRingHom).toFun ((algebraMap R A) r) = (algebraMap R A[M]) r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_7
inst✝¹ : CommSemiring R
inst✝ : Monoid M
m : M
r : R
⊢ single m r = (algebraMap R R[M]) r * (of R M) m

Tactic:
by

Goal state after:
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
m : M
r : R
⊢ single m ((algebraMap R A) r) = (algebraMap R A[M]) r * (of A M) m

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
δ : Type x
inst✝ : Preorder β
f : α → β
s : Set α
a : α
t : Set δ
g : δ → α
b : δ
hf : IsMinOn f s a
hg : MapsTo g t s
ha : g b = a
y : δ
hy : y ∈ t
⊢ y ∈ {x | (fun x ↦ (f ∘ g) b ≤ (f ∘ g) x) x}

Tactic:
by

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
inst✝ : Subsingleton M
r : R
⊢ (uniqueRingEquiv M).toFun ((algebraMap R A[M]) r) = (algebraMap R A) r

Tactic:
by

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_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ x_fst ∈ map (LinearMap.fst R E F) g

Tactic:
by

Goal state after:
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
⊢ (uniqueAlgEquiv R M).symm a = single 1 a

Tactic:
by

Goal state after:
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
m : M
⊢ ((uniqueAlgEquiv R M).symm a).coeff m = a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMaxFilter g l a
⊢ IsMinFilter (fun x ↦ f x - g x) l a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMinFilter g l a
⊢ IsMaxFilter (fun x ↦ f x - g x) l a

Tactic:
by

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
⊢ curryRingEquiv.toFun ((algebraMap R A[M × N]) r) = (algebraMap R A[N][M]) r

Tactic:
by

Goal state after:
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
m : M
n : N
a : A
⊢ (curryAlgEquiv R) (single (m, n) a) = single m (single n a)

Tactic:
by

Goal state after:
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
m : M
n : N
a : A
⊢ (curryAlgEquiv R).symm (single m (single n a)) = single (m, n) a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsMinOn f s a
hg : IsMaxOn g s a
⊢ IsMinOn (fun x ↦ f x - g x) s a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsMaxOn f s a
hg : IsMinOn g s a
⊢ IsMaxOn (fun x ↦ f x - g x) s a

Tactic:
by

Goal state after:
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
F : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
r : R
⊢ mapDomain (⇑f) ((algebraMap R A[M]) r) = (algebraMap R A[N]) r

Tactic:
by

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
⊢ g.toLinearPMap.graph = g

Tactic:
by

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✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : A →ₐ[R] B
g : M →* B
h_comm : ∀ (x : A) (y : M), Commute (f x) (g y)
⊢ ∀ (r : R), (↑↑(liftNCRingHom (↑f) g h_comm)).toFun ((algebraMap R A[M]) r) = (algebraMap R B) r

Tactic:
by

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
⊢ g.toLinearPMap.toFun.range = map (LinearMap.snd R E F) g

Tactic:
by

Goal state after:
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
φ₁ φ₂ : A[M] →ₐ[R] B
single_one_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1)
single_one_left : φ₁.comp singleOneAlgHom = φ₂.comp singleOneAlgHom
⊢ φ₁ = φ₂

Tactic:
by

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)
⊢ IsMaxOn f (Ioo a c) b

Tactic:
by

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

Tactic:
by

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
⊢ f.inverse.domain = f.toFun.range

Tactic:
by

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

Tactic:
by

Goal state after:
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
F : M →* A
f : R[M]
⊢ ((lift R A M) F) f = f.coeff.sum fun a b ↦ b • F a

Tactic:
by

Goal state after:
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
F : M →* A
a : M
b : R
⊢ ((lift R A M) F) (single a b) = b • F a

Tactic:
by

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 = ⊥
x : F × E
hv : x ∈ Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph
hv' : x.1 = 0
⊢ x.2 = 0

Tactic:
by

Goal state after:
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
F : M →* A
m : M
⊢ ((lift R A M) F) ((of R M) m) = F m

Tactic:
by

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 (Icc a b)
h₁ : AntitoneOn f (Ico b c)
⊢ IsMaxOn f (Ico a c) b

Tactic:
by

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 = ⊥
⊢ f.inverse.graph = Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph

Tactic:
by

Goal state after:
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
F : R[M] →ₐ[R] A
f : R[M]
⊢ F f = f.coeff.sum fun a b ↦ b • F (single a 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Monoid M
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f : M →* A
x : R[M]
⊢ ((lift S A M) f) ((mapRingHom M (algebraMap R S)) x) = ((lift R A M) f) x

Tactic:
by

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 = ⊥
⊢ f.inverse.toFun.range = f.domain

Tactic:
by

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 (Icc b c)
⊢ IsMaxOn f (Ioc a c) b

Tactic:
by

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✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
⊢ ∀ (r : R), (↑↑(mapDomainRingHom A f)).toFun ((algebraMap R A[M]) r) = (algebraMap R A[N]) r

Tactic:
by

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 = ⊥
x : ↥f.domain
⊢ (↑f x, ↑x) ∈ f.inverse.graph

Tactic:
by

Goal state after:
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
⊢ mapDomainAlgHom R A (MonoidHom.id M) = AlgHom.id R A[M]

Tactic:
by

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
⊢ ↑f.inverse y = ↑x

Tactic:
by

Goal state after:
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
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
⊢ mapDomainAlgHom R A (g.comp f) = (mapDomainAlgHom R A g).comp (mapDomainAlgHom R A f)

Tactic:
by

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 (Icc a b)
h₁ : AntitoneOn f (Icc b c)
⊢ IsMaxOn f (Icc a c) b

Tactic:
by

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

Tactic:
by

Goal state after:
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
f : A[M]
n : N
⊢ ((domCongr R A e) f).coeff n = f.coeff (e.symm n)

Tactic:
by

Goal state after:
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
x : A[M]
⊢ ((domCongr R A e) x).coeff.support = Finset.map (↑e).toEmbedding x.coeff.support

Tactic:
by

Goal state after:
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
a : A
⊢ (domCongr R A e) (single m a) = single (e m) a

Tactic:
by

Goal state after:
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
⊢ (domCongr R A e).toLinearMap ∘ₗ lsingle m = lsingle (e m)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p + q).coeff n = p.coeff n + q.coeff n

Tactic:
by

Goal state after:
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)
⊢ IsMaxOn f (Ioi a) b

Tactic:
by

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

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]
⊢ (r • p).support ⊆ p.support

Tactic:
by

Goal state after:
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
⊢ domCongr R A (MulEquiv.refl M) = AlgEquiv.refl

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
f : N ≃* O
⊢ (domCongr R A e).trans (domCongr R A f) = domCongr R A (e.trans f)

Tactic:
by

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✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
⊢ domCongr R A 1 = 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
x✝¹ x✝ : MulAut M
⊢ domCongr R A (x✝¹ * x✝) = domCongr R A x✝¹ * domCongr R A x✝

Tactic:
by

Goal state after:
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
⊢ (mapDomainRingHom A f).comp (algebraMap R A[M]) = algebraMap R A[N]

Tactic:
by

Goal state after:
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
⊢ (mapRingHom M f).comp (algebraMap R R[M]) = (algebraMap S S[M]).comp f

Tactic:
by

Goal state after: