mathlib-initiative/mathlib-tactics huggingface dataset:
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).coeff p.natDegree = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0

Tactic:
← natDegree_eq_natDegree hpq,

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).coeff (map f p).natDegree = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0
Module: Mathlib.Algebra.Order.Pi

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
⊢ mulSingle i a ≤ mulSingle i b ↔ a ≤ b

Tactic:
simp [mulSingle]

Goal state after:
Module: Mathlib.Algebra.Order.Pi

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ 1 ≤ mulSingle i a ↔ 1 ≤ a

Tactic:
simp [mulSingle]

Goal state after:
Module: Mathlib.Algebra.Order.Pi

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ 1 < mulSingle i a ↔ 1 < a

Tactic:
simp [mulSingle]

Goal state after:
Module: Mathlib.Algebra.Order.Pi

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ mulSingle i a ≤ 1 ↔ a ≤ 1

Tactic:
simp [mulSingle]

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

Goal state before:
pp: case mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
hai : a ≠ i
h : x i + y i = 0
⊢ 0 = x i ∧ 0 = y i

Tactic:
add_eq_zero

Goal state after:
case mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
hai : a ≠ i
h : x i = 0 ∧ y i = 0
⊢ 0 = x i ∧ 0 = y i
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
p q r : R[X]
inst✝ : Nontrivial A
x : R
⊢ ¬C ((algebraMap R A) x) = X

Tactic:
ext_iff,

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
p q r : R[X]
inst✝ : Nontrivial A
x : R
⊢ ¬∀ (n : ℕ), (C ((algebraMap R A) x)).coeff n = X.coeff n
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:
← @neLocus_add_right α N _ _ _ _ _ (-g),

Goal state after:
α : 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 + -g).neLocus (g + -g) = (f - g).support
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ a ∈ (coeffEquiv.toFun p).support ∪ (coeffEquiv.toFun q).support, (f 0 * a.prod fun n e ↦ g n ^ e) = 0

Tactic:
simp [f.map_zero]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
⊢ (f 0 * s.prod fun n e ↦ g n ^ e) = 0

Tactic:
simp [f.map_zero]

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₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * (monomial (Finsupp.single n 1 + s)) a)

Tactic:
monomial_single_add,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * (X n ^ 1 * (monomial s) a))
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 : R →+* S₁
⊢ map f = eval₂Hom (C.comp f) X

Tactic:
by ext a x <;> simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
this : coeff d q = 0
⊢ coeff d p + coeff d q ≠ 0

Tactic:
rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]

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 : R →+* S₁
p : MvPolynomial σ R
⊢ ((map f) p).support ⊆ p.support

Tactic:
by
  simp only [Finset.subset_iff, mem_support_iff]
  intro x hx
  contrapose hx
  rw [coeff_map, hx, map_zero]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (Finsupp.mapDomain f d) ((rename f) φ) = coeff d φ

Tactic:
induction φ using MvPolynomial.induction_on' with

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.degrees.toFinset = p.degrees.toFinset

Tactic:
convert! rfl

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
n : σ
p : MvPolynomial σ R
⊢ Multiset.count n p.degrees = Multiset.count n p.degrees

Tactic:
convert! rfl

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : CommSemiring S₂
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S₂
f : S₁ →ₐ[R] S₂
x✝ : MvPolynomial σ S₂
⊢ x✝ ∈ range ⇑(mapAlgHom f) ↔ x✝ ∈ ↑(coeffsIn σ (Subalgebra.toSubmodule f.range))

Tactic:
erw [mem_range_map_iff_coeffs_subset, mem_coeffsIn_iff_coeffs_subset]

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : CommSemiring S₂
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S₂
f : S₁ →ₐ[R] S₂
x✝ : MvPolynomial σ S₂
⊢ ↑x✝.coeffs ⊆ range ⇑↑f ↔ ↑x✝.coeffs ⊆ ↑(Subalgebra.toSubmodule f.range)
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ cons x s = cons y 0 ↔ s = 0 ∧ x = y

Tactic:
cons_injective2.eq_iff,

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ x = y ∧ s = 0 ↔ s = 0 ∧ x = y
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ cons x s = cons 0 (single i y) ↔ s = single i y ∧ x = 0

Tactic:
cons_injective2.eq_iff,

Goal state after:
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ x = 0 ∧ s = single i y ↔ s = single i y ∧ x = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ ∑ s, d s ≤ d.sum fun x e ↦ e

Tactic:
by
      rw [Finsupp.sum_fintype]
      intros
      rfl

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
h : f.totalDegree < n * Fintype.card σ
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ ∃ i, d i < n

Tactic:
by
  contrapose! h
  calc
    n * Fintype.card σ = ∑ _s : σ, n := by
      rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
    _ ≤ ∑ s, d s := Finset.sum_le_sum fun s _ => h s
    _ ≤ d.sum fun _ e => e := by
      rw [Finsupp.sum_fintype]
      intros
      rfl
    _ ≤ f.totalDegree := le_totalDegree hd

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

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ ∀ y ∈ (p * X ^ n).support, p.natTrailingDegree + n ≤ y

Tactic:
intro y

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
⊢ y ∈ (p * X ^ n).support → p.natTrailingDegree + n ≤ y
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = 0

Tactic:
by_cases he₂ : ((X - C x) * P).eraseLead = 0

Goal state after:
case pos
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ((X - C x) * P).eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = 0

case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = 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
⊢ f p.leadingCoeff ≠ 0

Tactic:
have h4 : map f p ≠ 0 := by
    rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]

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
⊢ f p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = ↑(p.comp q).natDegree

Tactic:
apply degree_eq_natDegree

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ p.comp q ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
Monic.def,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).Monic

Tactic:
Monic.def,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : p.natDegree + q.natDegree = 0
⊢ p = 1

Tactic:
add_eq_zero

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p = 1
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

Tactic:
rw [Polynomial.natDegree, degree_finSuccEquiv c, Nat.cast_withBot, WithBot.unbotD_coe]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i ≠ 0

Tactic:
· rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]
        exact n.succ_ne_zero

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) s, f.Monic

Tactic:
exact Multiset.forall_mem_map_iff.2 fun a _ => monic_X_sub_C a

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
⊢ (∏ a ∈ s, (X - C (f a))).natDegree = #s

Tactic:
Finset.prod,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
⊢ (Multiset.map (fun a ↦ X - C (f a)) s.val).prod.natDegree = #s
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ (h.unit⁻¹ • p).Monic

Tactic:
Monic.def,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ (h.unit⁻¹ • p).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ p * q = 0 ↔ q = 0

Tactic:
constructor
  · intro hp
    rw [← smul_eq_zero_iff_eq h.unit⁻¹] at hp
    have : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q := by
      ext
      simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
      refine sum_congr rfl fun x _ => ?_
      rw [← mul_assoc]
    rwa [this, Monic.mul_right_eq_zero_iff] at hp
    exact monic_of_isUnit_leadingCoeff_inv_smul _
  · rintro rfl
    simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ (p.sum fun e a ↦ a * x ^ e) = ∑ i, (degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i

Tactic:
exact (sum_fin _ (by simp_rw [zero_mul, forall_const]) (mem_degreeLT.mp hp)).symm

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, ?_⟩

Goal state after:
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
⊢ Polynomial.leadingCoeff 0 = p.coeff n
Module: Mathlib.Algebra.Algebra.Subalgebra.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := ⋯
l' : ι → ↥S' := ⋯
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ⋯
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
⊢ ∀ (r : ↑((fun x ↦ x ^ N) '' s' '' ↑ι')), ↑r • x ∈ toSubmodule (ofId (↥S') S).range

Tactic:
rintro ⟨_, _, ⟨i, hi, rfl⟩, rfl⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ι'.sup n
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
i : ι
hi : i ∈ ↑ι'
⊢ ↑⟨(fun x ↦ x ^ N) (s' i), ⋯⟩ • x ∈ toSubmodule (ofId (↥S') S).range
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 (Set.range ⇑(algebraMap R A) ∪ s)).op =
    Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s)

Tactic:
Subsemiring.op_closure,

Goal state after:
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) ∪ s)) =
    Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : MvPolynomial (↑S) R
⊢ ∃ a,
    (MvPolynomial.aeval fun s ↦ of' R M ↑s) a =
      (MvPolynomial.aeval fun s ↦ of' R M ↑s) P + (MvPolynomial.aeval fun s ↦ of' R M ↑s) Q

Tactic:
exact ⟨P + Q, map_add _ _ _⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : FreeAlgebra R ↑S
⊢ ∃ a,
    ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a =
      ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P + ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) Q

Tactic:
exact ⟨P + Q, map_add _ _ _⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : MvPolynomial (↑S) R
⊢ ∃ a,
    (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a =
      (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P + (MvPolynomial.aeval fun s ↦ (of R M) ↑s) Q

Tactic:
exact ⟨P + Q, map_add _ _ _⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : FreeAlgebra R ↑S
⊢ ∃ a,
    ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a =
      ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P + ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) Q

Tactic:
exact ⟨P + Q, map_add _ _ _⟩

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
⊢ Disjoint ((aeval f) p).ker ((aeval f) q).ker

Tactic:
rw [disjoint_iff_inf_le]
  intro v hv
  rcases hpq with ⟨p', q', hpq'⟩
  simpa [LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).1,
    LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).2] using
    congr_arg (fun p : R[X] => aeval f p v) hpq'.symm

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
⊢ ∀ m ∈ toSubmodule S, ∀ n ∈ toSubmodule T, m * n ∈ toSubmodule (S ⊔ T)

Tactic:
intro y

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
⊢ y ∈ toSubmodule S → ∀ n ∈ toSubmodule T, y * n ∈ toSubmodule (S ⊔ T)
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S ≤ toSubmodule S * toSubmodule S

Tactic:
intro x hx1
    rw [← mul_one x]
    exact Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)

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 ι
g : (i : ι) → R ⧸ I i
⊢ ∃ a, (quotientInfToPiQuotient I) a = g

Tactic:
choose f hf using fun i ↦ mk_surjective (g i)

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
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
⊢ ∃ a, (quotientInfToPiQuotient I) a = g
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (t : α) (ts is : List α),
    map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is)) →
      map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f []) →
        map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)

Tactic:
introv IH1 IH2

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))
IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f [])
⊢ map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case succ.refine_2.e_b
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝¹ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ id).snd ++ [x✝ ++ [t]] = permutations'Aux t x✝

Tactic:
rw [permutations'Aux_eq_permutationsAux2, permutationsAux2_append]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s

Tactic:
← Nat.card_prod

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card ((α ⧸ s) × ↥s)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (map (cons y) (permutations'Aux x s)).Nodup

Tactic:
nodup_map_iff

Goal state after:
case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (permutations'Aux x s).Nodup

case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ Injective (cons y)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ (a :: l).rotate 1 = l ++ [a]

Tactic:
rw [rotate_cons_succ, rotate_zero]

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
by
  refine (primeFactorsList_unique ?_ ?_).symm
  · rw [List.prod_append, prod_primeFactorsList ha, prod_primeFactorsList hb]
  · intro p hp
    rw [List.mem_append] at hp
    rcases hp with hp' | hp' <;> exact prime_of_mem_primeFactorsList hp'

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ a = 0

Tactic:
rw [Fin.ext_iff]

Goal state after:
n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ ↑a = ↑0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
⊢ Nat.card ((G × G') ⧸ H.prod K) = Nat.card (G ⧸ H) * Nat.card (G' ⧸ K)

Tactic:
← Nat.card_prod

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
⊢ Nat.card ((G × G') ⧸ H.prod K) = Nat.card ((G ⧸ H) × G' ⧸ K)