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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
P Q : R[X]
hPQ : X ^ n * P = X ^ n * Q
i : ℕ
⊢ P.coeff i = Q.coeff i

Tactic:
← coeff_X_pow_mul P n i,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
P Q : R[X]
hPQ : X ^ n * P = X ^ n * Q
i : ℕ
⊢ (X ^ n * P).coeff (i + n) = Q.coeff i
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.leadingCoeff = 0 ↔ p ≠ 0

Tactic:
leadingCoeff_eq_zero

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p = 0 ↔ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: 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
⊢ q.natDegree < p.natDegree

Tactic:
natDegree_add_eq_right_of_natDegree_lt h

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
H : q.natDegree < p.natDegree
h✝ : ¬p.natDegree = q.natDegree
h : p.natDegree < q.natDegree
⊢ q.natDegree < p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
⊢ p ≠ 0

Tactic:
by
  rintro rfl
  simp [Monic] at hp

Goal state after:
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
hp : ¬p = 0
⊢ ¬p.leadingCoeff = 0

Tactic:
leadingCoeff_eq_zero

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
⊢ ¬p = 0
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ¬(p ^ n).leadingCoeff = 0

Tactic:
leadingCoeff_eq_zero

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ¬p ^ n = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ ¬q.leadingCoeff = 0

Tactic:
leadingCoeff_eq_zero

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ ¬q = 0
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ ¬(↑u).leadingCoeff = 0

Tactic:
leadingCoeff_eq_zero

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ ¬↑u = 0
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

Tactic:
leadingCoeff_C_mul_X_pow

Goal state after:
R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ a = a
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

Tactic:
leadingCoeff_C_mul_X_pow

Goal state after:
R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ a = a
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
| succ i hi =>

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Tactic:
have : f.coeff i = 0 := by
        rw [← notMem_support_iff]
        exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
      simp [this, Ne.symm hi, coeff_monomial]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (p.sum fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
refine Eq.trans (Finset.sum_eq_single p.natDegree ?h₀ ?h₁) ?h₂

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ ∀ b ∈ p.support, b ≠ p.natDegree → (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0

case h₂
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree
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]
hp : (map f p).leadingCoeff = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0

Tactic:
leadingCoeff_eq_zero

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ x + y = single a n → ∃ a_2 b, a_2 + b = n ∧ single a a_2 = x ∧ single a b = y

Tactic:
intro h
    refine ⟨x a, y a, DFunLike.congr_fun h a |>.trans single_eq_same, ?_⟩
    simp_rw [DFunLike.ext_iff, ← forall_and]
    intro i
    replace h := DFunLike.congr_fun h i
    simp_rw [single_apply, Finsupp.add_apply] at h ⊢
    obtain rfl | hai := Decidable.eq_or_ne a i
    · exact ⟨if_pos rfl, if_pos rfl⟩
    · simp_rw [if_neg hai, add_eq_zero] at h ⊢
      exact h.imp Eq.symm Eq.symm

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:
simp only [neg_comp, X_comp, neg_neg, comp_X]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι ↪ κ
f1 f2 : ι →₀ α
⊢ embDomain f (f1 - f2) = embDomain f f1 - embDomain f f2

Tactic:
embDomain_eq_mapDomain,

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι ↪ κ
f1 f2 : ι →₀ α
⊢ mapDomain (⇑f) (f1 - f2) = mapDomain (⇑f) f1 - mapDomain (⇑f) f2
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case step.inl
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
h✝ : (P.coeff l • Q).natDegree < Q.natDegree
⊢ P.coeff l • Q = 0

pp: case step.inr
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
⊢ P.coeff l • Q = 0

Tactic:
· apply eq_zero_of_mul_eq_zero_of_smul _ h (P.coeff l • Q)
    rw [smul_eq_C_mul, mul_left_comm, hQ, mul_zero]

Goal state after:
case step.inr
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
⊢ P.coeff l • Q = 0
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
this : P.coeff l * Q.leadingCoeff = 0
⊢ P.coeff l • Q = 0

Tactic:
rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0

Tactic:
have := coeff_monomial m (Finsupp.single i k) (1 : R)
  rwa [@monomial_eq _ _ (1 : R) (Finsupp.single i k) _, C_1, one_mul, Finsupp.prod_single_index]
    at this
  exact pow_zero _

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

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
⊢ IsLeftRegular (X n)

Tactic:
intro P

Goal state after:
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₂
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ ∀ m ∈ M * N, ∀ (i : σ →₀ ℕ), (monomial i) m ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
intro r hr s
    induction hr using Submodule.mul_induction_on' with
    | mem_mul_mem m hm n hn =>
      rw [← add_zero s, ← monomial_mul]
      apply Submodule.mul_mem_mul <;> simpa
    | add x _ y _ hx hy =>
      simpa [map_add] using add_mem hx hy

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

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
⊢ ((map f) p).degrees ≤ p.degrees

Tactic:
by
  classical exact Finset.sup_mono <| support_map_subset ..

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 : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
s : σ →₀ ℕ
hs : coeff s p ≠ 0
⊢ coeff (s + Finsupp.single i k) (p * X i ^ k) ≠ 0

Tactic:
rwa [X_pow_eq_monomial, coeff_mul_monomial, mul_one]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.leadingCoeff = 0
h : p.natDegree = n.succ
⊢ False

Tactic:
leadingCoeff_eq_zero

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p = 0
h : p.natDegree = n.succ
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ (1 * p).natDegree = (C ai * (C a * p)).natDegree

Tactic:
by rw [← C_1, ← au, map_mul, ← mul_assoc]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ p.natDegree = (p * 1).natDegree

Tactic:
← mul_one p

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ (p * 1).natDegree = (p * 1).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ (p * 1).natDegree = (p * C a * C ai).natDegree

Tactic:
by rw [← C_1, ← au, map_mul, ← mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
N : ℕ
| reflect N (C r * 1)

Tactic:
← pow_zero X,

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
N : ℕ
| reflect N (C r * X ^ 0)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
⊢ ¬(map f p).leadingCoeff = 0

Tactic:
leadingCoeff_eq_zero

Goal state after:
case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
⊢ ¬map f p = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p.leadingCoeff = 0
⊢ False

Tactic:
leadingCoeff_eq_zero

Goal state after:
case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.Monic

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons]

Goal state after:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a * (Multiset.map f t).prod).Monic
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ (((finSuccEquiv R n) p).coeff i).support
⊢ m j ≤ p.support.sup fun m ↦ m j.succ

Tactic:
← Finsupp.cons_succ j i m

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ (((finSuccEquiv R n) p).coeff i).support
⊢ (cons i m) j.succ ≤ p.support.sup fun m ↦ m j.succ
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ ¬∃ a ∈ t, a.leadingCoeff = 0

Tactic:
leadingCoeff_eq_zero

Goal state after:
case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ ¬∃ a ∈ t, a = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ ¬∃ a ∈ t, a = 0

Tactic:
rintro ⟨_, h, rfl⟩

Goal state after:
case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h✝ : 0 ∉ t
a✝ : Nontrivial R
h : 0 ∈ t
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ f ∈ degreeLE R n ↔ f.degree ≤ n

Tactic:
simp only [degreeLE, Submodule.mem_iInf, degree_le_iff_coeff_zero, LinearMap.mem_ker]

Goal state after:
R : Type u
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ (∀ (i : ℕ), ↑i > n → (lcoeff R i) f = 0) ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : p = 0
⊢ False

Tactic:
rw [hp_zero, degree_zero] at h

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < ⊥
hp_zero : p = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (∅.prod f).coeff k ∈ I ^ (∅.sum n - k)

Tactic:
rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]

Goal state after:
case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (if k = 0 then 1 else 0) ∈ ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hA : FiniteType R A
hB : FiniteType R B
⊢ (⊤.prod ⊤).FG

Tactic:
exact hA.1.prod hB.1

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ toSubmodule S
z : A
hz : z ∈ toSubmodule T
⊢ y * z ∈ toSubmodule (S ⊔ T)

Tactic:
simp only [mem_toSubmodule]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ toSubmodule S
z : A
hz : z ∈ toSubmodule T
⊢ y * z ∈ S ⊔ 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).ker ⊔ ((aeval f) q).ker
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
⊢ ((aeval f) q) (((aeval f) p) x) = 0

Tactic:
LinearMap.mem_ker.1 hx,

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
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
⊢ ((aeval f) q) 0 = 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
h✝ : Nontrivial R
a✝ : Nontrivial S
this✝¹ : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra
this✝ : SMul ↥A ↥(Algebra.adjoin ↥A ↑B) := this✝¹.toSMul
this : IsScalarTower R ↥A ↥(Algebra.adjoin ↥A ↑B)
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥(restrictScalars R (Algebra.adjoin ↥A ↑B))

Tactic:
Algebra.restrictScalars_adjoin

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
h✝ : Nontrivial R
a✝ : Nontrivial S
this✝¹ : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra
this✝ : SMul ↥A ↥(Algebra.adjoin ↥A ↑B) := this✝¹.toSMul
this : IsScalarTower R ↥A ↥(Algebra.adjoin ↥A ↑B)
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin R (↑A ∪ ↑B))
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ ker (RingHom.pi fun i ↦ Quotient.mk (I i)) = ⨅ i, I i

Tactic:
ker_Pi_Quotient_mk

Goal state after:
R : Type u
inst✝¹ : Ring R
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ ⨅ i, I i = ⨅ i, I i
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Infinite { a // a ≠ 0 }
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }

Tactic:
Nat.card_eq_zero_of_infinite,

Goal state after:
case inr
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Infinite { a // a ≠ 0 }
⊢ 0 - 1 = Nat.card { a // a ≠ 0 }
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Infinite { a // a ≠ 0 }
⊢ 0 - 1 = Nat.card { a // a ≠ 0 }

Tactic:
Nat.card_eq_zero_of_infinite,

Goal state after:
case inr
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Infinite { a // a ≠ 0 }
⊢ 0 - 1 = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hf : Pairwise (IsCoprime on I)
x : (i : ι) → R ⧸ I i
⊢ ∃ r, ∀ (i : ι), (Quotient.mk (I i)) r = x i

Tactic:
obtain ⟨y, rfl⟩ := Ideal.quotientInfToPiQuotient_surj hf x
  obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective y
  exact ⟨r, fun i ↦ rfl⟩

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

Goal state before:
pp: case inl
b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b
⊢ 1 ∣ b

Tactic:
apply one_dvd

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

Goal state before:
pp: n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ ∀ (p : ℕ), Prime p → p ∣ n → ¬p ∣ m

Tactic:
exact fun p hp hn hm ↦
    ((le_of_dvd (by lia) hm).trans_lt <| h.trans_le <| minFac_le_of_dvd hp.two_le hn).false

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

Goal state before:
pp: α : Type u_1
t : α
ts : List α
⊢ permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd

Tactic:
induction ts with | nil => rfl | cons a ts ih => ?_

Goal state after:
case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts : List α
r L : List (List α)
⊢ (foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L).length = (map length L).sum + r.length

Tactic:
simp [foldr_permutationsAux2, length_permutationsAux2, length_flatMap]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (n * m) x

Tactic:
by
  simp only [mul_comm n, hm.mul_const n]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f^[n] x = minimalPeriod f x / (minimalPeriod f x).gcd n

Tactic:
apply Nat.dvd_antisymm
  · apply IsPeriodicPt.minimalPeriod_dvd
    rw [IsPeriodicPt, IsFixedPt, ← iterate_mul, ← Nat.mul_div_assoc _ (gcd_dvd_left _ _),
      mul_comm, Nat.mul_div_assoc _ (gcd_dvd_right _ _), mul_comm, iterate_mul]
    exact (isPeriodicPt_minimalPeriod f x).iterate _
  · apply Coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)
    apply Nat.dvd_of_mul_dvd_mul_right h
    rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _),
      mul_comm]
    apply IsPeriodicPt.minimalPeriod_dvd
    rw [IsPeriodicPt, IsFixedPt, iterate_mul]
    exact isPeriodicPt_minimalPeriod _ _

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 0 ↔ x ∉ periodicPts f

Tactic:
exact minimalPeriod_eq_zero_iff_notMem_periodicPts

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

Goal state before:
pp: case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
m : l ∈ ts.permutationsAux (t :: is)
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
exact Or.inr (Or.inl m)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ (∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)

Tactic:
refine ⟨fun H n => ?_, fun H n _ => H n⟩

Goal state after:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n] x) (f^[n + 1] x)