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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
⊢ ↑(iSup K) = ⋃ i, ↑(K i)

Tactic:
let s : Subalgebra R A :=
    { __ := Subsemiring.copy _ _ (Subsemiring.coe_iSup_of_directed dir).symm
      algebraMap_mem' := fun _ ↦ Set.mem_iUnion.2
        ⟨Classical.arbitrary ι, Subalgebra.algebraMap_mem _ _⟩ }

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
s : Subalgebra R A :=
  let __spread.0 := (⨆ i, (K i).toSubsemiring).copy (⋃ i, ↑(K i).toSubsemiring) ⋯;
  { toSubsemiring := __spread.0, algebraMap_mem' := ⋯ }
⊢ ↑(iSup K) = ⋃ i, ↑(K i)
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
this : ∀ (x y : R), x ≤ y → star x ≤ star y
⊢ star x ≤ star y → x ≤ y

Tactic:
simpa only [star_star] using this (star x) (star y)

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ 0 < star x ↔ 0 < x

Tactic:
by
  simpa using star_lt_star_iff (x := 0) (y := x)

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
h : ∀ a ∈ S, 1 ⊗ₜ[R] a * x = x * 1 ⊗ₜ[R] a
b : B
hb : b ∈ S
⊢ (Algebra.TensorProduct.comm R A B).symm (b ⊗ₜ[R] 1 * (Algebra.TensorProduct.comm R A B) x) =
    (Algebra.TensorProduct.comm R A B).symm ((Algebra.TensorProduct.comm R A B) x * b ⊗ₜ[R] 1)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
h : ∀ a ∈ S, a ⊗ₜ[R] 1 * (Algebra.TensorProduct.comm R A B) x = (Algebra.TensorProduct.comm R A B) x * a ⊗ₜ[R] 1
b : B
hb : b ∈ S
⊢ (Algebra.TensorProduct.comm R A B) (1 ⊗ₜ[R] b * x) = (Algebra.TensorProduct.comm R A B) (x * 1 ⊗ₜ[R] b)

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case e'_5
R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht : LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t
⊢ f '' t = range fun x ↦ f ↑x

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case mem
R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
x✝ : R
h✝ : x✝ ∈ range fun s ↦ star s * s
⊢ f x✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case zero
R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
⊢ f 0 ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case add
R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a✝¹ : f x✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a✝ : f y✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ f (x✝ + y✝) ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ (range fun i ↦ ↑(bW i)) = ⇑W.subtype '' range fun i ↦ bW i

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
w : ↥W
i : m
⊢ ((bW.sumQuot bQ).repr ↑w) (Sum.inl i) = (bW.repr w) i

Tactic:
by
  classical
  refine Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i) <;>
  aesop (add simp Finsupp.single_apply)

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case e'_1
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ (fun x ↦ x ∈ ∅) = fun x ↦ x ∈ ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
v : V
hv : v ∈ W
j : n
⊢ W.mkQ v = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case e'_4
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
e_1✝ : ↥∅ = ↑∅
⊢ (fun x ↦ x ∈ ∅) = fun x ↦ x ∈ ∅

Tactic:
aesop

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
f g : E →ₛₗ.[σ] F
EQ : f = g
x y : ↥f.domain
h : ↑x = ↑y
⊢ x = y

Tactic:
exact mod_cast h

Goal state after:
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
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
this : Nonempty (↥Q ≃ₗ[K] ↥Q')
⊢ ∀ (x : ↥W), ↑(f x) = (eQ.symm ≪≫ₗ f.prodCongr this.some ≪≫ₗ eQ') ↑x

Tactic:
aesop

Goal state after:
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
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K (↥W × ↥Q) = Module.rank K ↥Q' + Module.rank K ↥W

pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W < ℵ₀

Tactic:
Module.nonempty_linearEquiv_iff_rank_eq.mp ⟨eQ⟩,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K V = Module.rank K ↥Q' + Module.rank K ↥W

K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W < ℵ₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Commute on f)),
    (s.SupIndep fun i ↦ (f i).ker) → (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
⊢ ((insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker

Tactic:
replace ih : ker (Finset.noncommProd s f <| Set.Pairwise.mono (s.subset_insert i) comm) =
        ⨆ x ∈ s, ker (f x) := ih _ (h.subset (s.subset_insert i))

Goal state after:
case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ ((insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker
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
S : Submodule K V
hS : finrank K ↥S = 1
⊢ S ≠ ⊥

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ 0 + Quot.mk (Rel R X) a✝ = Quot.mk (Rel R X) a✝

Tactic:
exact Quot.sound Rel.zero_add

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)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x : E
⊢ x ∈ sSup (domain '' c) ↔ ∃ f ∈ c, x ∈ f.domain

Tactic:
Submodule.mem_sSup_of_directed (hnonempty.image _)
    (DirectedOn.mono_comp LinearPMap.domain_mono.monotone hc)

Goal state after:
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)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x : E
⊢ (∃ y ∈ domain '' c, x ∈ y) ↔ ∃ f ∈ c, x ∈ f.domain
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
h : (x, y) ∈ f.graph
⊢ x ∈ f.domain

Tactic:
mem_domain_iff

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 : E
y : F
h : (x, y) ∈ f.graph
⊢ ∃ y, (x, y) ∈ f.graph
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
hx : x ∈ f.domain
⊢ x ∈ g.domain

Tactic:
mem_domain_iff

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 : ∃ y, (x, y) ∈ f.graph
⊢ ∃ y, (x, y) ∈ g.graph
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
e : A ≃ₐ[R] B
x✝ : A[M]
⊢ (mapAlgHom M ↑e.symm) ((↑↑(mapAlgHom M ↑e).toRingHom).toFun x✝) = x✝

Tactic:
aesop

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✝⁸ : 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
e : A ≃ₐ[R] B
x✝ : B[M]
⊢ (↑↑(mapAlgHom M ↑e).toRingHom).toFun ((mapAlgHom M ↑e.symm) x✝) = x✝

Tactic:
aesop

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

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

Tactic:
aesop

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

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

Tactic:
aesop

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]
_fd : A
fds : _fd ∈ f.coeff.support
_gd : A
gds : _gd ∈ g.coeff.support
⊢ degb _fd + degb _gd ≤ degb _fd + g.coeff.support.sup degb

Tactic:
← Finset.le_sup gds

Goal state after:
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]
_fd : A
fds : _fd ∈ f.coeff.support
_gd : A
gds : _gd ∈ g.coeff.support
⊢ degb _fd + degb _gd ≤ degb _fd + degb _gd
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (↑n).natDegree = 0

Tactic:
simp only [← C_eq_natCast, natDegree_C]

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ ¬↑u = 0

Tactic:
exact Units.ne_zero _

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ (a • p).degree = p.degree

Tactic:
refine le_antisymm (degree_smul_le a p) <| degree_le_degree ?_
  rw [coeff_smul, coeff_natDegree, smul_eq_mul, ne_eq]
  exact hp.mul_right_eq_zero_iff.ne.mpr ha

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ x, C x = p) → p.natDegree = 0

Tactic:
aesop

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : ℕ
x✝ : b ∈ p.support
hb : b ≠ 0
⊢ (fun e a ↦ a * 0 ^ e) b (p.coeff b) = 0

Tactic:
by simp [zero_pow hb]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
p : R[X]
⊢ ∀ (n : ℕ), (map g (map f p)).coeff n = (map (g.comp f) p).coeff n

Tactic:
by simp [coeff_map]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ D 0 = 0

Tactic:
hzero

Goal state after:
case zero
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ 0 = 0
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : x i + y i = if a = i then n else 0
hai : a ≠ i
⊢ (if a = i then x a else 0) = x i ∧ (if a = i then y a else 0) = y i

Tactic:
simp_rw [if_neg hai, add_eq_zero] at h ⊢

Goal state after:
case mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
hai : a ≠ i
h : x i = 0 ∧ y i = 0
⊢ 0 = x i ∧ 0 = y i
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
⊢ (algEquivCMulXAddC a b).symm = algEquivCMulXAddC (⅟a) (-⅟a * b)

Tactic:
ext p : 1

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
p : R[X]
⊢ (algEquivCMulXAddC a b).symm p = (algEquivCMulXAddC (⅟a) (-⅟a * b)) p
Module: Mathlib.Order.PiLex

Goal state before:
pp: case h
ι : Type u_1
β : ι → Type u_2
inst✝¹ : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst✝ : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j < i → x j = y j
hxy : y i < x i
⊢ (∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → toLex y j = toLex x j) ∧ (fun {i} x1 x2 ↦ x1 < x2) (toLex y i) (toLex x i)

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: case h
ι : Type u_1
β : ι → Type u_2
inst✝¹ : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst✝ : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j > i → x j = y j
hxy : y i < x i
⊢ (∀ (j : ι), (fun x1 x2 ↦ x1 > x2) j i → toColex y j = toColex x j) ∧
    (fun {i} x1 x2 ↦ x1 < x2) (toColex y i) (toColex x i)

Tactic:
aesop

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₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e

Tactic:
apply MvPolynomial.induction_on p

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (a : R) {s : σ →₀ ℕ} {a_1 : R},
    eval₂ f g (C a * (monomial s) a_1) = eval₂ f g (C a) * f a_1 * s.prod fun n e ↦ g n ^ e

case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
      (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * (monomial s) a) = eval₂ f g q * f a * s.prod fun n e ↦ g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g ((p + q) * (monomial s) a) = eval₂ f g (p + q) * f a * s.prod fun n e ↦ g n ^ e

case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * X n) * f a * s.prod fun n e ↦ g n ^ e
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (a : R) {s : σ →₀ ℕ} {a_1 : R},
    eval₂ f g (C a * (monomial s) a_1) = eval₂ f g (C a) * f a_1 * s.prod fun n e ↦ g n ^ e

Tactic:
intro a' s a
    simp [C_mul_monomial, eval₂_monomial, f.map_mul]

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

Goal state before:
pp: case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
⊢ ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    a_1 ∉ f.support → b ≠ 0 → motive ((monomial f) a) → motive ((monomial (Finsupp.single a_1 b + f)) a)

Tactic:
intro n e p _hpn _he ih
    have : ∀ e : ℕ, motive (monomial p a * X n ^ e) := by
      intro e
      induction e with
      | zero => simp [ih]
      | succ e e_ih => simp [pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]
    simp [add_comm, monomial_add_single, this]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
α : Type u_2
inst✝ : DecidableEq σ
s : Finset α
f : α → MvPolynomial σ R
⊢ (∑ x ∈ s, f x).support ⊆ s.biUnion fun x ↦ (f x).support

Tactic:
by
  simpa [support, coeff, MvPolynomial] using Finsupp.support_finsetSum

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₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ k (eval₂ f g p) = eval₂ (k.comp f) (⇑k ∘ g) p

Tactic:
apply MvPolynomial.induction_on p

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (a : R), k (eval₂ f g (C a)) = eval₂ (k.comp f) (⇑k ∘ g) (C a)

case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    k (eval₂ f g p) = eval₂ (k.comp f) (⇑k ∘ g) p →
      k (eval₂ f g q) = eval₂ (k.comp f) (⇑k ∘ g) q → k (eval₂ f g (p + q)) = eval₂ (k.comp f) (⇑k ∘ g) (p + q)

case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    k (eval₂ f g p) = eval₂ (k.comp f) (⇑k ∘ g) p → k (eval₂ f g (p * X n)) = eval₂ (k.comp f) (⇑k ∘ g) (p * X n)