mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case refine_3
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 : ∑ e ∈ t', g e • e = 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, f x ≠ 0

Tactic:
· obtain ⟨x₁, x₁_mem', rfl⟩ := Finset.mem_map.mp x₁_mem
    have := mem_erase.mp x₁_mem'
    exact ⟨x₁, by
      simpa only [f, Embedding.coeFn_mk, sub_add_cancel, this.2, true_and, if_neg this.1]⟩

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
K : Type u_7
L : Type u_8
E : Type u_9
F : Type u_10
inst✝⁵ : DivisionRing K
inst✝⁴ : DivisionRing L
σ : K →+* L
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : AddCommGroup F
inst✝ : Module L F
x : E
y : F
hx : x ≠ 0
c : K
hc✝ : c • x = 0
hc : c = 0
⊢ 0 • y = 0

Tactic:
zero_smul

Goal state after:
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
K : Type u_7
L : Type u_8
E : Type u_9
F : Type u_10
inst✝⁵ : DivisionRing K
inst✝⁴ : DivisionRing L
σ : K →+* L
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : AddCommGroup F
inst✝ : Module L F
x : E
y : F
hx : x ≠ 0
c : K
hc✝ : c • x = 0
hc : c = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
⊢ c ≤ Module.rank K V ↔ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
by
  have := nontrivial_of_invariantBasisNumber K
  constructor
  · intro h
    obtain ⟨κ, t'⟩ := Module.Free.exists_basis (R := K) (M := V)
    let t := t'.reindexRange
    have : LinearIndepOn K id (Set.range t') := by
      convert! t.linearIndependent.linearIndepOn_id
      ext
      simp [t]
    rw [← t.mk_eq_rank'', le_mk_iff_exists_subset] at h
    rcases h with ⟨s, hst, hsc⟩
    exact ⟨s, hsc, this.mono hst⟩
  · rintro ⟨s, rfl, si⟩
    exact si.cardinal_le_rank

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

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hv : ∀ (v : V), ∃ r, r • v₀ = v
hzero : v₀ = 0
⊢ False

Tactic:
simp_rw [hzero, smul_zero, exists_const] at hv

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
⊢ False
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
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
⊢ (f ∘ₗ g).ker = f.ker ⊔ g.ker

Tactic:
by
  suffices ∀ x, f x = 0 → f (g x) = 0 by rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']; simpa
  intro x hx
  rw [← comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_apply, hx, map_zero]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ ∀ (x : FreeAlgebra R X), (n + 1) • x = n • x + x

Tactic:
by
    rintro ⟨a⟩
    dsimp only [HSMul.hSMul, SMul.smul, NSMul.nsmul, Quot.map]
    rw [map_add, map_one, mk_mul, mk_mul, ← add_one_mul (_ : FreeAlgebra R X)]
    congr 1
    exact Quot.sound Rel.add_scalar

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
W : Type u_1
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Module A V
inst✝³ : AddCommGroup W
inst✝² : Module K W
inst✝¹ : Module A W
inst✝ : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
⊢ Surjective ⇑f

Tactic:
change Surjective (f.restrictScalars K)

Goal state after:
K : Type u
V : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
W : Type u_1
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Module A V
inst✝³ : AddCommGroup W
inst✝² : Module K W
inst✝¹ : Module A W
inst✝ : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
⊢ Surjective ⇑(↑K f)
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
f g : E →ₛₗ.[σ] F
⊢ f - g = f + -g

Tactic:
ext x _ h

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

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 : E →ₛₗ.[σ] F
x : E
hf✝ : x ∈ (f - g).domain
h : x ∈ (f + -g).domain
⊢ ↑(f - g) ⟨x, hf✝⟩ = ↑(f + -g) ⟨x, h⟩
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
f g : E →ₛₗ.[σ] F
⊢ -(f + g) = -g + -f

Tactic:
ext x _ h

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

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 : E →ₛₗ.[σ] F
x : E
hf✝ : x ∈ (-(f + g)).domain
h : x ∈ (-g + -f).domain
⊢ ↑(-(f + g)) ⟨x, hf✝⟩ = ↑(-g + -f) ⟨x, h⟩
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case right_distrib
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
⊢ (liftFun R X f a✝ + liftFun R X f b✝) * liftFun R X f c✝ =
    liftFun R X f a✝ * liftFun R X f c✝ + liftFun R X f b✝ * liftFun R X f c✝

Tactic:
rw [right_distrib]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.of
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✝ : X
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.of a✝)) = F (Quot.mk (Rel R X) (Pre.of a✝))

Tactic:
change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _

Goal state after:
case mk.of
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✝ : X
⊢ (⇑F ∘ ι R) a✝ = F (Quot.mk (Rel R X) (Pre.of a✝))
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case monomial
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
n : ℕ
b : R
⊢ eval x (C a * (monomial n) b) = a * eval x ((monomial n) b)

Tactic:
| monomial n b =>

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

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

Tactic:
| monomial n b =>

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

Goal state before:
pp: case monomial
R : Type u
a : R
inst✝ : Semiring R
p r : R[X]
n : ℕ
b : R
⊢ (C a * (monomial n) b).comp r = C a * ((monomial n) b).comp r

Tactic:
| monomial n b =>

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

Goal state before:
pp: n : ℕ
n1 : n ≠ 1
⊢ n.minFacProp n.minFac

Tactic:
by
  by_cases n0 : n = 0
  · simp [n0, minFacProp]
  have n2 : 2 ≤ n := by
    revert n0 n1
    rcases n with (_ | _ | _) <;> simp [succ_le_succ]
  simp only [minFac_eq]
  by_cases d2 : 2 ∣ n <;> simp only [d2, ↓reduceIte]
  · exact ⟨le_rfl, d2, fun k k2 _ => k2⟩
  · refine
      minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt ?_ d2)
    exact fun e => e.symm ▸ d

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
⊢ (p * X ^ n).coeff (d - n + n) = p.coeff (d - n + n - n)

Tactic:
coeff_mul_X_pow,

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
⊢ p.coeff (d - n) = p.coeff (d - n + n - n)
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
P : R[X]
⊢ ∀ ⦃a₂ : R[X]⦄, (fun x ↦ X ^ n * x) P = (fun x ↦ X ^ n * x) a₂ → P = a₂

Tactic:
Q

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
P Q : R[X]
⊢ (fun x ↦ X ^ n * x) P = (fun x ↦ X ^ n * x) Q → P = Q
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.natDegree

Tactic:
← Nat.cast_le (α := WithBot ℕ),

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
⊢ (p - q).degree ≤ max p.degree q.degree

Tactic:
by
  simpa only [degree_neg q] using! degree_add_le p (-q)

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (p * C a).degree = p.degree

Tactic:
by
  obtain rfl | hp := eq_or_ne p 0
  · simp
  nontriviality R
  rw [degree_mul', degree_C ha.ne_zero]
  · simp
  · simpa [ha.mul_left_eq_zero]

Goal state after:
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
⊢ a ∈ f.support

Tactic:
simpa [mem_support_iff, ne_eq] using H

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

Goal state before:
pp: case add
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
p q : R[X]
hp : (aeval (MulOpposite.op x)) p = MulOpposite.op ((aeval x) p)
hq : (aeval (MulOpposite.op x)) q = MulOpposite.op ((aeval x) q)
⊢ (aeval (MulOpposite.op x)) (p + q) = MulOpposite.op ((aeval x) (p + q))

Tactic:
simp [map_add, hp, hq]

Goal state after:
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 default < y default ∨ ∀ (x_1 : ι), ofLex x x_1 = ofLex y x_1) ↔ x default < y default ∨ x default = y default

Tactic:
Unique.forall_iff,

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
⊢ x default < y default ∨ ofLex x default = ofLex y default ↔ x default < y default ∨ x default = y default
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (β i)
x y : Colex ((i : ι) → β i)
⊢ (x default < y default ∨ ∀ (x_1 : ι), ofColex x x_1 = ofColex y x_1) ↔ x default < y default ∨ x default = y default

Tactic:
Unique.forall_iff,

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (β i)
x y : Colex ((i : ι) → β i)
⊢ x default < y default ∨ ofColex x default = ofColex y default ↔ x default < y default ∨ x default = y default
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
x✝ : IsUnit (X - C r)
g : R[X]
_hfg : (X - C r) * g = 1
hgf : g * (X - C r) = 1
⊢ eval ?m.92 (?m.91 * (X - C ?m.92)) = 1

pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
x✝ : IsUnit (X - C r)
g : R[X]
_hfg : (X - C r) * g = 1
hgf : g * (X - C r) = 1
⊢ R

pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
x✝ : IsUnit (X - C r)
g : R[X]
_hfg : (X - C r) * g = 1
hgf : g * (X - C r) = 1
⊢ R[X]

Tactic:
hgf,

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
x✝ : IsUnit (X - C r)
g : R[X]
_hfg : (X - C r) * g = 1
hgf : g * (X - C r) = 1
⊢ eval r 1 = 1
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case h
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 : ℕ
hi : i > P.natDegree
⊢ 0 • Q = 0

Tactic:
zero_smul

Goal state after:
case h
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 : ℕ
hi : i > P.natDegree
⊢ 0 = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ f.comp singleZeroRingHom = g.comp singleZeroRingHom

Tactic:
ext x
    exact hC _

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : Decidable (a = 0)
⊢ ((monomial s) a).support = if a = 0 then ∅ else {s}

Tactic:
rw [← Subsingleton.elim (Classical.decEq R a 0) h]

Goal state after:
R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : Decidable (a = 0)
⊢ ((monomial s) a).support = if a = 0 then ∅ else {s}
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P : MvPolynomial σ R
⊢ ∀ ⦃a₂ : MvPolynomial σ R⦄, (fun x ↦ X n * x) P = (fun x ↦ X n * x) a₂ → P = a₂

Tactic:
Q

Goal state after:
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
⊢ (fun x ↦ X n * x) P = (fun x ↦ X n * x) Q → P = Q
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q, p = (rename f) q

Tactic:
obtain ⟨s, q, rfl⟩ := exists_finset_rename p
  let n := Fintype.card { x // x ∈ s }
  let e := Fintype.equivFin { x // x ∈ s }
  refine ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, ?_⟩
  rw [← rename_rename, rename_rename e]
  simp only [Function.comp_def, Equiv.symm_apply_apply, rename_rename]

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
⊢ coeff d ((rename f) φ) = 0

Tactic:
rw [← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction

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

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

Tactic:
degreeOf_C

Goal state after:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
h : i ≠ j
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
⊢ p = X ^ p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
  · nontriviality R
    rw [h, natTrailingDegree_X_pow, ← h]
  · ext n
    rw [coeff_X_pow]
    obtain hn | rfl | hn := lt_trichotomy n p.natDegree
    · rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree (hn.trans_le h)]
    · simpa only [if_pos rfl] using! h₁.leadingCoeff
    · rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.natDegree = f.natDegree - 1

Tactic:
refine f.eraseLead_natDegree_le.antisymm <| le_natDegree_of_ne_zero ?_

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.coeff (f.natDegree - 1) ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hq : q.natDegree ≠ 0
⊢ (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
← coeff_comp_degree_mul_degree hq,

Goal state after:
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hq : q.natDegree ≠ 0
⊢ (p.comp q).leadingCoeff = (p.comp q).coeff (p.natDegree * q.natDegree)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
i : ℕ
m : σ →₀ ℕ
hm : ¬coeff m (((optionEquivLeft R σ) p).coeff i) = 0
⊢ ¬coeff (optionElim i m).some (((optionEquivLeft R σ) p).coeff ((optionElim i m) none)) = 0

Tactic:
simpa using! hm

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : (p * q).Monic
⊢ q.Monic

Tactic:
contrapose hpq

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.Monic
⊢ ¬(p * q).Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : (p * q).Monic
⊢ p.Monic

Tactic:
contrapose hpq

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.Monic
⊢ ¬(p * q).Monic
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff ((revAt f.natDegree) 0) = f.leadingCoeff

Tactic:
revAt_le zero_le,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff (f.natDegree - 0) = f.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ p = 1

Tactic:
convert! eq_C_of_degree_eq_zero hdeg

Goal state after:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ 1 = C (p.coeff 0)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ q * p ≠ 0

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ q * p ≠ 0

Tactic:
· simpa [h]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ q * p ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ p * q ≠ 0

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0

Tactic:
· simpa [h]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x ∈ Subalgebra.toSubmodule (adjoin R s)

Tactic:
← hp'

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x ∈ span R p
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ p.degree < (X ^ n).degree

Tactic:
· simp [mem_degreeLT.1 hp]

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

Goal state before:
pp: case mp.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.coeff n

Tactic:
refine ⟨0, I.zero_mem, bot_le, ?_⟩
      rw [leadingCoeff_zero, eq_comm]
      exact coeff_eq_zero_of_degree_lt hpdeg

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

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ i, ∃ p ∈ I, p.degree ≤ ↑i ∧ p.leadingCoeff = x) → ∃ p ∈ I, p.leadingCoeff = x

Tactic:
rintro ⟨i, p, hpI, _, rfl⟩
      exact ⟨p, hpI, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Subsemiring.closure (MulOpposite.unop ⁻¹' Set.range ⇑(algebraMap R A) ∪ MulOpposite.unop ⁻¹' s) =
    Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s)

Tactic:
congr with x

Goal state after:
case e_a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
⊢ x ∈ MulOpposite.unop ⁻¹' Set.range ⇑(algebraMap R A) ↔ x ∈ Set.range ⇑(algebraMap R Aᵐᵒᵖ)
Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ Subsemiring.closure (MulOpposite.op ⁻¹' Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.op ⁻¹' s) =
    Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ MulOpposite.op ⁻¹' s)

Tactic:
congr with x

Goal state after:
case e_a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
x : A
⊢ x ∈ MulOpposite.op ⁻¹' Set.range ⇑(algebraMap R Aᵐᵒᵖ) ↔ x ∈ Set.range ⇑(algebraMap R A)