mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
⊢ image
      (fun x ↦
        match x with
        | ((x, y), z, w) => (x.sumElim z, y.sumElim w))
      (antidiagonal x ×ˢ antidiagonal y) =
    antidiagonal (x.sumElim y)

Tactic:
ext ⟨u, v⟩
  simp only [mem_antidiagonal, mem_image, mem_product, Prod.mk.injEq, Prod.exists]
  refine ⟨fun ⟨a, b, a', b', h1, h2, h3⟩ ↦ ?_, fun h ↦
    ⟨u.comapDomain Sum.inl Sum.inl_injective.injOn, v.comapDomain Sum.inl Sum.inl_injective.injOn,
    u.comapDomain Sum.inr Sum.inr_injective.injOn, v.comapDomain Sum.inr Sum.inr_injective.injOn,
    ⟨?_, ?_⟩, comapDomain_sumElim_comapDomain .., comapDomain_sumElim_comapDomain ..⟩⟩
  · rw [← h2, ← h3, ← sumElim_add, h1.left, h1.right]
  · rw [← comapDomain_add_of_injective Sum.inl_injective, h, comapDomain_inl_sumElim]
  · rw [← comapDomain_add_of_injective Sum.inr_injective, h, comapDomain_inr_sumElim]

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

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
j : ι
⊢ (single j (a - b)) j = (single j a - single j b) j

pp: case inr
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
⊢ (single i (a - b)) j = (single i a - single i b) j

Tactic:
· rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]

Goal state after:
case inr
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
⊢ (single i (a - b)) j = (single i a - single i b) j
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
⊢ x ≤ y ↔ x default ≤ y default

Tactic:
le_iff_lt_or_eq,

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

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (β i)
x y : Colex ((i : ι) → β i)
⊢ x ≤ y ↔ x default ≤ y default

Tactic:
le_iff_lt_or_eq,

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = eval (ψ a) (map (ψ.comp (algebraMap R S)) p)

Tactic:
← map_map,

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = eval (ψ a) (map ψ (map (algebraMap R S) p))
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) ↔ x i ≤ a

Tactic:
le_iff_lt_or_eq,

Goal state after:
ι : 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
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 (update x i a) ≤ toLex x ↔ a ≤ x i

Tactic:
le_iff_lt_or_eq,

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

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ ∃ a, a₁✝ < a ∧ a < a₂

Tactic:
refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
⊢ a₁✝ j = Function.update a₂ i a j

case refine_2
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ (fun {i} x1 x2 ↦ x1 < x2) (a₁✝ i) (Function.update a₂ i a i)

case refine_3
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
⊢ Function.update a₂ i a j = a₂ j

case refine_4
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ (fun {i} x1 x2 ↦ x1 < x2) (Function.update a₂ i a i) (a₂ i)
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
⊢ p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q

Tactic:
let _ := invertibleOne (α := R)
  simpa using! dvd_comp_C_mul_X_add_C_iff p q 1 (-a)

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
inst✝ : DecidableEq ι
j : ι
a b : α j
⊢ (single j (a - b)) j = (single j a - single j b) j

pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
h : j ≠ i
⊢ (single i (a - b)) j = (single i a - single i b) j

Tactic:
· rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
h : j ≠ i
⊢ (single i (a - b)) j = (single i a - single i b) j
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case monomial
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
n : ℕ
t : R
hmq : (aeval a) (C t * X ^ n) • m ∈ q
⊢ (a * (aeval a) (C t * X ^ n)) • m ∈ q

Tactic:
mul_smul

Goal state after:
case monomial
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
n : ℕ
t : R
hmq : (aeval a) (C t * X ^ n) • m ∈ q
⊢ a • (aeval a) (C t * X ^ n) • m ∈ q
Module: Mathlib.Data.Finsupp.Fin

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

Tactic:
have := DFunLike.congr_fun h 0

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
x₀ y₀ : M
x y : Fin n →₀ M
h : cons x₀ x = cons y₀ y
this : (cons x₀ x) 0 = (cons y₀ y) 0
⊢ x₀ = y₀ ∧ x = y
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
H : ↑n ≤ p.trailingDegree
⊢ n ≤ p.natTrailingDegree

Tactic:
rwa [trailingDegree_eq_natTrailingDegree hp, Nat.cast_le] at H

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

Goal state before:
pp: R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).natDegree ≤ m * n

Tactic:
refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))

Goal state after:
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ m * p.natDegree ≤ m * n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
rcases eq_or_ne o (m * n) with rfl | h
  · simpa only [ite_true] using coeff_pow_of_natDegree_le pn
  · simpa only [h, ite_false] using coeff_eq_zero_of_natDegree_lt <|
      lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm)

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)

Tactic:
rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
N : ℕ
| C r * X ^ N
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.inl
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * P).coeff n + ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff n = ((X - C x) * P).coeff n

Tactic:
add_eq_left

Goal state after:
case neg.inl
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff n = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
⊢ coeff n.some (((optionEquivLeft R S₁) ((monomial j) r)).coeff (n none)) = coeff n ((monomial j) r)

Tactic:
optionEquivLeft_monomial

Goal state after:
case monomial
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
⊢ coeff n.some (((Polynomial.monomial (j none)) ((monomial j.some) r)).coeff (n none)) = coeff n ((monomial j) r)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ p = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i

Tactic:
conv_lhs => rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
  suffices C (p.coeff p.natDegree) = 1 by rw [this, one_mul]
  exact congr_arg C hp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ p.degree ≤ 0 ↔ p.natDegree = 0

Tactic:
natDegree_eq_zero_iff_degree_le_zero

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ p.degree ≤ 0 ↔ p.degree ≤ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hC
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ ∀ (r : R),
    ((finSuccEquiv R n).toRingEquiv.toRingHom.comp
          (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
        (C r) =
      ((Polynomial.mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (C r)

pp: case hX
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ ∀ (i : Option σ),
    ((finSuccEquiv R n).toRingEquiv.toRingHom.comp
          (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
        (X i) =
      ((Polynomial.mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X i)

Tactic:
· simp [Polynomial.algebraMap_apply, algebraMap_eq, finSuccEquiv_apply, optionEquivLeft_apply]

Goal state after:
case hX
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ ∀ (i : Option σ),
    ((finSuccEquiv R n).toRingEquiv.toRingHom.comp
          (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
        (X i) =
      ((Polynomial.mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X i)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → (k • p).coeff m_1 = 0
⊢ p.coeff m = 0

Tactic:
refine h ?_

Goal state after:
case refine_2
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → (k • p).coeff m_1 = 0
⊢ (fun x ↦ k • x) (p.coeff m) = (fun x ↦ k • x) 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i

Tactic:
induction n generalizing f with

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 = ∅
⊢ ∃ n, Submodule.span R ∅ ≤ degreeLE R ↑n

Tactic:
Submodule.span_empty

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s = ∅
⊢ ∃ n, ⊥ ≤ degreeLE R ↑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' := 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 ∈ ↑ι'
⊢ (s' i ^ (N - n i) * s' i ^ n i) • x ∈ toSubmodule (ofId (↥S') S).range

Tactic:
mul_smul

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 ∈ ↑ι'
⊢ s' i ^ (N - n i) • s' i ^ n i • x ∈ toSubmodule (ofId (↥S') S).range
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : R[M]
ih : ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = f
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = r • f

Tactic:
rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : R[M]
ih : ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = f
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = r • f

Tactic:
rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : R[M]
ih : ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = f
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = r • f

Tactic:
rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : R[M]
ih : ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = f
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = r • f

Tactic:
rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

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

Goal state before:
pp: case intro.e_f
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
x✝ : σ →₀ ℕ
⊢ ϕ ((monomial x✝) (coeff x✝ p)) = (ϕ.comp C) (coeff x✝ p) * ∏ i, ϕ (X i) ^ x✝ i

Tactic:
simp only [monomial_eq, ϕ.map_pow, map_prod ϕ, ϕ.comp_apply, ϕ.map_mul, Finsupp.prod_pow]

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

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

Tactic:
exact h.mul_left'

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

Goal state before:
pp: case left
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs < b

Tactic:
natAbs_of_nonneg hz1

Goal state after:
case left
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z < b
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case right
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs ≡ a [ZMOD b]

Tactic:
natAbs_of_nonneg hz1

Goal state after:
case right
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z ≡ a [ZMOD b]
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : x ∈ ker (Quotient.lift I f H)
y : R
hy : (Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (ker f)

Tactic:
rw [mem_ker, ← hy, Ideal.Quotient.lift_mk, ← mem_ker] at hx

Goal state after:
case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : y ∈ ker f
hy : (Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (ker f)
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ Set.range Nat.cast = {0, 1}

Tactic:
rw [funext natCast_eq_ite, Set.range_ite_const]

Goal state after:
case hp
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ∃ a, Even a

case hn
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ∃ a, ¬Even a
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case h
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
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i j : ι
hj : j ≠ i
⊢ (Quotient.mk (I i)) (f j * e j) = 0

Tactic:
simp [(he j).2 i hj.symm]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
nextOr,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (if x = y then z else (z :: zs).nextOr x d) = (y :: z :: zs).nextOr x d'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (if x = y then z else (z :: zs).nextOr x d) = (y :: z :: zs).nextOr x d'

Tactic:
nextOr,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (if x = y then z else (z :: zs).nextOr x d) = if x = y then z else (z :: zs).nextOr x d'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (y :: z :: l).nextOr x ((y :: z :: l).get ⟨0, ⋯⟩) = z

Tactic:
nextOr,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (if x = y then z else (z :: l).nextOr x ((y :: z :: l).get ⟨0, ⋯⟩)) = z
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case succ.refine_2
α : 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'
⊢ flatMap (fun y ↦ (permutationsAux2 t [] [] y id).snd) ts.permutations' ++
      flatMap (fun x ↦ [x ++ [t]]) ts.permutations' ~
    ([t] ++ ts).permutations'

Tactic:
singleton_append,

Goal state after:
case succ.refine_2
α : 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'
⊢ flatMap (fun y ↦ (permutationsAux2 t [] [] y id).snd) ts.permutations' ++
      flatMap (fun x ↦ [x ++ [t]]) ts.permutations' ~
    (t :: ts).permutations'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
⊢ (y :: l).next x h = y

Tactic:
by
  rw [next, get, ← dropLast_append_getLast (cons_ne_nil y l), hx, nextOr_concat]
  subst hx
  intro H
  obtain ⟨_ | k, hk, hk'⟩ := getElem_of_mem H
  · grind
  suffices k + 1 = l.length by simp [this] at hk
  rcases l with - | ⟨hd, tl⟩
  · simp at hk
  · rw [nodup_iff_injective_get] at hl
    rw [length, Nat.succ_inj]
    exact Fin.val_eq_of_eq <| @hl ⟨k, Nat.lt_of_succ_lt <| by simpa using hk⟩
      ⟨tl.length, by simp⟩ (by grind)

Goal state after: