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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
⊢ 0 < x

Tactic:
by
  have h₁ : 0 ≤ x := by grind
  have h₂ : x ≠ 0 := by grind [= spectrum.zero_notMem_iff]
  exact lt_of_le_of_ne h₁ h₂.symm

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

Goal state before:
pp: R✝ : Type u
M✝ : Type v
ι : Type w
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ #{ i // p i ≠ ⊥ } < ℵ₀

Tactic:
refine lt_of_le_of_lt hp.subtype_ne_bot_le_finrank_aux ?_

Goal state after:
R✝ : Type u
M✝ : Type v
ι : Type w
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ ↑(finrank R M) < ℵ₀
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommGroup V'
inst✝³ : Module K V
inst✝² : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
inst✝¹ : Nontrivial V
inst✝ : Nontrivial V'
v : V
hv : v ≠ 0
w : V'
hw : w ≠ 0
this : v ∉ ⊥
g : V →ₗ[K] V'
left✝ : g ∘ₗ ⊥.subtype = 0
hg : g v = w
⊢ g v ≠ 0 v

Tactic:
by simp_all

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
⊢ eval₂ f (f r) p = 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 (eval r p)
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
x : ↥(sSup (domain '' c))
this : ∃ y ∈ domain '' c, ↑x ∈ y
⊢ ∃ x_1, ↑x ∈ (↑x_1).domain

Tactic:
Set.exists_mem_image,

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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
x : ↥(sSup (domain '' c))
this : ∃ x_1 ∈ c, ↑x ∈ x_1.domain
⊢ ∃ x_1, ↑x ∈ (↑x_1).domain
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.comp q = p.sum fun e a ↦ C a * q ^ e

Tactic:
by rw [comp, eval₂_eq_sum]

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

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

Tactic:
Nat.isUnit_iff,

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

Goal state before:
pp: p : ℕ
hp✝ : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
⊢ m = 1 → p ≤ n

Tactic:
by simp_all

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 : E →ₗ.[R] F
⊢ Submodule.map (LinearMap.fst R E F) f.graph = f.domain

Tactic:
by
  ext x
  simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
    LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
  constructor <;> intro h
  · rcases h with ⟨x, hx, _⟩
    exact hx
  · use f ⟨x, h⟩
    simp only [h, exists_const]

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

Goal state before:
pp: case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)

Tactic:
by_cases d2 : 2 ∣ n <;> simp only [d2, ↓reduceIte]

Goal state after:
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ n.minFacProp 2

case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (n.minFacAux 3)
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac

Tactic:
· exact (minFac_prime n1).pos

Goal state after:
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 : ℕ
H1 : Nat.find ⋯ ∣ x
⊢ ↑x = 0

Tactic:
rw [← Nat.mul_div_cancel' H1, Nat.cast_mul,
            of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
            zero_mul]

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

Goal state before:
pp: n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
this : n.minFac = 1
⊢ False

Tactic:
by simp_all

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]
⊢ (Multiset.prod (Quot.mk (⇑(List.isSetoid R[A])) a✝)).coeff.support.sup degb ≤
    (Multiset.map (fun f ↦ f.coeff.support.sup degb) (Quot.mk (⇑(List.isSetoid R[A])) a✝)).sum

Tactic:
Multiset.quot_mk_to_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 ≤ (Multiset.map (fun f ↦ f.coeff.support.sup degb) ↑a✝).sum
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree

Tactic:
rw [Nat.cast_withBot]

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree
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
    exact h rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).degree ≤ p.degree

Tactic:
by
  apply sup_mono
  simpa using Finset.erase_subset ..

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

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

Tactic:
have : coeff p (natDegree q) = 0 := coeff_natDegree_eq_zero_of_degree_lt h

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree < q.degree
this : p.coeff q.natDegree = 0
⊢ (p + q).leadingCoeff = q.leadingCoeff
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe
a✝ : ℕ
h : ↑1 ≤ ↑a✝
⊢ 1 ≤ ↑a✝

Tactic:
WithBot.coe_one

Goal state after:
case coe
a✝ : ℕ
h : 1 ≤ ↑a✝
⊢ 1 ≤ ↑a✝
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ + ↑1 ≤ ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝

Tactic:
WithBot.coe_one

Goal state after:
case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ + 1 ≤ ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
ha : ¬IsUnit a
hap : a ∣ p
⊢ 0 < a.degree

Tactic:
contrapose! ha with h
  rw [Polynomial.eq_C_of_degree_le_zero h] at hap ⊢
  simpa [hp.C_dvd_iff_isUnit, isUnit_C] using hap

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt
        have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi
        calc
          (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
          _ < i * p.natDegree + p.natDegree := by gcongr

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]
n : ℕ
hn : p.natDegree < n
x : S
⊢ eval₂ f x p = ∑ i ∈ range n, f (p.coeff i) * x ^ i

Tactic:
eval₂_eq_sum,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ (p.sum fun e a ↦ f a * x ^ e) = ∑ i ∈ range n, f (p.coeff i) * x ^ i
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ (single a (f a)).sum g ≤ f.sum g

Tactic:
rw [sum, support_single _ H, sum_singleton, single_eq_same]
    apply Finset.single_le_sum (fun i hi ↦ h i (f i))
    simpa [mem_support_iff, ne_eq] using H

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ (aeval x) p = ∑ i ∈ range n, p.coeff i • x ^ i

Tactic:
simp_rw [Algebra.smul_def]
  exact eval₂_eq_sum_range' (algebraMap R S) hn x

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

Goal state before:
pp: case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval₂ (RingHom.id S) z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ f.coeff i * z ^ i

Tactic:
eval₂_eq_sum,

Goal state after:
case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ f.sum fun e a ↦ (RingHom.id S) a * z ^ e
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ f.coeff i * z ^ 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 : α) → Zero (N a)
f : Π₀ (a : α), N a
⊢ f.neLocus 0 = f.support

Tactic:
ext
  rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
⊢ ∏ y ∈ t, X y ^ x y = (monomial (Finsupp.indicator t fun i x_1 ↦ x i)) 1

Tactic:
rw [monomial_eq, C_1, one_mul, Finsupp.prod, Finset.prod_subset (support_indicator_subset _ _)]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
⊢ ∏ y ∈ t, X y ^ x y = ∏ x_1 ∈ t, X x_1 ^ (Finsupp.indicator t fun i x_2 ↦ x i) x_1

R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
⊢ ∀ x_1 ∈ t, x_1 ∉ (Finsupp.indicator t fun i x_2 ↦ x i).support → X x_1 ^ (Finsupp.indicator t fun i x_2 ↦ x i) x_1 = 1
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
⊢ motive ((monomial s) a)

Tactic:
apply @Finsupp.induction σ ℕ _ _ s

Goal state after:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
⊢ motive ((monomial 0) a)

case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
⊢ ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    a_1 ∉ f.support → b ≠ 0 → motive ((monomial f) a) → motive ((monomial (Finsupp.single a_1 b + f)) a)
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddLeftStrictMono (α i)
x✝³ x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex (x✝³ + x✝²)) a) ((ofLex (x✝³ + x✝¹)) a)

Tactic:
dsimp; gcongr

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddRightStrictMono (α i)
f x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex (Function.swap (fun x1 x2 ↦ x1 + x2) f x✝²)) a)
    ((ofLex (Function.swap (fun x1 x2 ↦ x1 + x2) f x✝¹)) a)

Tactic:
dsimp; gcongr

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
p : MvPolynomial σ R
⊢ p.coeffs = ∅

Tactic:
simpa [coeffs] using Subsingleton.eq_zero p

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 : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (Finsupp.mapDomain f d) ((rename f) φ) = coeff d φ

Tactic:
induction φ using MvPolynomial.induction_on' with
  | monomial u r =>
    rw [rename_monomial, coeff_monomial, coeff_monomial]
    simp only [(Finsupp.mapDomain_injective hf).eq_iff]
  | add =>
    simp only [*, map_add, coeff_add]

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S₁
p q : MvPolynomial σ R
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : CommSemiring B
inst✝² : Algebra S R
inst✝¹ : Algebra S A
inst✝ : Algebra S B
f : R →ₐ[S] A
X : σ → A
r : S
⊢ (↑↑(eval₂Hom (↑f) X)).toFun ((algebraMap S (MvPolynomial σ R)) r) = (algebraMap S A) r

Tactic:
by
      simp [IsScalarTower.algebraMap_eq S R (MvPolynomial σ R), algebraMap_eq]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ reflect n 1 = X ^ n

Tactic:
← C.map_one,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ reflect n (C 1) = X ^ n
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : f = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

pp: case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
· rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
⊢ reflect (f.natDegree + g.natDegree) (f * g) = reflect f.natDegree f * reflect g.natDegree g

Tactic:
reflect_mul f g rfl.le rfl.le

Goal state after:
R : Type u_1
inst✝ : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
⊢ reflect f.natDegree f * reflect g.natDegree g = reflect f.natDegree f * reflect g.natDegree g
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons (j 0) j.tail
⊢ False

Tactic:
cons_tail

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : ¬coeff m f = 0
⊢ ¬coeff (cons (m 0) m.tail) f = 0

Tactic:
by simpa using h

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ m 0 = i
⊢ ¬coeff (cons (m 0) m.tail) f = 0 ∧ cons (m 0) m.tail = m

Tactic:
cons_tail

Goal state after:
case h
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ m 0 = i
⊢ ¬coeff m f = 0 ∧ m = m
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
φ_k : ∀ (f : R[X]), f.natDegree < k → φ f = 0
φ_mon : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = n - k
⊢ ∀ {n : ℕ}, n ≤ k → n - k = 0

Tactic:
by simp_all

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (Multiset.map leadingCoeff (Multiset.map f s.val)).prod ≠ 0

Tactic:
by simpa using h

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) (Multiset.map f s.val)).prod ≠ 0

Tactic:
by simpa using h

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ f_1 ∈ Multiset.map f s.val, f_1.Monic

Tactic:
by simpa using h

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
f : ι → R[X]
inst✝ : Nontrivial R
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ f_1 ∈ Multiset.map f s.val, f_1.Monic

Tactic:
by simpa using h

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

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Tactic:
· rintro h f g - hg rfl hdg
    exact h g hg hdg (dvd_mul_left g f)

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.coeff p.natDegree = 1 ↔ p.coeff p.natDegree = 1

Tactic:
← @coeff_restriction _ _ p

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.coeff p.natDegree = 1 ↔ ↑(p.restriction.coeff p.natDegree) = 1
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x

Tactic:
by
  simp only [leadingCoeffNth, degreeLE, Submodule.mem_map, lcoeff_apply, Submodule.mem_inf,
    mem_degreeLE]
  constructor
  · rintro ⟨p, ⟨hpdeg, hpI⟩, rfl⟩
    rcases lt_or_eq_of_le hpdeg with hpdeg | hpdeg
    · refine ⟨0, I.zero_mem, bot_le, ?_⟩
      rw [leadingCoeff_zero, eq_comm]
      exact coeff_eq_zero_of_degree_lt hpdeg
    · refine ⟨p, hpI, le_of_eq hpdeg, ?_⟩
      rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]
  · rintro ⟨p, hpI, hpdeg, rfl⟩
    have : natDegree p + (n - natDegree p) = n :=
      add_tsub_cancel_of_le (natDegree_le_of_degree_le hpdeg)
    refine ⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩
    · apply le_trans (degree_mul_le _ _) _
      apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _
      rw [← Nat.cast_add, this]
    · rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < (p * X).degree
⊢ False

Tactic:
rw [← X_mul, congr_arg degree hp, degree_one, Nat.WithBot.lt_zero_iff, degree_eq_bot] at this

Goal state after:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p = 0
⊢ False
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: case refine_3
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝² : A
hx✝ : x✝² ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
x✝¹ : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
x✝ : y ∈ Algebra.adjoin R (↑S ∪ ↑T)
hx : x ∈ toSubmodule S * toSubmodule T
hy : y ∈ toSubmodule S * toSubmodule T
this : x * y ∈ toSubmodule S * (toSubmodule T * toSubmodule S)
⊢ x * y ∈ toSubmodule S * toSubmodule T

Tactic:
mul_comm T.toSubmodule,

Goal state after:
case refine_3
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝² : A
hx✝ : x✝² ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
x✝¹ : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
x✝ : y ∈ Algebra.adjoin R (↑S ∪ ↑T)
hx : x ∈ toSubmodule S * toSubmodule T
hy : y ∈ toSubmodule S * toSubmodule T
this : x * y ∈ toSubmodule S * (toSubmodule S * toSubmodule T)
⊢ x * y ∈ toSubmodule S * toSubmodule T
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ((aeval f) (p * (q * q'))) v = ((aeval f) (q' * (p * q))) v

Tactic:
rw [← mul_assoc, mul_comm]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a + b ≡ b [ZMOD n] ↔ n ∣ a

Tactic:
rw [add_comm, add_modEq_left_iff]

Goal state after: