mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
a : ι → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M) A
⊢ (n : ℕ) × Basis (Fin n) R M

Tactic:
have : LinearMap.ker φ = ⊥ := LinearMap.ker_lsmul hA

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this✝ : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this✝.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
a : ι → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M) A
this : φ.ker = ⊥
⊢ (n : ℕ) × Basis (Fin n) R M
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a₁ b ↦ if a₁ = i then b * snf.a a₁ else 0) = snf.a i * c i

Tactic:
Finsupp.sum_ite_eq',

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (if i ∈ c.support then c i * snf.a i else 0) = snf.a i * c i
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
⊢ ⇑(snf.bM.repr ↑m) ∘ ⇑snf.f = snf.a • ⇑(snf.bN.repr m)

Tactic:
ext i
  simp [Pi.smul_apply (snf.a i)]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
m : ↥M
⊢ x • mk' S 1 m = mk' S x m

Tactic:
rw [smul_mk', mul_one]

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

Goal state before:
pp: A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥A⁰
⊢ mk' K x y = 1 ↔ x = ↑y

Tactic:
have := (algebraMap A K).domain_nontrivial

Goal state after:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
⊢ mk' K x y = 1 ↔ x = ↑y
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
x : K₁
⊢ (algebraMap K₂ L₂) (e x) = f ((algebraMap K₁ L₁) x)

Tactic:
obtain ⟨r, s, hs, rfl⟩ := IsFractionRing.div_surjective A x
  simp_rw [map_div₀, AlgHom.commutes, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply A B L₁, AlgHom.commutes, ← IsScalarTower.algebraMap_apply]

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

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f1 f2 : K →+* L
hf : ∀ (x : A), f1 ((algebraMap A K) x) = f2 ((algebraMap A K) x)
⊢ f1 = f2

Tactic:
by
  ext z
  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective A z
  rw [map_div₀, map_div₀, hf, hf]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
⊢ 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m

Tactic:
let f : A ⊗[R] A →ₗ[R] A ⊗[R] M := lift
    { toFun x :=
      { toFun y := x ⊗ₜ (y • m)
        map_add' := by simp [add_smul, tmul_add]
        map_smul' := by simp }
      map_add' := by intros; ext; simp [add_tmul]
      map_smul' := by intros; ext; simp [smul_tmul'] }

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
f : A ⊗[R] A →ₗ[R] A ⊗[R] M :=
  lift
    { toFun := fun x ↦ { toFun := fun y ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
⊢ 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
S : Type uS
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
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S A
inst✝³ : Algebra R S
inst✝² : Algebra S C
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight
⊢ f = g

Tactic:
by
  apply AlgHom.toLinearMap_injective
  ext a b
  have := congr_arg₂ HMul.hMul (AlgHom.congr_fun ha a) (AlgHom.congr_fun hb b)
  dsimp at *
  rwa [← map_mul, ← map_mul, tmul_mul_tmul, one_mul, mul_one] at this

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

Goal state before:
pp: R : Type uR
S : Type uS
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ Function.RightInverse ⇑((TensorProduct.mk R S M) 1) ⇑(LinearMap.liftBaseChange S LinearMap.id)

Tactic:
intro m

Goal state after:
R : Type uR
S : Type uS
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
m : M
⊢ (LinearMap.liftBaseChange S LinearMap.id) (((TensorProduct.mk R S M) 1) m) = m
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : SMulCommClass R A A
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R A A
inst✝ : IsScalarTower R B B
a : A
b : B
⊢ mulLeft R (a ⊗ₜ[R] b) = map (mulLeft R a) (mulLeft R b)

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : SMulCommClass R A A
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R A A
inst✝ : IsScalarTower R B B
a : A
b : B
⊢ mulRight R (a ⊗ₜ[R] b) = map (mulRight R a) (mulRight R b)

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type uR
S : Type uS
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ↑R (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ (TensorProduct.rid R R S).toLinearMap =
    LinearMap.lTensor S (Algebra.linearMap R B)

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
⊢ (↑(TensorProduct.rid R S A)).comp includeLeftRingHom = RingHom.id A

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
R' : Type u_6
S' : Type u_7
T' : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra R' T'
fR : R →+* R'
fS : S →+* S'
fT : T →+* T'
HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR
HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR
⊢ (mapRingHom fR fS fT HS HT).comp includeLeftRingHom = includeLeftRingHom.comp fS

Tactic:
by
  ext; simp

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

Goal state before:
pp: case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ s • inl r✝ + s • ↑a✝ = inl (s • 1 * r✝) + ↑((s • 1) • a✝)

Tactic:
smul_one_mul,

Goal state after:
case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ s • inl r✝ + s • ↑a✝ = inl (s • r✝) + ↑((s • 1) • a✝)
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
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ star c * x * c + star c * y * c ≤ star c * (x + y) * c

Tactic:
by rw [mul_add, add_mul]

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

Goal state before:
pp: case intro.intro
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type w
n : Type w'
inst✝¹ : Finite m
inst✝ : Finite n
val✝¹ : Fintype m
val✝ : Fintype n
⊢ Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)

Tactic:
obtain ⟨I, b⟩ := Module.Free.exists_basis (R := R) (M := M)

Goal state after:
case intro.intro
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type w
n : Type w'
inst✝¹ : Finite m
inst✝ : Finite n
val✝¹ : Fintype m
val✝ : Fintype n
I : Type v
b : Basis I R M
⊢ Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i ↦ ↑i) → s.card ≤ n
⊢ Module.rank R M ≤ ↑n

Tactic:
rw [Module.rank_def]

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i ↦ ↑i) → s.card ≤ n
⊢ ⨆ ι, #↑↑ι ≤ ↑n
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
hs : ⊤ ≤ span K s
⊢ range ⇑(ofSpan hs) = ⋯.extend ⋯

Tactic:
coe_ofSpan,

Goal state after:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
hs : ⊤ ≤ span K s
⊢ range Subtype.val = ⋯.extend ⋯
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ↑(ofVectorSpaceIndex K V)
⊢ (extend ⋯) x = ↑x

Tactic:
exact Basis.mk_apply _ _ _

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
n : ℕ
inst✝ : n.AtLeastTwo
a : R
⊢ eval a (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simp only [OfNat.ofNat, eval_natCast]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case grade0
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
r✝ : R
⊢ (algebraMap R (FreeAlgebra R X)) r✝ ∈ S

Tactic:
| grade0 =>

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

Goal state before:
pp: case monomial
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
r : R
⊢ eval₂ f x ((monomial n) r) = eval x (map f ((monomial n) r))

Tactic:
| monomial n r =>

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

Goal state before:
pp: R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝⁵ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : AddCommMonoid M
inst✝¹ : Module R A
inst✝ : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ ((c • p).sum fun x1 x2 ↦ (f x1) x2) = (RingHom.id R) c • p.sum fun x1 x2 ↦ (f x1) x2

Tactic:
rw [sum_eq_of_subset (f · ·) (fun n => (f n).map_zero) (support_smul c p)]
    simp only [sum_def, Finset.smul_sum, coeff_smul, map_smul, RingHom.id_apply]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ x + 0 ≠ 0 ∧ y ≠ 0

Tactic:
add_zero,

Goal state after:
R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0 ∧ y ≠ 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 * 0 + y + z * 0 ≠ 0 ∧ (x * if n = k then 1 else 0) + y * 0 + z ≠ 0

Tactic:
if_neg (hkm.trans hmn).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 * 0 ≠ 0 ∧ x * 0 + y + z * 0 ≠ 0 ∧ (x * if n = k then 1 else 0) + y * 0 + z ≠ 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 + 0 + 0 ≠ 0 ∧ 0 + y + 0 ≠ 0 ∧ 0 + 0 + z ≠ 0

Tactic:
add_zero,

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 ≠ 0 ∧ 0 + y ≠ 0 ∧ 0 + z ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : p.degree < q.degree
⊢ max p.degree q.degree ≤ (p + q).degree

Tactic:
rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ (p * q).natDegree

Tactic:
natDegree_mul h2.1 h2.2

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ p.natDegree + q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (C a * p).leadingCoeff = a * p.leadingCoeff

Tactic:
rwa [leadingCoeff, coeff_C_mul, natDegree_C_mul_of_isUnit, leadingCoeff]

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

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

Tactic:
rw [natDegree_add_C, natDegree_C_mul_X a ha]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ eval 0 p = p.coeff 0 * 0 ^ 0

Tactic:
eval_eq_sum

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun e a ↦ a * 0 ^ e) = p.coeff 0 * 0 ^ 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: case monomial
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
⊢ eval 1 (map f ((monomial n) r)) = f (eval 1 ((monomial n) r))

Tactic:
| monomial n r =>

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

Goal state before:
pp: case monomial
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n✝ n : ℕ
r : R
⊢ eval (↑n✝) (map f ((monomial n) r)) = f (eval (↑n✝) ((monomial n) r))

Tactic:
| monomial n r =>

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

Goal state before:
pp: case monomial
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
i : ℤ
n : ℕ
r : R
⊢ eval (↑i) (map f ((monomial n) r)) = f (eval (↑i) ((monomial n) r))

Tactic:
| monomial n r =>

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ (map f p).coeff p.natDegree ≠ 0

Tactic:
coeff_map

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ f (p.coeff p.natDegree) ≠ 0
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
A : Type z
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
f : R[X]
G : Type u_3
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G R A
g : G
x : A
⊢ (aeval (g • x)) f = g • (aeval x) f

Tactic:
by
  rw [← MulSemiringAction.toAlgHom_apply R, aeval_algHom_apply, MulSemiringAction.toAlgHom_apply]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = (aeval (ψ a)) (map φ p)

Tactic:
conv_rhs => rw [← eval_map_algebraMap]

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = eval (ψ a) (map (algebraMap T U) (map φ p))
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
⊢ ∃ a, a₁✝ < a ∧ a < a₂

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := exists_between hi

Goal state after:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ ∃ a, a₁✝ < a ∧ a < a₂
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: 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')

Tactic:
rw [zero_add] at this

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 s (a * a')
⊢ C a * (monomial s) a' = (monomial s) (a * a')
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      (∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q) →
        ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p + q)) = eval₂ f g p_1 * eval₂ f g (p + q)

pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p * X n)) = eval₂ f g p_1 * eval₂ f g (p * X n)

Tactic:
· simp +contextual [mul_add, eval₂_add]

Goal state after:
case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p * X n)) = eval₂ f g p_1 * eval₂ f g (p * X n)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ⊆ (p + q).support

Tactic:
intro m

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
⊢ m ∈ p.support \ q.support → m ∈ (p + q).support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.degrees = 0 ↔ ∀ b ∈ p.support, b = 0

Tactic:
Multiset.eq_zero_iff_forall_notMem

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ (a : σ), a ∉ p.degrees) ↔ ∀ b ∈ p.support, b = 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), f (coeff m p) = f (coeff m q)
⊢ ∀ (m : σ →₀ ℕ), coeff m p = coeff m q

Tactic:
intro m

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), f (coeff m p) = f (coeff m q)
m : σ →₀ ℕ
⊢ coeff m p = coeff m q