mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (LinearMap.liftBaseChange S ↑f) (x * y) = (LinearMap.liftBaseChange S ↑f) x * (LinearMap.liftBaseChange S ↑f) y

Tactic:
← LinearMap.mul_apply_apply S,

Goal state after:
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✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (LinearMap.liftBaseChange S ↑f) (((LinearMap.mul S (S ⊗[R] A)) x) y) =
    (LinearMap.liftBaseChange S ↑f) x * (LinearMap.liftBaseChange S ↑f) y
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✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (((LinearMap.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f)) x) y =
    (LinearMap.liftBaseChange S ↑f) x * (LinearMap.liftBaseChange S ↑f) y

Tactic:
← LinearMap.mul_apply_apply S,

Goal state after:
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✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (((LinearMap.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f)) x) y =
    ((LinearMap.mul S B) ((LinearMap.liftBaseChange S ↑f) x)) ((LinearMap.liftBaseChange S ↑f) y)
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : StarRing A
inst✝¹ : Module R A
inst✝ : StarModule R A
x y : Unitization R A
⊢ (star (x * y)).toProd.2 = (star y * star x).toProd.2

Tactic:
simp [-star_mul', add_comm (star x.fst • star y.snd)]

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

Goal state before:
pp: case mem.add
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
hr : r ∈ range fun s ↦ star s * s
a₁ a₂ : A
hx✝ : a₁ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hy✝ : a₂ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
ha₁ : r • a₁ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
ha₂ : r • a₂ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ r • (a₁ + a₂) ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
simpa [smul_add] using add_mem ha₁ ha₂

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

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ c * a * star c ≤ c * b * star c

Tactic:
by
  simpa only [star_star] using star_left_conjugate_le_conjugate hab (star c)

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
s : Set M
hs : s ⊆ ↑M'
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (⇑M'.mkQ) t
⊢ LinearIndepOn R (⇑(span R (id '' s)).mkQ ∘ id) t

Tactic:
rw [image_id]
    exact ht.of_comp ((span R s).mapQ M' (LinearMap.id) (span_le.2 hs))

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
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
refine ⟨fun h ↦ ?_, map_rel f⟩
    let f_inv : S →⋆ₙ+* R := (f : R ≃⋆+* S).symm
    have f_inv_f (r : R) : f_inv (f r) = r := EquivLike.inv_apply_apply f r
    rw [← f_inv_f x, ← f_inv_f y]
    exact NonUnitalStarRingHom.map_le_map_of_map_star f_inv h

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
⊢ lift.{v, max u v} (Module.rank R ({ x // x ∈ s } →₀ R)) ≤ lift.{max u v, v} #↑s

Tactic:
rank_finsupp_self

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
⊢ lift.{v, max u v} (lift.{u, v} #{ x // x ∈ s }) ≤ lift.{max u v, v} #↑s
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case neg
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
j : ↑n
h : ¬i = j
⊢ f (b j) = 0

Tactic:
← mem_ker,

Goal state after:
case neg
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
j : ↑n
h : ¬i = j
⊢ b j ∈ f.ker
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S < 1 ↔ S = ⊥

Tactic:
Nat.lt_one_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S = 0 ↔ S = ⊥
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.mk.mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝³ : FreeAlgebra R X
a✝² : Pre R X
b✝ : FreeAlgebra R X
a✝¹ : Pre R X
c✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝² * Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝ =
    Quot.mk (Rel R X) a✝² * (Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝)

Tactic:
exact Quot.sound Rel.mul_assoc

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
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
⊢ ∃ c, c • x = y

Tactic:
have : Submodule.span K {x} = ⊤ := by
    have : FiniteDimensional K V := .of_finrank_eq_succ h
    apply eq_top_of_finrank_eq
    rw [h]
    exact finrank_span_singleton hx

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : K ∙ x = ⊤
⊢ ∃ c, c • x = y
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mul_compat_left
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
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

pp: case mul_compat_right
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
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)

Tactic:
repeat
        change liftFun R X f _ * liftFun R X f _ = _
        simp only [*]
        rfl

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.mul
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = F (Quot.mk (Rel R X) a)
hb : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = F (Quot.mk (Rel R X) b)
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) (a.mul b)) = F (Quot.mk (Rel R X) (a.mul b))

Tactic:
| mul a b ha hb =>

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
x : E
⊢ x ∈ f.domain ↔ x ∈ g.domain

Tactic:
mem_domain_iff,

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
x : E
⊢ (∃ y, (x, y) ∈ f.graph) ↔ ∃ y, (x, y) ∈ g.graph
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
⊢ ¬False ∧ ¬False

Tactic:
not_false_eq_true,

Goal state after:
R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ True ∧ True
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
⊢ ¬False ∧ ¬False ∧ ¬False

Tactic:
not_false_eq_true,

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
⊢ True ∧ True ∧ True
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∀ b ∈ range (n + 1), b ≠ k → (X ^ b).coeff k * r ^ (n - b) * ↑(n.choose b) = 0

pp: case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0

Tactic:
· intro _ _ h
    simp [coeff_X_pow, h.symm]

Goal state after:
case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ ↑p.natDegree ≤ q.degree

Tactic:
exact le_degree_of_ne_zero h

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

Tactic:
exact le_degree_of_ne_zero h

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

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

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

Tactic:
· intro h
    apply_fun fun p => p.coeff 0 at h
    simpa using h

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

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

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

Tactic:
· intro h
    apply_fun fun p => p.coeff 0 at h
    simpa using h

Goal state after:
case mpr
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
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
hp : p ≠ 0
hq : q ≠ 0
⊢ ↑p.natDegree + q.degree ≤ (p * q).degree

Tactic:
degree_eq_natDegree hq

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ↑p.natDegree + ↑q.natDegree ≤ (p * q).degree
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
hp : p ≠ 0
hq : q ≠ 0
⊢ ↑p.natDegree + q.degree = ↑p.natDegree + ↑q.natDegree

Tactic:
degree_eq_natDegree hq

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ↑p.natDegree + ↑q.natDegree = ↑p.natDegree + ↑q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ ∑ x ∈ antidiagonal (df + dg), f.coeff x.1 * g.coeff x.2 = f.coeff df * g.coeff dg

Tactic:
Finset.sum_eq_single_of_mem (df, dg)

Goal state after:
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ f.coeff (df, dg).1 * g.coeff (df, dg).2 = f.coeff df * g.coeff dg

case h
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (df, dg) ∈ antidiagonal (df + dg)

case h₀
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ ∀ b ∈ antidiagonal (df + dg), b ≠ (df, dg) → f.coeff b.1 * g.coeff b.2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: S : Type v
inst✝ : Semiring S
r : S
⊢ (X + C r).leadingCoeff = 1

Tactic:
rw [← pow_one (X : S[X]), leadingCoeff_X_pow_add_C zero_lt_one]

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ ↑p.natDegree ≤ ↑p.natDegree + q.degree

Tactic:
degree_eq_natDegree hq

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ ↑p.natDegree ≤ ↑p.natDegree + ↑q.natDegree
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' + b.sumElim b' = x.sumElim y

Tactic:
← sumElim_add,

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 + b).sumElim (a' + b') = x.sumElim y
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : Preorder ι
inst✝¹ : DecidableEq ι
inst✝ : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f i < f j
⊢ toColex (f ∘ ⇑(Equiv.swap i j)) < toColex f

Tactic:
by
  rw [Equiv.swap_comm]
  exact lex_desc (ι := ιᵒᵈ) h₁ h₂

Goal state after:
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 : α) → Zero (N a)
f : Π₀ (a : α), N a
a✝ : α
⊢ a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support

Tactic:
mem_neLocus,

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a✝ : α
⊢ f a✝ ≠ 0 a✝ ↔ a✝ ∈ f.support
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ Q = 0

Tactic:
suffices ∀ i, P.coeff i • Q = 0 by
    rw [← leadingCoeff_eq_zero]
    apply h
    simpa [ext_iff, mul_comm Q.leadingCoeff] using fun i ↦ congr_arg (·.coeff Q.natDegree) (this i)

Goal state after:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ ∀ (i : ℕ), P.coeff i • Q = 0
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: 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
hl : (P.coeff l • Q).natDegree = Q.natDegree
this : P.coeff l * Q.leadingCoeff = 0
⊢ (P.coeff l • Q).leadingCoeff = 0

Tactic:
← coeff_natDegree,

Goal state after:
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
this : P.coeff l * Q.leadingCoeff = 0
⊢ (P.coeff l • Q).coeff (P.coeff l • Q).natDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
r : R
⊢ (map f) (eval₂ C g (C r)) = eval₂ C (⇑(map f) ∘ g) ((map f) (C r))

Tactic:
rw [eval₂_C, map_C, map_C, eval₂_C]

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
⊢ (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)

Tactic:
apply MvPolynomial.induction_on p
  · intro r
    rw [eval₂_C, map_C, map_C, eval₂_C]
  · intro p q hp hq
    rw [eval₂_add, (map f).map_add, hp, hq, (map f).map_add, eval₂_add]
  · intro p s hp
    rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X,
      comp_apply]

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∑ a ∈ x.support, (Finsupp.single (f a) (x a)) i ≠ 0
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
contrapose! hi

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
⊢ ∑ a ∈ x.support, (Finsupp.single (f a) (x a)) i = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : σ →₀ ℕ
h : s ∈ p.support
i : σ
hi : i ∈ s.support
⊢ i ∈ p.vars

Tactic:
contrapose! hi

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : σ →₀ ℕ
h : s ∈ p.support
i : σ
hi : i ∉ p.vars
⊢ i ∉ s.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
⊢ degreeOf i (X j) = if i = j then 1 else 0

Tactic:
by_cases c : i = j

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0

case neg
R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : ¬i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
⊢ degreeOf i (X j) = if i = j then 1 else 0

Tactic:
by_cases c : i = j
  · simp only [c, if_true, degreeOf_def, degrees_X, Multiset.count_singleton]
  simp [c, degreeOf_def, degrees_X]

Goal state after:
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₂
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S₂
f : S₁ →ₐ[R] S₂
x✝ : MvPolynomial σ S₂
⊢ ↑x✝.coeffs ⊆ range ⇑↑f ↔ ↑x✝.coeffs ⊆ ↑(Subalgebra.toSubmodule f.range)

Tactic:
simp [Set.subset_def]

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

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ p.totalDegree

pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
· rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ p.totalDegree ≤ (p + q).totalDegree
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
g : σ → T
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
induction p using MvPolynomial.induction_on with
  | C r => simp [← IsScalarTower.algebraMap_apply]
  | add p q hp hq => simp [hp, hq]
  | mul_X p i h => cases i <;> simp [h]

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ ((rename f) φ).vars
⊢ i ∈ Finset.image f φ.vars

Tactic:
simp only [vars_def, Multiset.mem_toFinset, Finset.mem_image] at hi ⊢

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ ((rename f) φ).degrees
⊢ ∃ a ∈ φ.degrees, f a = i
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑(n * q.natDegree) ≤ ↑(p.natDegree * q.natDegree)

Tactic:
gcongr; exact le_natDegree_of_ne_zero (mem_support_iff.1 hn)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N : ℕ
f : R[X]
⊢ (reflect N f).support = image (⇑(revAt N)) f.support

Tactic:
cases f; ext1; simp [reflect]

Goal state after: