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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
⊢ lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q)) ∘ₗ
      lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))) =
    LinearMap.id

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_2
α : Type u_1
x y : α
h : x ≠ y
a b : Fin (Nat.succ 0).succ
h' : ![x, y] a = ![x, y] b
⊢ a = b

Tactic:
fin_cases a <;> fin_cases b <;> aesop

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R⁰ R
h : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
induction x with | _ r s
  rw [OreLocalization.inv_def, OreLocalization.one_def]
  have hr : r ≠ 0 := by
    rintro rfl
    simp at h
  simp only [hr]
  with_unfolding_all apply OreLocalization.mul_inv ⟨r, _⟩

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁸ : Semiring R
S : Submonoid R
inst✝⁷ : OreSet S
X : Type u_2
inst✝⁶ : AddCommMonoid X
inst✝⁵ : Module R X
R₀ : Type ?u.16
inst✝⁴ : Semiring R₀
inst✝³ : Module R₀ X
inst✝² : Module R₀ R
inst✝¹ : IsScalarTower R₀ R X
inst✝ : IsScalarTower R₀ R R
r s : R₀
x : OreLocalization S X
⊢ (r + s) • x = r • x + s • x

Tactic:
simp only [← smul_one_oreDiv_one_smul, add_smul, ← add_oreDiv]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrixAlgEquiv v₁) (f ∘ₗ g) = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g

Tactic:
simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]

Goal state after:
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁹ : CommSemiring R✝
M✝ N : Submonoid R✝
S✝ : Type u_2
inst✝¹⁸ : CommSemiring S✝
inst✝¹⁷ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁶ : CommSemiring P✝
inst✝¹⁵ : IsLocalization M✝ S✝
g : R✝ →+* P✝
hg : ∀ (y : ↥M✝), IsUnit (g ↑y)
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
⊢ Submonoid.comap (↑h) (Submonoid.map (↑h) M) = M

Tactic:
Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective

Goal state after:
R✝ : Type u_1
inst✝¹⁹ : CommSemiring R✝
M✝ N : Submonoid R✝
S✝ : Type u_2
inst✝¹⁸ : CommSemiring S✝
inst✝¹⁷ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁶ : CommSemiring P✝
inst✝¹⁵ : IsLocalization M✝ S✝
g : R✝ →+* P✝
hg : ∀ (y : ↥M✝), IsUnit (g ↑y)
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
⊢ M = M
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
add✝ : Add α := e.add
mul✝ : Mul α := e.mul
x y : α
⊢ e.toFun (x + y) = e.toFun x + e.toFun y

Tactic:
simp [add_def]

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
⊢ NonUnitalCommRing α

Tactic:
by
  let zero := e.zero
  let add := e.add
  let mul := e.mul
  let neg := e.Neg
  let sub := e.sub
  let nsmul := e.smul ℕ
  let zsmul := e.smul ℤ
  apply e.injective.nonUnitalCommRing _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
C : Type uC
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ↑↑(leftComm R A B C) = ↑(_root_.TensorProduct.leftComm R A B C)

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : CompatibleSMul R S S S
⊢ ↑(lmulEquiv R S) = ↑(lidOfCompatibleSMul R S S)

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Algebra.StrictPositivity

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
u : Aˣ
⊢ 0 ≤ a ∧ IsUnit (↑u * a * star ↑u) ↔ 0 ≤ a ∧ IsUnit a

Tactic:
← Units.coe_star,

Goal state after:
A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
u : Aˣ
⊢ 0 ≤ a ∧ IsUnit (↑u * a * ↑(star u)) ↔ 0 ≤ a ∧ IsUnit a
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case mem.mem
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r✝ : R
a✝ : A
r : R
a : A
⊢ (fun s ↦ star s * s) r • (fun s ↦ star s * s) a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩

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

Goal state before:
pp: R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
⊢ Module.rank R ((i : η) → φ i) = sum fun i ↦ Module.rank R (φ i)

Tactic:
cases nonempty_fintype η
  let B i := chooseBasis R (φ i)
  let b : Basis _ R (∀ i, φ i) := Pi.basis fun i => B i
  simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
h : ∃ v, v ≠ 0 ∧ W = K ∙ v
⊢ IsAtom W

Tactic:
rcases h with ⟨v, ⟨hv, rfl⟩⟩
    exact nonzero_span_atom v hv

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
φ : F
⊢ ∀ {a : B},
    a ∈ (NonUnitalAlgHom.range (NonUnitalAlgHomClass.toNonUnitalAlgHom φ)).carrier →
      star a ∈ (NonUnitalAlgHom.range (NonUnitalAlgHomClass.toNonUnitalAlgHom φ)).carrier

Tactic:
by rintro _ ⟨a, rfl⟩; exact ⟨star a, map_star φ a⟩

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x ∈ t.erase x₀, (if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) • x +
      (-∑ z ∈ t.erase x₀, g (z - x₀)) • x₀ =
    0

Tactic:
neg_smul,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x ∈ t.erase x₀, (if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) • x +
      -((∑ z ∈ t.erase x₀, g (z - x₀)) • x₀) =
    0
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: A : Type v
inst✝³ : NonUnitalSemiring A
inst✝² : StarRing A
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R A
s : NonUnitalStarSubalgebra R A
⊢ Submodule.span R ↑s = s.toSubmodule

Tactic:
by
  simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_2
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n
⊢ f (b i) = (b.repr (b i)) ⟨w, ⋯⟩

Tactic:
Basis.repr_self

Goal state after:
case refine_2
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n
⊢ f (b i) = (Finsupp.single i 1) ⟨w, ⋯⟩
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
y' z' : ↥(R ∙ x)
⊢ σ (Classical.choose ⋯) • y = σ (Classical.choose ⋯) • y + σ (Classical.choose ⋯) • y

Tactic:
rw [← add_smul, ← RingHom.map_add, H]
        have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)
        simp only [add_smul, this, ← coe_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
f g : E →ₛₗ.[σ] F
h : Disjoint f.domain g.domain
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
⊢ ↑f x = ↑g y

Tactic:
by
  rw [disjoint_def] at h
  have hy : y = 0 := Subtype.ext (h y (hxy ▸ x.2) y.2)
  have hx : x = 0 := Subtype.ext (hxy.trans <| congr_arg _ hy)
  simp [*]

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
⊢ ((lift R) f) (ι R x) = f x

Tactic:
rw [ι_def, lift]
  rfl

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

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ q = 1 → p = 0

pp: case mpr
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ p = 0 → q = 1

Tactic:
· rintro rfl
    exact char_zero_of_expChar_one R p

Goal state after:
case mpr
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ p = 0 → q = 1
Module: Mathlib.LinearAlgebra.LinearPMap

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

Tactic:
rw [Prod.smul_mk] at hav'

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
inst✝³ : Module S F
G : Type u_6
inst✝² : AddCommGroup G
inst✝¹ : Module T G
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
a : R
v : ↥(map (LinearMap.fst R E F) g)
hsmul : a • ↑v ∈ map (LinearMap.fst R E F) g
hav : (a • ↑v, valFromGraph hg hsmul) ∈ g
hav' : (a • ↑v, a • valFromGraph hg ⋯) ∈ g
⊢ valFromGraph hg ⋯ = (RingHom.id R) a • valFromGraph hg ⋯
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 simp [curryAlgEquiv]

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

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

Tactic:
exact h₁ (left_mem_Ico.2 (g₀.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (C x * X ^ k).coeff n = if n = k then x else 0

Tactic:
C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ ((monomial k) x).coeff n = if n = k then x else 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (x + y * 0 + z * if k = n then 1 else 0) ≠ 0 ∧
    ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0) ≠ 0 ∧
      ((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z ≠ 0

Tactic:
if_neg hkm.ne',

Goal state after:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (x + y * 0 + z * if k = n then 1 else 0) ≠ 0 ∧
    (x * 0 + y + z * if m = n then 1 else 0) ≠ 0 ∧ ((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ degt 0 ≤ 0

Tactic:
refine (OrderDual.ofDual_le_ofDual.mp ?_)

Goal state after:
case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ OrderDual.ofDual 0 ≤ OrderDual.ofDual (degt 0)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ (C a * X ^ n).degree = ↑n

Tactic:
C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ ((monomial n) a).degree = ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ((monomial n) a).degree ≤ ↑n

Tactic:
by rw [h, (monomial n).map_zero, degree_zero]; exact bot_le

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
⊢ (C a * X).natDegree = 1

Tactic:
simpa only [pow_one] using natDegree_C_mul_X_pow 1 a ha

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ n ≤ p.natDegree

Tactic:
rw [← Nat.cast_le (α := WithBot ℕ), ← degree_eq_natDegree]

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree

R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.leadingCoeff = 0 ↔ p.degree = ⊥

Tactic:
leadingCoeff_eq_zero,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p = 0 ↔ p.degree = ⊥
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (C a * X ^ n).leadingCoeff = a

Tactic:
C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ ((monomial n) a).leadingCoeff = a
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).degree = 2

Tactic:
rw [add_assoc, degree_add_eq_left_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    degree_C_mul_X_pow 2 ha]

Goal state after:
R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑2 = 2
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ { toFun := D, map_add' := hadd }.srange

Tactic:
exact add_mem (supDegree_mem_range D hp) (supDegree_mem_range D hq)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ (eval₂ C (C r * X) p).coeff n = p.coeff n * r ^ n

Tactic:
eval₂_eq_sum_range,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ (∑ i ∈ range (p.natDegree + 1), C (p.coeff i) * (C r * X) ^ i).coeff n = p.coeff n * r ^ n
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ (p.comp (C r * X)).coeff n = p.coeff n * r ^ n

Tactic:
simp_rw [comp, eval₂_eq_sum_range, (commute_X _).symm.mul_pow,
    ← C_pow, finsetSum_coeff, coeff_C_mul, coeff_X_pow]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * if n = x then 1 else 0) = p.coeff n * r ^ n
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
f : α →₀ ℕ
p : (α →₀ ℕ) × (α →₀ ℕ)
⊢ p ∈ f.antidiagonal'.support ↔ p.1 + p.2 = f

Tactic:
rcases p with ⟨p₁, p₂⟩

Goal state after:
α : Type u
inst✝ : DecidableEq α
f p₁ p₂ : α →₀ ℕ
⊢ (p₁, p₂) ∈ f.antidiagonal'.support ↔ (p₁, p₂).1 + (p₁, p₂).2 = f
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ single i a ≤ f ↔ a ≤ f i

Tactic:
exact (le_iff' support_single_subset).trans <| by simp

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

Goal state before:
pp: case step.inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
h✝ : (P.coeff l • Q).natDegree < Q.natDegree
⊢ P * P.coeff l • Q = 0

Tactic:
rw [smul_eq_C_mul, mul_left_comm, hQ, mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
Q : R[X]
hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}
⊢ False

Tactic:
refine hQ.2 (eq_zero_of_mul_eq_zero_of_smul P (fun a ha ↦ ?_) Q (mul_comm P _ ▸ hQ.1))

Goal state after:
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
Q : R[X]
hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}
a : R
ha : a • P = 0
⊢ a = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ C a * (monomial s) a' = (monomial s) (a * a')

Tactic:
have := single_mul_single 0 s a a'

Goal state after:
R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
this : AddMonoidAlgebra.single 0 a * AddMonoidAlgebra.single s a' = AddMonoidAlgebra.single (0 + s) (a * a')
⊢ C a * (monomial s) a' = (monomial s) (a * a')
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_2
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ (↑f).comp (of R (σ →₀ ℕ)) = (↑g).comp (of R (σ →₀ ℕ))

Tactic:
· apply Finsupp.mulHom_ext'; intro x
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `Finsupp.mulHom_ext'` needs to have increased priority
    apply MonoidHom.ext_mnat
    exact hX _

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

Goal state before:
pp: 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 (⇑k ∘ g) ((map f) p) → k (eval₂ f g (p * X n)) = eval₂ k (⇑k ∘ g) ((map f) (p * X n))

Tactic:
intro p s hp

Goal state after:
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✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ k (eval₂ f g (p * X s)) = eval₂ k (⇑k ∘ g) ((map f) (p * X s))