mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r s : R
⊢ r ∈ σ (-↑ₐ s + (↑ₐ s + a)) ↔ r ∈ σ a

Tactic:
neg_add_cancel_left

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r s : R
⊢ r ∈ σ a ↔ r ∈ σ a
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
hle : x ≤ y
z : R
⊢ x + z ≤ y + z

Tactic:
by
    rw [StarOrderedRing.le_iff] at hle ⊢
    refine hle.imp fun s hs ↦ ?_
    rw [hs.2, add_right_comm]
    exact ⟨hs.1, rfl⟩

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] ↥(centralizer R S)
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A))
      ((Algebra.TensorProduct.comm R A ↥(centralizer R S)) x) =
    (Algebra.TensorProduct.comm R A B) ((Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x)

Tactic:
by rw [Algebra.TensorProduct.comm_comp_map_apply]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a ↦ a • g i) ∈ span R (range fun x ↦ ↑(f x))
h₂ : (c.sum fun i a ↦ a • g i) ∈ span R (range g)
this : M'.mkQ (c.sum fun i a ↦ a • g i) = 0
⊢ (c.sum fun i a ↦ a • g i) = 0

Tactic:
map_finsuppSum,

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a ↦ a • g i) ∈ span R (range fun x ↦ ↑(f x))
h₂ : (c.sum fun i a ↦ a • g i) ∈ span R (range g)
this : (c.sum fun a b ↦ M'.mkQ (b • g a)) = 0
⊢ (c.sum fun i a ↦ a • g i) = 0
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{max u w, v} #m * lift.{max u v, w} #n * 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n

Tactic:
mul_one,

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max v w u, v} #m * lift.{max v w u, w} #n
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
rw [h]; exact mem_top

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
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
| y

Tactic:
rw [← one_smul S y]

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
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
| 1 • y
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
V₂ : Type v'
inst✝⁷ : AddCommGroup V₂
inst✝⁶ : Module K V₂
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : IsStablyFiniteRing R
⊢ IsStablyFiniteRing (End R M)

Tactic:
by
  let e := (Module.Free.chooseBasis R M).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ..
  rw [RingEquiv.isStablyFiniteRing_iff e.conjRingEquiv]
  infer_instance

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
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : f y = f x
⊢ x ∈ p ⊔ f.ker

Tactic:
exact Submodule.mem_sup.mpr ⟨y, hy, x - y, by simp [hxy], add_sub_cancel y x⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
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 : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ fg (⟨z₁, hz₁⟩ + ⟨z₂, hz₂⟩) = ↑f (⟨x ⟨z₁, hz₁⟩, ⋯⟩ + ⟨x ⟨z₂, hz₂⟩, ⋯⟩) + ↑g (⟨y ⟨z₁, hz₁⟩, ⋯⟩ + ⟨y ⟨z₂, hz₂⟩, ⋯⟩)

Tactic:
apply fg_eq

Goal state after:
case w.refine_1
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 : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := ⋯
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ ↑(⟨x ⟨z₁, hz₁⟩, ⋯⟩ + ⟨x ⟨z₂, hz₂⟩, ⋯⟩) + ↑(⟨y ⟨z₁, hz₁⟩, ⋯⟩ + ⟨y ⟨z₂, hz₂⟩, ⋯⟩) = ↑(⟨z₁, hz₁⟩ + ⟨z₂, hz₂⟩)
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_2
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 : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
c : R
z : ↥(f.domain ⊔ g.domain)
⊢ fg (c • z) = ↑f (c • ⟨x z, ⋯⟩) + ↑g (c • ⟨y z, ⋯⟩)

Tactic:
apply fg_eq

Goal state after:
case w.refine_2
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 : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := ⋯
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
c : R
z : ↥(f.domain ⊔ g.domain)
⊢ ↑(c • ⟨x z, ⋯⟩) + ↑(c • ⟨y z, ⋯⟩) = ↑(c • z)
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
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
f g h : E →ₛₗ.[σ] F
x : E
⊢ x ∈ (f + g + h).domain ↔ x ∈ (f + (g + h)).domain

Tactic:
simp only [add_domain, inf_assoc]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p = p.sum fun e a ↦ f a * x ^ e

Tactic:
rw [eval₂_def]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x
⊢ eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod

Tactic:
induction ps using List.reverseRecOn with
  | nil => simp
  | append_singleton ps p ihp =>
    simp only [List.forall_mem_append, List.forall_mem_singleton] at hf
    simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]

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:
sum_eq_of_subset (f · ·) (fun n => (f n).map_zero) (support_smul c p)

Goal state after:
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]
⊢ ∑ n ∈ p.support, (f n) ((c • p).coeff n) = (RingHom.id R) c • p.sum fun x1 x2 ↦ (f x1) x2
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 * 1 + y * (X ^ m).coeff k ≠ 0 ∧ x * (X ^ k).coeff m + y * 1 ≠ 0

Tactic:
mul_one,

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

Tactic:
mul_one,

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 * (X ^ m).coeff k + z * (X ^ n).coeff k ≠ 0 ∧
    x * (X ^ k).coeff m + y + z * (X ^ n).coeff m ≠ 0 ∧ x * (X ^ k).coeff n + y * (X ^ m).coeff n + z ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
a : R
ha : ¬a = 0
⊢ WithBot.unbotD 0 0 = 0

Tactic:
WithBot.unbotD_zero

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
a : R
ha : ¬a = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
a : R
ha : ¬a = 0
⊢ (C a).natDegree = 0

Tactic:
rw [natDegree, degree_C ha, WithBot.unbotD_zero]

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

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

Tactic:
by
  rw [add_comm]
  exact leadingCoeff_add_of_degree_lt h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
⊢ p.leadingCoeff * 1 ≠ 0

Tactic:
mul_one,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
⊢ p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case h₀.inr.inl
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
h : dg < dg'
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt (hdg.trans_lt h), mul_zero]

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✝⁶ : 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
hq : Monic D q
hp : p ≠ 0
h✝ : Nontrivial R
⊢ leadingCoeff D p * 1 ≠ 0

Tactic:
mul_one,

Goal state after:
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
hq : Monic D q
hp : p ≠ 0
h✝ : Nontrivial R
⊢ leadingCoeff D p ≠ 0
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₀ : p ≠ 0
⊢ (map f p).degree < p.degree

Tactic:
refine degree_map_le.lt_of_ne fun hpq ↦ hp₀ ?_

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0
Module: Mathlib.Algebra.Order.Pi

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : One γ
inst✝ : LE γ
f : α → β
g : α → γ
e : β → γ
hg : g ≤ 1
he : e ≤ 1
_b : β
⊢ extend f g e _b ≤ 1 _b

Tactic:
exact dite_le_one (fun _ ↦ hg _) (fun _ ↦ he _)

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ toLex (update x i a) < toLex x ∨ toLex (update x i a) = toLex x ↔ a < x i ∨ a = x i

Tactic:
toLex_update_lt_self_iff,

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ a < x i ∨ toLex (update x i a) = toLex x ↔ a < x i ∨ a = x i
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (f + -g) = g.support

Tactic:
neLocus_self_add_right,

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (-g).support = g.support
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₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (a : R) {p : MvPolynomial σ R}, eval₂ f g (p * C a) = eval₂ f g p * eval₂ f g (C a)

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 [eval₂_C, eval₂_mul_C]

Goal state after:
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)

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.Eval

Goal state before:
pp: 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}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q

Tactic:
by
  apply MvPolynomial.induction_on q
  · simp [eval₂_C, eval₂_mul_C]
  · simp +contextual [mul_add, eval₂_add]
  · simp +contextual [X, eval₂_mul_monomial, ← mul_assoc]

Goal state after:
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₁
f : R →+* S₁
r : R
m : σ →₀ ℕ
⊢ coeff m ((map f) (C r)) = f (coeff m (C r))

Tactic:
simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ ((p * q).support.sup fun s ↦ toMultiset s) ≤ (p.support.sup fun s ↦ toMultiset s) + q.support.sup fun s ↦ toMultiset s

Tactic:
exact supDegree_mul_le (map_add _)

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

Goal state before:
pp: case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ ∃ s_1 q, (rename Subtype.val) p * X n = (rename Subtype.val) q

Tactic:
refine ⟨insert n s, ⟨?_, ?_⟩⟩

Goal state after:
case mul_X.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ MvPolynomial (↥(insert n s)) R

case mul_X.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ (rename Subtype.val) p * X n = (rename Subtype.val) ?mul_X.refine_1
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ eval₂ φ g ((map f) p) = eval₂ (φ.comp f) g p

Tactic:
by
  rw [← eval_map, ← eval_map, map_map]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ Finset.image (⇑(mapDomain.addMonoidHom f)) φ.coeff.support
⊢ False

Tactic:
rw [Finset.mem_image] at H

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : ∃ a ∈ φ.coeff.support, (mapDomain.addMonoidHom f) a = d
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
⊢ degreeOf i ((monomial s) a) = s i

Tactic:
rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]

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

Goal state before:
pp: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
⊢ degreeOf i (p * 1) = degreeOf i p + 0

Tactic:
mul_one,

Goal state after:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
⊢ degreeOf i p = degreeOf i p + 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ ((rename f) p).support
h' : b ∈ Finset.image (⇑(mapDomain.addMonoidHom f)) p.coeff.support
⊢ (b.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
rw [Finset.mem_image] at h'

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ ((rename f) p).support
h' : ∃ a ∈ p.coeff.support, (mapDomain.addMonoidHom f) a = b
⊢ (b.sum fun x e ↦ e) ≤ p.totalDegree
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hf : p.natDegree ≤ n
hn : p.coeff n = 0
⊢ p.natDegree ≤ n - 1

Tactic:
obtain _ | n := n
  · exact hf
  · refine (Nat.le_succ_iff_eq_or_le.1 hf).resolve_left fun h ↦ ?_
    rw [← Nat.succ_eq_add_one, ← h, coeff_natDegree, leadingCoeff_eq_zero] at hn
    simp_all

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

Goal state before:
pp: R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m

Tactic:
by
  induction m with
  | zero => simp
  | succ m hm =>
    rw [pow_succ, pow_succ, ← hm, Nat.succ_mul, coeff_mul_add_eq_of_natDegree_le _ pn]
    refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))
    gcongr

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

Goal state before:
pp: case insert.inr.inl.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
by_cases hx0 : f x = 0

Goal state after:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
nd : ¬(p + q).natDegree = p.natDegree
⊢ False

Tactic:
exact nd (natDegree_add_eq_left_of_degree_lt pq)

Goal state after: