mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R →+* S
s t : S
φ ψ : R[X]
⊢ f = g → s = t → φ = ψ → eval₂ f s φ = eval₂ g t ψ

Tactic:
rintro rfl rfl rfl

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
s : S
φ : R[X]
⊢ eval₂ f s φ = eval₂ f s φ
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h'
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = domain 0
h' : ∀ ⦃x : E⦄ ⦃hf : x ∈ (f + g).domain⦄ ⦃hg : x ∈ domain 0⦄, ↑(f + g) ⟨x, hf⟩ = ↑0 ⟨x, hg⟩
⊢ ↑f ⟨x, hf⟩ + ↑g ⟨x, hg⟩ = 0

Tactic:
zero_domain

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
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = ⊤
h' : ∀ ⦃x : E⦄ ⦃hf : x ∈ (f + g).domain⦄ ⦃hg : x ∈ domain 0⦄, ↑(f + g) ⟨x, hf⟩ = ↑0 ⟨x, hg⟩
⊢ ↑f ⟨x, hf⟩ + ↑g ⟨x, hg⟩ = 0
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
⊢ False

Tactic:
have hf0 : f0 (ι R x) = 0 := lift_ι_apply _ _

Goal state after:
R : Type u_1
X : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : f0 (ι R x) = 0
⊢ False
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ m

pp: case a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ n

Tactic:
· exact gcd_dvd_left _ _

Goal state after:
case a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ n
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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ x_fst ∈ map (LinearMap.fst R E F) g

Tactic:
simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]

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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ ∃ x, (x_fst, x) ∈ g
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ ∀ (m : M) (r : R) (x : R[M]),
    m ∉ x.coeff.support →
      r ≠ 0 →
        f (x • v) = (RingHom.id R[M]) x • f v → f ((single m r + x) • v) = (RingHom.id R[M]) (single m r + x) • f v

Tactic:
intro g

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
g : M
⊢ ∀ (r : R) (x : R[M]),
    g ∉ x.coeff.support →
      r ≠ 0 →
        f (x • v) = (RingHom.id R[M]) x • f v → f ((single g r + x) • v) = (RingHom.id R[M]) (single g r + x) • f v
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
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:
simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]
    intro h
    rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]

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

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∑ i ∈ s, f i) ≤ s.sup fun i ↦ supDegree D (f i)

Tactic:
classical
  simp only [supDegree, coeff_sum]
  grw [Finsupp.support_finsetSum, Finset.sup_biUnion]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.toFinsupp.coeff.support.Nonempty

Tactic:
support_toFinsupp,

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.support.Nonempty
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.natDegree
⊢ (p + C a).natDegree = p.natDegree

Tactic:
← natDegree_C a

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : (C a).natDegree < p.natDegree
⊢ (p + C a).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h✝ : ¬p.natDegree = q.natDegree
h : p.natDegree < q.natDegree
⊢ False

Tactic:
| inl h =>

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

Goal state before:
pp: case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
H' : j ≤ q.natDegree
⊢ False

Tactic:
exact
              ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
                h₁

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

Goal state before:
pp: case refine_1
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ max (supDegree D p) (supDegree D q) ≤ supDegree D p

pp: case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ supDegree D (p - q) ≠ supDegree D p

Tactic:
· rw [hd, sup_idem]

Goal state after:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ supDegree D (p - q) ≠ supDegree D p
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_zero]

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

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : s.erase i = ∅
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)

Tactic:
rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩

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

Goal state before:
pp: case neg.refine_2
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ≠ i ∧ j ∈ s
⊢ supDegree D (f j) < supDegree D (f i)

Tactic:
exact hmax j hj.2 hj.1

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

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j✝ : ι
hj✝ : j✝ ∈ s
hne✝ : f j✝ ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
this : ∀ k ∈ s, k ≠ i → supDegree D (f k) < supDegree D (f i)
⊢ supDegree D (∑ i ∈ s, f i) ≠ ⊥

Tactic:
(supDegree_leadingCoeff_sum_eq hi this).1

Goal state after:
case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j✝ : ι
hj✝ : j✝ ∈ s
hne✝ : f j✝ ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
this : ∀ k ∈ s, k ≠ i → supDegree D (f k) < supDegree D (f i)
⊢ supDegree D (f i) ≠ ⊥
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: S : Type v
inst✝ : Semiring S
c : S
⊢ (X + C c).nextCoeff = c

Tactic:
nontriviality S
  simp [nextCoeff_of_natDegree_pos]

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ i ∈ s✝, f i ≤ g i
s : ι
H : s ∉ f.support
⊢ f s ≤ g s

Tactic:
· exact notMem_support_iff.1 H ▸ zero_le

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p : R[X]
⊢ (p.comp (-X)).comp (-X) = p

Tactic:
rw [comp_assoc]
  simp only [neg_comp, X_comp, neg_neg, comp_X]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝ : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
exact lex_lt_of_lt_of_preorder hwf hlt

Goal state after:
Module: Mathlib.Order.PiLex

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

Tactic:
lt_toLex_update_self_iff,

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

Goal state before:
pp: S : Type v
inst✝ : CommSemiring S
⊢ aevalTower (AlgHom.id S S) = aeval

Tactic:
ext s

Goal state after:
S : Type v
inst✝ : CommSemiring S
s : S
⊢ (aevalTower (AlgHom.id S S) s) X = (aeval s) X
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ = (↑(f.support ∪ g.support))ᶜ

Tactic:
by ext; simp [inf_eq_and_sup_eq_iff]

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

Goal state before:
pp: case add
R : Type u
A : Type z
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
q : Submodule R M
m : M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hm : m ∈ q
a : A
hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q
f₁ f₂ : R[X]
h₁ : (aeval a) f₁ • m ∈ q
h₂ : (aeval a) f₂ • m ∈ q
⊢ (aeval a) f₁ • m + (aeval a) f₂ • m ∈ q

Tactic:
exact Submodule.add_mem q 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 : α) → AddGroup (N a)
f g₁ g₂ : Π₀ (a : α), N a
⊢ (f - g₁).neLocus (f - g₂) = g₁.neLocus g₂

Tactic:
simp only [sub_eq_add_neg, @neLocus_add_left α N _ _ _, neLocus_neg_neg]

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

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

Tactic:
rintro rfl rfl rfl

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f₁ : R →+* S₁
g₁ : σ → S₁
p₁ : MvPolynomial σ R
⊢ (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₁ g₁) p₁
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ 0 ∉ p.coeffs

Tactic:
intro hz

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
hz : 0 ∈ p.coeffs
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ (p * q).degrees ≤ p.degrees + q.degrees

Tactic:
by
  classical
  simp_rw [degrees_def]
  exact supDegree_mul_le (map_add _)

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

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

Tactic:
obtain si | si := eq_or_lt_of_le <| Nat.zero_le (s i)

Goal state after:
case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : 0 = s i
⊢ s i ≤ degreeOf i p

case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : 0 < s i
⊢ s i ≤ degreeOf i p
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ 0
⊢ x ∈ 1

Tactic:
simp only [mem_degreesLE, nonpos_iff_eq_zero] at hx

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
⊢ x ∈ 1
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
this : x = C (coeff 0 x)
⊢ x ∈ 1

Tactic:
exact ⟨x.coeff 0, by simp [Algebra.smul_def, ← this]⟩

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
hm.irreducible_iff_natDegree',

Goal state after:
case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ ¬(p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
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
⊢ #(C x * X ^ k + C y * X ^ m + C z * X ^ n).support = 3

Tactic:
exact card_support_trinomial hkm hmn hx hy hz

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
· rw [Set.not_nonempty_iff_eq_empty] at s_emp
    rw [s_emp, Submodule.span_empty]
    exact ⟨0, bot_le⟩

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤
    span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)

Tactic:
span_mul_span,

Goal state after:
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ span (↥(Algebra.adjoin A ↑s)) (↑(insert 1 y) * ↑(insert 1 y)) ≤ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ↑⊤ = Set.univ

Tactic:
coe_top

Goal state after:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ Set.univ = Set.univ
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A → ∃ ι x f, Surjective ⇑f

Tactic:
iff_quotient_freeAlgebra

Goal state after:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))

Tactic:
simp only [hS, top_toSubmodule, Submodule.mem_top]

Goal state after:
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]
hpq : IsCoprime p q
v : M
hv : v ∈ ((aeval f) p).ker ⊓ ((aeval f) q).ker
⊢ v ∈ ⊥

Tactic:
rcases hpq with ⟨p', q', hpq'⟩

Goal state after:
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).ker ⊓ ((aeval f) q).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ v ∈ ⊥
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]
hpq : IsCoprime p q
v : M
a✝ : v ∈ ⊤
⊢ ∃ y ∈ ((aeval f) p).range, ∃ z ∈ ((aeval f) q).range, y + z = v

Tactic:
rcases hpq with ⟨p', q', hpq'⟩

Goal state after:
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
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ y ∈ ((aeval f) p).range, ∃ z ∈ ((aeval f) q).range, y + z = v
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]
hpq : IsCoprime p q
v : M
hv : v ∈ ((aeval f) (p * q)).ker
⊢ ∃ y ∈ ((aeval f) p).ker, ∃ z ∈ ((aeval f) q).ker, y + z = v

Tactic:
rcases hpq with ⟨p', q', hpq'⟩

Goal state after:
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
⊢ ∃ y ∈ ((aeval f) p).ker, ∃ z ∈ ((aeval f) q).ker, y + z = v
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ f ∈ Ideal.map C I → ∀ (m : σ →₀ ℕ), coeff m f ∈ I

Tactic:
intro hf
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
    · intro f hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [Ne.symm h]
    · simp
    · exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
    · intro f g _ hg n
      rw [smul_eq_mul, coeff_mul]
      exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)

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

Goal state before:
pp: m a b c : ℤ
hc : c ≠ 0
⊢ a * c ≡ b * c [ZMOD m * c] → a ≡ b [ZMOD m]

Tactic:
simp only [modEq_iff_dvd, ← Int.sub_mul]
  exact Int.dvd_of_mul_dvd_mul_right hc

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
⊢ Surjective ⇑(quotientInfToPiQuotient I)

Tactic:
intro g

Goal state after:
case intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
⊢ ∃ a, (quotientInfToPiQuotient I) a = g
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card αˣ = Nat.card α - 1

Tactic:
classical
  rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]
  rcases finite_or_infinite {a : α // a ≠ 0}
  · rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
  · rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]

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

Goal state before:
pp: n : ℕ
⊢ Coprime 2 n ↔ Odd n

Tactic:
rw [prime_two.coprime_iff_not_dvd, ← not_even_iff_odd, even_iff_two_dvd]

Goal state after:
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
⊢ a ≠ b

Tactic:
by_contra hab

Goal state after:
case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
hab : a = b
⊢ False