mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : finrank K ↥S = 1
T : Submodule K V
hT : T < S
this : FiniteDimensional K ↥S
⊢ T = ⊥

Tactic:
have : FiniteDimensional K T := .of_injective (inclusion hT.le) (inclusion_injective hT.le)

Goal state after:
case refine_2
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : finrank K ↥S = 1
T : Submodule K V
hT : T < S
this✝ : FiniteDimensional K ↥S
this : FiniteDimensional K ↥T
⊢ T = ⊥
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
nz : v ≠ 0
⊢ K ∙ v = ⊤ ↔ ∀ (w : V), ∃ c, c • v = w

Tactic:
apply span_singleton_eq_top_iff

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (↑n).comp p = ↑n

Tactic:
by rw [← C_eq_natCast, C_comp]

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

Goal state before:
pp: n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ n.minFacProp (n.minFacAux x✝)

Tactic:
rw [minFacAux]
    by_cases h : n < k * k
    · have pp : Prime n :=
        prime_def_le_sqrt.2
          ⟨n2, fun m m2 l d => not_lt_of_ge l <| lt_of_lt_of_le (sqrt_lt.2 h) (a m m2 d)⟩
      simpa only [k, h] using
        ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩
    have k2 : 2 ≤ k := by
      subst e
      apply Nat.le_add_left
    simp only [k, h, ↓reduceIte]
    by_cases dk : k ∣ n <;> simp only [k, dk, ↓reduceIte]
    · exact ⟨k2, dk, a⟩
    · refine
        have := minFac_lemma n k h
        minFacAux_has_prop n2 (k + 2) (i + 1) (by simp [k, e, Nat.left_distrib, add_right_comm])
          fun m m2 d => ?_
      rcases Nat.eq_or_lt_of_le (a m m2 d) with rfl | ml
      · contradiction
      apply (Nat.eq_or_lt_of_le ml).resolve_left
      intro me
      rw [← me, e] at d
      have d' : 2 * (i + 2) ∣ n := d
      have := a _ le_rfl (dvd_of_mul_right_dvd d')
      rw [e] at this
      exact absurd this (by contradiction)

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
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.toLinearPMap.graph
⊢ (x_fst, x_snd) ∈ g

Tactic:
LinearPMap.mem_graph_iff

Goal state after:
case mp
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 : ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑g.toLinearPMap y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ g
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr
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, x_snd) ∈ g.toLinearPMap.graph

Tactic:
LinearPMap.mem_graph_iff

Goal state after:
case mpr
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
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑g.toLinearPMap y = (x_fst, x_snd).2
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∑ x ∈ antidiagonal 1, p.coeff x.1 * q.coeff x.2 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0

Tactic:
Nat.antidiagonal_eq_map

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∑ x ∈ Finset.map { toFun := fun i ↦ (i, 1 - i), inj' := ⋯ } (range (1 + 1)), p.coeff x.1 * q.coeff x.2 =
    p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k n : ℕ
⊢ (X ^ k).coeff n = if n = k then 1 else 0

Tactic:
simp only [one_mul, map_one, ← coeff_C_mul_X_pow]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ (C r * φ).coeff c

Tactic:
rw [coeff_C_mul]

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ r * φ.coeff c
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
natDegree_C_mul_of_isUnit,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ a * p.coeff p.natDegree = a * p.leadingCoeff

case ha
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ IsUnit a
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ f (eval x p) = 0

Tactic:
← eval₂_hom,

Goal state after:
S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ eval₂ f (f x) p = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case zero
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic D 1

Tactic:
exact monic_one hD

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ R[ X] = ⊤

Tactic:
refine top_unique fun p _hp => ?_
  set S := adjoin R ({X} : Set R[X])
  rw [← sum_monomial_eq p]; simp only [← smul_X_eq_monomial]
  exact S.sum_mem fun n _hn => S.smul_mem (S.pow_mem (subset_adjoin rfl) _) _

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
h : eval₂ f (f r) p = 0
⊢ f (eval r p) = f 0

Tactic:
← eval₂_hom,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
h : eval₂ f (f r) p = 0
⊢ eval₂ f (f r) p = f 0
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁴ : DecidableEq α
M : α → Type u_3
inst✝³ : (a : α) → Zero (N a)
inst✝² : (a : α) → Zero (M a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
hF : ∀ (a : α), Function.Injective (F a)
⊢ (mapRange F F0 f).neLocus (mapRange F F0 g) = f.neLocus g

Tactic:
by
  ext a
  simpa only [mem_neLocus] using! (hF a).ne_iff

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 : Π₀ (a : α), N a
⊢ f.neLocus g = (f - g).support

Tactic:
by
  rw [← @neLocus_add_right α N _ _ _ _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
⊢ (i = l → ¬j = m) → P.coeff i * Q.coeff j = 0

Tactic:
H

Goal state after:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
⊢ P.coeff i * Q.coeff j = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: 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)

Tactic:
change motive (monomial 0 a)
    exact C a

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p ≠ 0 ↔ ∃ d, coeff d p ≠ 0

Tactic:
by
  rw [Ne, eq_zero_iff]
  push Not
  rfl

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

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
⊢ r ∣ coeff c (C r * φ)

Tactic:
rw [coeff_C_mul]

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
⊢ r ∣ r * coeff c φ
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
⊢ (map f) ((rename g) p) = (rename g) ((map f) p)

Tactic:
apply MvPolynomial.induction_on p
    (fun a => by simp only [map_C, rename_C])
    (fun p q hp hq => by simp only [hp, hq, map_add]) fun p n hp => by
    simp only [hp, rename_X, map_X, map_mul]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ Finset.image (fun m ↦ coeff m 1) (support 1) ⊆ {1}

Tactic:
Finset.image_subset_iff

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ ∀ x ∈ support 1, coeff x 1 ∈ {1}
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
h✝ : a = 0
⊢ ⊥ ≤ toMultiset s

pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
h✝ : ¬a = 0
⊢ toMultiset s ≤ toMultiset s

Tactic:
exacts [bot_le, le_rfl]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
hb : toMultiset b ≤ t
⊢ (monomial a) (coeff i x) * (monomial b) 1 ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.degree ≤ ↑n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0

Tactic:
degree_le_iff_coeff_zero,

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ (∀ (m : ℕ), ↑n < ↑m → p.coeff m = 0) ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
⊢ (↑n).natTrailingDegree = 0

Tactic:
simp only [← C_eq_intCast, natTrailingDegree_C]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
P : MvPolynomial σ R
n : ℕ
⊢ ((uniqueAlgEquiv R σ) P).coeff n = coeff (Finsupp.single default n) P

Tactic:
by
  induction P using induction_on' with
  | monomial d r =>
      rw [uniqueAlgEquiv_monomial, Finsupp.unique_single d]
      simp [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial]
  | add P Q hP hQ =>
      simpa using congrArg₂ (· + ·) hP hQ

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
⊢ ↑t.prod.natDegree = (Multiset.map degree t).sum

Tactic:
natDegree_multiset_prod_of_monic _ h,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
⊢ ↑(Multiset.map natDegree t).sum = (Multiset.map degree t).sum
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ¬p.degree = ⊥

Tactic:
refine (lt_trans ?_ h).ne'

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

Goal state before:
pp: case refine_2
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)
r : A
hr : r ∈ Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ r ∈ span R (p * q)

Tactic:
← hq',

Goal state after:
case refine_2
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)
r : A
hr : r ∈ span (↥(adjoin R s)) q
⊢ r ∈ span R (p * q)
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_1
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ P (Algebra.adjoin R ↑∅)

pp: case refine_2
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ ∀ (a : A) (s : Finset A), a ∉ s → P (Algebra.adjoin R ↑s) → P (Algebra.adjoin R ↑(insert a s))

Tactic:
· simpa using base

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ ∀ (a : A) (s : Finset A), a ∉ s → P (Algebra.adjoin R ↑s) → P (Algebra.adjoin R ↑(insert a s))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
⊢ f.leadingCoeff ∈ comap C I

Tactic:
simpa [hI] using (I.mem_leadingCoeff f.leadingCoeff).2 ⟨f, hfI, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Goal state before:
pp: ι : Sort u_1
R : Type u_2
inst✝ : NonAssocSemiring R
S : Subsemiring R
a✝ b✝ : Rᵐᵒᵖ
hx : a✝ ∈ S.op.carrier
hy : b✝ ∈ S.op.carrier
⊢ a✝ + b✝ ∈ S.op.carrier

Tactic:
by simp_all [add_mem]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Goal state before:
pp: ι : Sort u_1
R : Type u_2
inst✝ : NonAssocSemiring R
S : Subsemiring Rᵐᵒᵖ
a✝ b✝ : R
hx : a✝ ∈ S.unop.carrier
hy : b✝ ∈ S.unop.carrier
⊢ a✝ + b✝ ∈ S.unop.carrier

Tactic:
by simp_all [add_mem]

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

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

Tactic:
as_sum p

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ ∑ v ∈ p.support, (monomial v) (coeff v p) ∈ I
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b m : ℤ
h : a ≡ b [ZMOD m * n]
⊢ a ≡ b [ZMOD n]

Tactic:
rw [modEq_iff_dvd] at *; exact (dvd_mul_left n m).trans h

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

Goal state before:
pp: case refine_2
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ (m / ↑(m.gcd c)).gcd (c / ↑d) = 1

Tactic:
gcd_div (gcd_dvd_left ..) (gcd_dvd_right ..),

Goal state after:
case refine_2
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m.gcd c / (↑(m.gcd c)).natAbs = 1
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h : ↑q = 0
⊢ False

Tactic:
by
  rw [cast_eq_zero_iff R p q] at h
  rcases hq.eq_one_or_self_of_dvd _ h with rfl | h
  · exact false_of_nontrivial_of_char_one (R := R)
  · exact hneq h

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ Injective ⇑(Quotient.lift I f H) ↔ ker f = I

Tactic:
rw [injective_iff_ker_eq_bot, ker_quotient_lift, map_eq_bot_iff_le_ker, mk_ker]

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f ≤ I ↔ ker f = I
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p % 2 = 1 ↔ p ≠ 2

Tactic:
refine ⟨fun h hf => ?_, hp.eq_two_or_odd.resolve_left⟩

Goal state after:
p : ℕ
hp : Prime p
h : p % 2 = 1
hf : p = 2
⊢ False
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
hf : Surjective ⇑f
x✝ : S ⧸ I
x : S
hx : (Quotient.mk I) x = x✝
y : R
hy : f y = x
⊢ (quotientMap I f H) ((Quotient.mk J) y) = x✝

Tactic:
by simp [hx, hy]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
ih : map (map f) ts.permutations' = (map f ts).permutations'
⊢ map (map f) (t :: ts).permutations' = (map f (t :: ts)).permutations'

Tactic:
| cons t ts ih =>

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
⊢ p a ha

Tactic:
refine Algebra.adjoin_induction (fun x hx ↦ ?_) algebraMap add mul ha
  push _ ∈ _ at hx
  obtain (hx | hx) := hx
  · exact mem x hx
  · simpa using star _ (Algebra.subset_adjoin (by simpa using Or.inl hx)) (mem _ hx)

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ 0 < minimalPeriod f x

Tactic:
classical
  simp only [minimalPeriod, dif_pos hx, (Nat.find_spec hx).1.lt]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ == l₂) = decide (l₁ = l₂)

Tactic:
rw [Bool.eq_iff_iff, @beq_iff_eq _ (_), decide_eq_true_iff]

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

Goal state before:
pp: case h.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : l.Nodup
h✝ : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
hk : 0 < (y :: l).dropLast.length
hk' : (y :: l).dropLast[0] = (y :: l).getLast ⋯
⊢ False

pp: case h.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : l.Nodup
h✝ : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : (y :: l).dropLast[k + 1] = (y :: l).getLast ⋯
⊢ False

Tactic:
· grind

Goal state after:
case h.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : l.Nodup
h✝ : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : (y :: l).dropLast[k + 1] = (y :: l).getLast ⋯
⊢ False
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Tactic:
rw [prev, dif_neg hx]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
hm : x = hd'
⊢ hd ∈ hd :: hd' :: tl

Tactic:
exact mem_cons_self

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : a = x
⊢ some y = (y :: tail)[idxOf a (x :: y :: tail)]?

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ some ((y :: tail).nextOr a d) = (y :: tail)[idxOf a (x :: y :: tail)]?

Tactic:
· grind

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ some ((y :: tail).nextOr a d) = (y :: tail)[idxOf a (x :: y :: tail)]?
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
h' : (x :: y :: tail).getLast hl = x
⊢ y = d

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
h' : ¬(x :: y :: tail).getLast hl = x
⊢ (y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d

Tactic:
· grind

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
h' : ¬(x :: y :: tail).getLast hl = x
⊢ (y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : x = y
⊢ (↑(x :: y :: l)).Nontrivial ↔ (↑(x :: l)).Nontrivial

Tactic:
by simp [h, Nontrivial]

Goal state after: