mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴⁰ : CommRing S
inst✝³⁹ : Algebra R S
P : Type u_3
inst✝³⁸ : CommRing P
A✝ : Type u_4
inst✝³⁷ : CommRing A✝
K : Type u_5
B✝ : Type u_6
inst✝³⁶ : CommRing B✝
inst✝³⁵ : IsDomain B✝
inst✝³⁴ : Field K
L : Type u_7
inst✝³³ : Field L
inst✝³² : Algebra A✝ K
inst✝³¹ : IsFractionRing A✝ K
g : A✝ →+* L
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
x : FA
⊢ (ringEquivOfRingEquiv f.toRingEquiv).toFun ((algebraMap FA FB) x) = (algebraMap FA FC) x

Tactic:
obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective A x
    simp_rw [map_div₀, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B FB]
    simp [← IsScalarTower.algebraMap_apply A C FC]

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

Goal state before:
pp: A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
⊢ Injective ⇑(fieldEquivOfAlgEquivHom K L)

Tactic:
intro f g h

Goal state after:
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
f g : B ≃ₐ[A] B
h : (fieldEquivOfAlgEquivHom K L) f = (fieldEquivOfAlgEquivHom K L) g
⊢ f = g
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
S : Type u_4
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
M : Submonoid R
inst✝⁶ : IsLocalization M S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
⊢ ∀ (r : S), (↑↑f.toRingHom).toFun ((algebraMap S A) r) = (algebraMap S B) r

Tactic:
let f := f.comp (IsScalarTower.toAlgHom R S A)
    let g := IsScalarTower.toAlgHom R S B
    have : f.toRingHom.comp (algebraMap R S) = g.toRingHom.comp (algebraMap R S) := by simp
    suffices f = g by rwa [DFunLike.ext_iff] at this
    apply IsLocalization.algHom_ext M
    rwa [DFunLike.ext_iff] at this ⊢

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

Goal state before:
pp: case add
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
C : Type u_3
inst✝ : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp includeRight.toRingHom = g.comp includeRight.toRingHom
x y : A ⊗[R] B
a✝¹ : f x = g x
a✝ : f y = g y
⊢ f (x + y) = g (x + y)

Tactic:
| add x y _ _ =>

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

Goal state before:
pp: case add
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x y : A ⊗[R] B
a✝¹ : x ∈ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight)
a✝ : y ∈ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight)
⊢ x + y ∈ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight)

Tactic:
| add x y _ _ =>

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : StarAddMonoid R
inst✝ : Star A
a : A
⊢ IsSelfAdjoint ↑a ↔ IsSelfAdjoint a

Tactic:
simp only [isSelfAdjoint_iff, ← inr_star, inr_injective.eq_iff]

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
⊢ centralizer R (⇑includeRight '' S) = (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val).range

Tactic:
by
  have eq1 := centralizer_coe_image_includeLeft_eq_center_tensorProduct R B A S
  apply_fun Subalgebra.comap (Algebra.TensorProduct.comm R A B).toAlgHom at eq1
  convert! eq1
  · ext x
    simpa [mem_centralizer_iff] using
      ⟨fun h b hb ↦ (Algebra.TensorProduct.comm R A B).symm.injective <| by aesop, fun h b hb ↦
        (Algebra.TensorProduct.comm R A B).injective <| by aesop⟩
  · ext x
    simp only [AlgHom.mem_range, mem_comap, AlgEquiv.coe_toAlgHom]
    constructor
    · rintro ⟨x, rfl⟩
      exact ⟨(Algebra.TensorProduct.comm R _ _) x,
        by rw [Algebra.TensorProduct.comm_comp_map_apply]⟩
    · rintro ⟨y, hy⟩
      refine ⟨(Algebra.TensorProduct.comm R _ _) y, (Algebra.TensorProduct.comm R A B).injective ?_⟩
      rw [← hy, comm_comp_map_apply, ← Algebra.TensorProduct.comm_symm, AlgEquiv.symm_apply_apply]

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

Tactic:
by
  rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := A),
    ← centralizer_coe_map_includeLeft_eq_center_tensorProduct R A B ⊤]
  ext
  simp [includeLeft, includeLeftRingHom]

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

Goal state before:
pp: case inr
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
j i : n
⊢ ((bW.sumQuot bQ).coord (Sum.inr j)) ((bW.sumQuot bQ) (Sum.inr i)) =
    (bQ.coord j ∘ₗ W.mkQ) ((bW.sumQuot bQ) (Sum.inr i))

Tactic:
| inr i =>

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

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

Tactic:
← gsum,

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

Goal state before:
pp: case inr
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 : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ p x ⋯

Tactic:
· simpa using star _ (NonUnitalAlgebra.subset_adjoin R (by simpa using Or.inl hx)) (mem _ hx)

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
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this.extend ⋯)) K V := Basis.extend this
b_eq : b = Basis.extend this
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
⊢ Fintype.card ↑(this.extend ⋯) ≤ finrank K ↥S

Tactic:
←
            finrank_eq_card_basis b,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this.extend ⋯)) K V := Basis.extend this
b_eq : b = Basis.extend this
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
⊢ finrank K V ≤ finrank K ↥S
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 : V
hv : v ≠ 0
⊢ finrank K ↥(K ∙ v) = 1

Tactic:
by
  apply le_antisymm
  · exact finrank_span_le_card ({v} : Set V)
  · rw [Nat.succ_le_iff, finrank_pos_iff]
    use ⟨v, mem_span_singleton_self v⟩, 0
    apply Subtype.coe_ne_coe.mp
    simp [hv]

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

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

Tactic:
eval_eq_sum,

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ (p.sum fun e a ↦ f a * f r ^ e) = f (p.sum fun e a ↦ a * r ^ e)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : q.IsRoot a
⊢ eval a p * eval a q = 0

Tactic:
IsRoot.def.1 H,

Goal state after:
R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : q.IsRoot a
⊢ eval a p * 0 = 0
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : p.IsRoot a
⊢ eval a p * eval a q = 0

Tactic:
IsRoot.def.1 H,

Goal state after:
R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : p.IsRoot a
⊢ 0 * eval a q = 0
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ ¬p ∣ 2

Tactic:
exact fun h ↦ (Fact.out : 2 < p).not_ge <| Nat.le_of_dvd Nat.zero_lt_two h

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ 0 * r = 0

Tactic:
rw [zero_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

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

Tactic:
exact (existsUnique_from_graph @hg hadd).unique hvw hvw'

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

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

Tactic:
exact degtm a b

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

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

Tactic:
by
  rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]

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

Goal state before:
pp: case h
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List R[A]
⊢ (↑a✝).prod.coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) a✝).sum

Tactic:
Multiset.prod_coe

Goal state after:
case h
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List R[A]
⊢ a✝.prod.coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) a✝).sum
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f - g) ≤ supDegree D f ⊔ supDegree D g

Tactic:
rw [sub_eq_add_neg, ← supDegree_neg (f := g)]

Goal state after:
R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ degree 1 ≤ 0

Tactic:
by rw [← C_1]; exact degree_C_le

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

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

Tactic:
by
  rw [degree, support_monomial n ha, max_singleton, Nat.cast_withBot]

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

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

Tactic:
rw [C_mul_X_pow_eq_monomial, degree_monomial n ha]

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

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

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

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
· simp only [hp, zero_mul, leadingCoeff_zero]

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
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
⊢ leadingCoeff D (0 * q) = leadingCoeff D 0

Tactic:
rw [zero_mul]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
⊢ (Polynomial.map f p).IsRoot (f x)

Tactic:
rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x p = ∑ i ∈ range (p.natDegree + 1), p.coeff i * x ^ i

Tactic:
eval_eq_sum,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ (p.sum fun e a ↦ a * x ^ e) = ∑ i ∈ range (p.natDegree + 1), p.coeff i * x ^ i
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ eval x p = ∑ i ∈ range n, p.coeff i * x ^ i

Tactic:
eval_eq_sum,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ (p.sum fun e a ↦ a * x ^ e) = ∑ i ∈ range n, p.coeff i * x ^ i
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.coeff 0 = f.coeff f.natDegree

Tactic:
(degree_eq_iff_natDegree_eq _).1 dz

Goal state after:
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.coeff 0 = f.coeff Zero.zero

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
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
⊢ x ≤ y ↔ x default ≤ y default

Tactic:
by
  simp_rw [le_iff_lt_or_eq, Pi.Lex.lt_iff_of_unique, ← ofLex_inj, funext_iff, Unique.forall_iff,
    ofLex_apply]

Goal state after:
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : ∀ (i : ι), AddLeftMono (α i)
⊢ ∀ {a b : Π₀ (i : ι), α i}, a ≤ b → ∃ c, b = a + c

Tactic:
intro f g h

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : ∀ (i : ι), AddLeftMono (α i)
f g : Π₀ (i : ι), α i
h : f ≤ g
⊢ ∃ c, g = f + c
Module: Mathlib.Algebra.MvPolynomial.Eval

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

Tactic:
classical exact Finsupp.sum_add_index (by simp [f.map_zero]) (by simp [add_mul, f.map_add])

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

Goal state before:
pp: case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ d_1 ∈ φ.support, d_1 = d
⊢ coeff d φ = if d = d then coeff d φ else 0

Tactic:
if_pos rfl

Goal state after:
case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ d_1 ∈ φ.support, d_1 = d
⊢ coeff d φ = coeff d φ
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d₀ : σ →₀ ℕ
h : ∀ d ∈ φ.support, d = d₀
⊢ φ = (monomial d₀) (coeff d₀ φ)

Tactic:
by
  classical
  ext d
  rcases eq_or_ne d d₀ with rfl | hd
  · rw [coeff_monomial, if_pos rfl]
  · rw [notMem_support_iff.mp fun hmem ↦ hd (h d hmem), coeff_monomial, if_neg fun e ↦ hd e.symm]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
⊢ (if Finsupp.single i 1 = Finsupp.single i 1 then 1 else 0) = 1

Tactic:
if_pos rfl

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
⊢ 1 = 1
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ constantCoeff (C r) = r

Tactic:
by
  simp [constantCoeff_eq]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
⊢ constantCoeff (X i) = 0

Tactic:
by
  simp [constantCoeff_eq]

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

Goal state before:
pp: case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = (rename Subtype.val) q) →
      (∃ s q_1, q = (rename Subtype.val) q_1) → ∃ s q_1, p + q = (rename Subtype.val) q_1

Tactic:
rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
    refine ⟨s ∪ t, ⟨?_, ?_⟩⟩
    · refine rename (Subtype.map id ?_) p + rename (Subtype.map id ?_) q <;>
        simp +contextual only [id, true_or, or_true,
          Finset.mem_union, forall_true_iff]
    · simp only [rename_rename, map_add]
      rfl

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

Goal state before:
pp: case refine_1.mem_mul_mem
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) (m * n) ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
| mem_mul_mem m hm n hn =>

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

Goal state before:
pp: case monomial
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
d u : σ →₀ ℕ
r : R
⊢ coeff (Finsupp.mapDomain f d) ((rename f) ((monomial u) r)) = coeff d ((monomial u) r)

Tactic:
rw [rename_monomial, coeff_monomial, coeff_monomial]

Goal state after:
case monomial
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
d u : σ →₀ ℕ
r : R
⊢ (if Finsupp.mapDomain f u = Finsupp.mapDomain f d then r else 0) = if u = d then r else 0