mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
s : Set (↥I ⊗[R] M)
hs : Finite ↑s
J : ↥I ⊗[R] M → Submodule R N
fg : ∀ (x : ↥I ⊗[R] M), (J x).FG
hle : ∀ (x : ↥I ⊗[R] M), J x ≤ I
y : (x : ↥I ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : ↥I ⊗[R] M), x = (rTensor M (inclusion ⋯)) (y x)
x : ↥I ⊗[R] M
hx : x ∈ s
⊢ (rTensor M (inclusion ⋯) ∘ₗ rTensor M (inclusion ⋯)) (y x) = (rTensor M (inclusion ⋯)) (y x)

Tactic:
← rTensor_comp

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
s : Set (↥I ⊗[R] M)
hs : Finite ↑s
J : ↥I ⊗[R] M → Submodule R N
fg : ∀ (x : ↥I ⊗[R] M), (J x).FG
hle : ∀ (x : ↥I ⊗[R] M), J x ≤ I
y : (x : ↥I ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : ↥I ⊗[R] M), x = (rTensor M (inclusion ⋯)) (y x)
x : ↥I ⊗[R] M
hx : x ∈ s
⊢ (rTensor M (inclusion ⋯ ∘ₗ inclusion ⋯)) (y x) = (rTensor M (inclusion ⋯)) (y x)
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (algebraMap R A) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r

Tactic:
by
  rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
F : Type u_3
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
inst✝¹ : EquivLike F R S
inst✝ : StarRingEquivClass F R S
f : F
x y : R
h : f x ≤ f y
f_inv : S →⋆ₙ+* R := ↑(↑f).symm
⊢ x ≤ y

Tactic:
have f_inv_f (r : R) : f_inv (f r) = r := EquivLike.inv_apply_apply f r

Goal state after:
R✝ : Type u_1
A : Type u_2
F : Type u_3
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
inst✝¹ : EquivLike F R S
inst✝ : StarRingEquivClass F R S
f : F
x y : R
h : f x ≤ f y
f_inv : S →⋆ₙ+* R := ↑(↑f).symm
f_inv_f : ∀ (r : R), f_inv (f r) = r
⊢ x ≤ y
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
inst✝ : Module.Free R B
⊢ centralizer R ↑includeLeft.range = (Algebra.TensorProduct.map (center R A).val (AlgHom.id R B)).range

Tactic:
← centralizer_univ,

Goal state after:
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
inst✝ : Module.Free R B
⊢ centralizer R ↑includeLeft.range = (Algebra.TensorProduct.map (centralizer R Set.univ).val (AlgHom.id R B)).range
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
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = (Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range

Tactic:
← centralizer_univ,

Goal state after:
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
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R Set.univ).val).range
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ ¬Nonempty ↑↑⟨s, hs⟩

Tactic:
rintro ⟨i : s⟩

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : ↑s
⊢ False
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case right
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ∀ b < K ∙ v, b = ⊥

Tactic:
intro T

Goal state after:
case right
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
⊢ T < K ∙ v → T = ⊥
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
ι : Type u_1
h : Module.Finite R (ι →₀ M)
i : ι
a✝ : Nontrivial M
s : Finset (ι →₀ M)
hs : span R ↑s = ⊤
⊢ Module.Finite R M ∧ Finite ι

Tactic:
exact ⟨.of_surjective (Finsupp.lapply (R := R) (M := M) i) (Finsupp.apply_surjective i),
       finite_of_span_finite_eq_top_finsupp s.finite_toSet hs⟩

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
⊢ f = g → f.domain = g.domain ∧ ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩

Tactic:
rintro rfl

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
f : E →ₛₗ.[σ] F
⊢ f.domain = f.domain ∧ ∀ ⦃x : E⦄ ⦃hf hg : x ∈ f.domain⦄, ↑f ⟨x, hf⟩ = ↑f ⟨x, hg⟩
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
⊢ Module.rank K ↥W ≤ 1 ↔ W.IsPrincipal

Tactic:
simp only [rank_le_one_iff, Submodule.isPrincipal_iff, le_antisymm_iff, le_span_singleton_iff,
    span_singleton_le_iff_mem]
  constructor
  · rintro ⟨⟨m, hm⟩, hm'⟩
    choose f hf using hm'
    exact ⟨m, ⟨fun v hv => ⟨f ⟨v, hv⟩, congr_arg ((↑) : W → V) (hf ⟨v, hv⟩)⟩, hm⟩⟩
  · rintro ⟨a, ⟨h, ha⟩⟩
    choose f hf using h
    exact ⟨⟨a, ha⟩, fun v => ⟨f v.1 v.2, Subtype.ext (hf v.1 v.2)⟩⟩

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ S = ⊥ → Module.rank F ↥S = 1

Tactic:
rintro rfl

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
⊢ Module.rank F ↥⊥ = 1
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
⊢ Quot.mk (Rel R X) a✝ * 1 = Quot.mk (Rel R X) a✝

Tactic:
exact Quot.sound Rel.mul_one

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

Goal state before:
pp: p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ n = 1 → m = p

Tactic:
rintro rfl

Goal state after:
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ 1 = 1
⊢ m = p
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m ≠ 0

Tactic:
rintro rfl

Goal state after:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : 0 ∣ n
⊢ False
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 : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
⊢ ↑(f.domRestrict S) x = ↑f y

Tactic:
by
  have : Submodule.inclusion (by simp) x = y := by
    ext
    simp [h]
  rw [← this]
  exact LinearPMap.mk_apply _ _ _

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
b : ℕ
⊢ p ∣ b ↔ ↑p ∣ ↑b

Tactic:
Int.natCast_dvd_natCast

Goal state after:
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
b : ℕ
⊢ p ∣ b ↔ p ∣ b
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ n.minFacProp (n.minFacAux (x✝ + 2))

Tactic:
· refine
        have := minFac_lemma n k h
        minFacAux_has_prop n2 (k + 2) (i + 1) (by simp [k, e, Nat.left_distrib, add_right_comm])
          fun m m2 d => ?_
      rcases Nat.eq_or_lt_of_le (a m m2 d) with rfl | ml
      · contradiction
      apply (Nat.eq_or_lt_of_le ml).resolve_left
      intro me
      rw [← me, e] at d
      have d' : 2 * (i + 2) ∣ n := d
      have := a _ le_rfl (dvd_of_mul_right_dvd d')
      rw [e] at this
      exact absurd this (by contradiction)

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
b : ℕ
h : 0 < ↑b
⊢ p ∣ b ↔ ↑p ∣ ↑b

Tactic:
Int.natCast_dvd_natCast

Goal state after:
case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
b : ℕ
h : 0 < ↑b
⊢ p ∣ b ↔ p ∣ b
Module: Mathlib.Algebra.CharP.Defs

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

Tactic:
rintro rfl

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

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

Tactic:
rintro rfl

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

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

Tactic:
rintro rfl

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

Goal state before:
pp: case mpr
n : ℕ
⊢ n = 1 → n.minFac = 1

Tactic:
rintro rfl

Goal state after:
case mpr
⊢ minFac 1 = 1
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

Tactic:
rintro rfl

Goal state after:
case mp
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R 1
⊢ p = 0
Module: Mathlib.Algebra.CharP.Defs

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

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

Goal state before:
pp: case e'_3
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 : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ 0 = ((a, y₁) - (a, y₂)).1

Tactic:
exact (sub_self _).symm

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

Goal state before:
pp: case single
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
m : M
a : A
⊢ φ₁ (single m a) = φ₂ (single m a)

Tactic:
| single m a =>

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 rw [MulAut.mul_def, AlgEquiv.aut_mul, trans_domCongr_domCongr]

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
⊢ p ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
h : coeff 0 n ≠ 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mpr
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Tactic:
rintro rfl

Goal state after:
case mpr
m : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑m
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mpr
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Tactic:
rintro rfl

Goal state after:
case mpr
m : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑m
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
n : ℕ
hn : (p ^ n).degree ≤ ↑n * a
⊢ (p ^ (n + 1)).degree ≤ ↑(n + 1) * a

Tactic:
rw [Nat.cast_succ, add_mul, one_mul, pow_succ]
      exact degree_mul_le_of_le hn hp

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

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

Tactic:
by
  simpa only [pow_one] using leadingCoeff_C_mul_X_pow a 1

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
⊢ p ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hp : Monic 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
c : R
hc : (C c).Monic
⊢ c ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hc : (C 0).Monic
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: case neg.pn
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree ≤ p.natDegree

pp: case neg.p1
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).coeff p.natDegree ≠ 0

Tactic:
· exact (natDegree_smul_le _ _).trans (le_refl _)

Goal state after:
case neg.p1
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).coeff p.natDegree ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
p : R[A]
D : A → B
hp : p ≠ 0
a : A
he : supDegree D p = D a
⊢ supDegree D p ∈ Set.range D

Tactic:
exact ⟨a, he.symm⟩

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
h✝ : Nontrivial R
h : IsUnit p
⊢ False

Tactic:
simp [degree_eq_zero_of_isUnit h] at hpl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.Monic
⊢ p = 1 → p.natDegree = 0

Tactic:
rintro rfl

Goal state after:
R : Type u
inst✝ : Semiring R
hf : Monic 1
⊢ natDegree 1 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hmem
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
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0

Tactic:
exact hpq

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

Goal state before:
pp: case succ
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✝ : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p ^ (n + 1))

Tactic:
rw [pow_succ']

Goal state after:
case succ
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✝ : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p * p ^ n)
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
⊢ ↑d + 1 = ↑d.succ

Tactic:
simp only [Nat.cast_succ]

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
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : map f p ≠ 0
⊢ p ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hp : f (leadingCoeff 0) = 0
hp₀ : map f 0 ≠ 0
⊢ False
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
⊢ (map f p).degree = p.degree

Tactic:
refine degree_map_le.antisymm ?_
  have hp0 : p ≠ 0 :=
    leadingCoeff_ne_zero.mp fun hp0 => hf (_root_.trans (congr_arg _ hp0) f.map_zero)
  rw [degree_eq_natDegree hp0]
  refine le_degree_of_ne_zero ?_
  rw [coeff_map]
  exact hf

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ f ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hf : IsUnit (leadingCoeff 0)
H : IsUnit (map φ 0)
dz : degree 0 = 0
⊢ False
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
⊢ (∃ a b a_1 b_1, (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) ↔ u + v = x.sumElim y

Tactic:
refine ⟨fun ⟨a, b, a', b', h1, h2, h3⟩ ↦ ?_, fun h ↦
    ⟨u.comapDomain Sum.inl Sum.inl_injective.injOn, v.comapDomain Sum.inl Sum.inl_injective.injOn,
    u.comapDomain Sum.inr Sum.inr_injective.injOn, v.comapDomain Sum.inr Sum.inr_injective.injOn,
    ⟨?_, ?_⟩, comapDomain_sumElim_comapDomain .., comapDomain_sumElim_comapDomain ..⟩⟩

Goal state after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
x✝ : ∃ a b a_1 b_1, (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v
a b : α →₀ ℕ
a' b' : β →₀ ℕ
h1 : a + b = x ∧ a' + b' = y
h2 : a.sumElim a' = u
h3 : b.sumElim b' = v
⊢ u + v = x.sumElim y

case refine_2
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inl u ⋯ + comapDomain Sum.inl v ⋯ = x

case refine_3
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
x✝ : ∃ a b a_1 b_1, (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v
a b : α →₀ ℕ
a' b' : β →₀ ℕ
h1 : a + b = x ∧ a' + b' = y
h2 : a.sumElim a' = u
h3 : b.sumElim b' = v
⊢ a.sumElim a' + v = x.sumElim y

Tactic:
← h3,

Goal state after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
x✝ : ∃ a b a_1 b_1, (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v
a b : α →₀ ℕ
a' b' : β →₀ ℕ
h1 : a + b = x ∧ a' + b' = y
h2 : a.sumElim a' = u
h3 : b.sumElim b' = v
⊢ a.sumElim a' + b.sumElim b' = x.sumElim y
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ p.coeff 0 = (aeval 0) p

Tactic:
by
  simp [coeff_zero_eq_eval_zero]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : 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
⊢ ¬toLex x ≤ toLex y

Tactic:
apply not_le_of_gt

Goal state after:
ι : 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
⊢ toLex y < toLex x
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : 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
⊢ ¬toColex x ≤ toColex y

Tactic:
apply not_le_of_gt

Goal state after:
ι : 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
⊢ toColex y < toColex x
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
P : MvPolynomial σ R → Prop
p : MvPolynomial σ R
monomial : ∀ (u : σ →₀ ℕ) (a : R), P ((MvPolynomial.monomial u) a)
add : ∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)
this : P ((MvPolynomial.monomial 0) 0)
⊢ P 0

Tactic:
monomial_zero

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
P : MvPolynomial σ R → Prop
p : MvPolynomial σ R
monomial : ∀ (u : σ →₀ ℕ) (a : R), P ((MvPolynomial.monomial u) a)
add : ∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)
this : P 0
⊢ P 0
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✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ eval₂ k (⇑k ∘ g) ((map f) p) * k (g s) = eval₂ k (⇑k ∘ g) ((map f) p) * (⇑k ∘ g) s

Tactic:
comp_apply

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)
⊢ eval₂ k (⇑k ∘ g) ((map f) p) * k (g s) = eval₂ k (⇑k ∘ g) ((map f) p) * k (g s)