mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case pos
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
h : ∃ y, ↑y - x ∈ ball K c
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c

Tactic:
obtain ⟨y, hy⟩ := h

Goal state after:
case pos
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
h : ∃ y, ↑y - k • x ∈ ball K c
⊢ ∃ y, ↑y - x ∈ ball K c

Tactic:
obtain ⟨y, hy⟩ := h

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - k • x ∈ ball K c
⊢ ∃ y, ↑y - x ∈ ball K c
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case mk.mk.mk
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
h : mk x ≤ mk y
z : FiniteElement K
⊢ mk x + mk z ≤ mk y + mk z

Tactic:
obtain h | h := mk_le_mk.1 h

Goal state after:
case mk.mk.mk.inl
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
h✝ : mk x ≤ mk y
z : FiniteElement K
h : x ≤ y
⊢ mk x + mk z ≤ mk y + mk z

case mk.mk.mk.inr
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
h✝ : mk x ≤ mk y
z : FiniteElement K
h : mk x = mk y
⊢ mk x + mk z ≤ mk y + mk z
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h : mk x ≠ 0
⊢ stdPart x = 0

Tactic:
obtain h | h := h.lt_or_gt

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : mk x ≠ 0
h : mk x < 0
⊢ stdPart x = 0

case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : mk x ≠ 0
h : 0 < mk x
⊢ stdPart x = 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x⁻¹ hx') =
    ((Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x ⋯))⁻¹

Tactic:
· apply eq_inv_of_mul_eq_one_left
      suffices FiniteElement.mk x⁻¹ hx' * .mk x hx.ge = 1 by
        rw [← map_mul, this, map_one]
      ext
      apply inv_mul_cancel₀
      aesop

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ∃ y, ↑y - x ∈ ball K c
⊢ ∃ y, ((↑f).supSpanSingleton x (f.eval x) hx).toFun y = toLex ((truncLTLinearMap K c) (ofLex (f.eval x)))

Tactic:
obtain ⟨y, hy⟩ := h

Goal state after:
case pos
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
⊢ ∃ y, ((↑f).supSpanSingleton x (f.eval x) hx).toFun y = toLex ((truncLTLinearMap K c) (ofLex (f.eval x)))
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case neg.inr
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c d : FiniteArchimedeanClass M
hdc : c ≤ d
h : ∃ y, ↑y - x ∈ ball K d
⊢ ∃ y, ↑y - x ∈ ball K c

Tactic:
obtain ⟨y, hy⟩ := h

Goal state after:
case neg.inr
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c d : FiniteArchimedeanClass M
hdc : c ≤ d
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K d
⊢ ∃ y, ↑y - x ∈ ball K c
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
⊢ seed.baseEmbedding ≤ sSupFun hc

Tactic:
obtain ⟨f, hf⟩ := hnonempty

Goal state after:
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
c : Set (Partial seed)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
f : Partial seed
hf : f ∈ c
⊢ seed.baseEmbedding ≤ sSupFun hc
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
m : ℕ
hm : n ≤ m
⊢ p.coeff m = q.coeff m

Tactic:
by
  nontriviality R
  rw [isMonicOfDegree_iff] at hp hq
  rcases eq_or_lt_of_le hm with rfl | hm
  · rw [hp.2, hq.2]
  · replace hp : p.natDegree < m := hp.1.trans_lt hm
    replace hq : q.natDegree < m := hq.1.trans_lt hm
    rw [coeff_eq_zero_of_natDegree_lt hp, coeff_eq_zero_of_natDegree_lt hq]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.natDegree - p.natTrailingDegree + p.natTrailingDegree = p.natDegree

pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0

Tactic:
tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.natDegree = p.natDegree

R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ eval r
      ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) • (X - C r) ^ (q - (q - (x + 1))) *
        (⇑derivative)^[x + 1] p') =
    0

Tactic:
h (x + 1) le_add_self (Nat.add_one_le_iff.mpr (mem_range.mp hx)),

Goal state after:
case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ eval r
      ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) • ((X - C r) ^ 1 * (X - C r) ^ (q - (q - (x + 1)) - 1)) *
        (⇑derivative)^[x + 1] p') =
    0
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ((range (p.natDegree + 1)).sum c).natDegree ≤ p.natDegree - q

pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ∀ (r : A),
    (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) (sumIDeriv p) = q ! • (aeval r) ((range (p.natDegree + 1)).sum c)

Tactic:
· refine (natDegree_sum_le _ _).trans ?_
    rw [fold_max_le]
    exact ⟨Nat.zero_le _, fun i _ => c_le i⟩

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ∀ (r : A),
    (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) (sumIDeriv p) = q ! • (aeval r) ((range (p.natDegree + 1)).sum c)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case h.right
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
⊢ (X - C η).leadingCoeff * P.eraseLead.leadingCoeff ::
      (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList) =
    P.nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
leadingCoeff_X_sub_C,

Goal state after:
case h.right
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
⊢ 1 * P.eraseLead.leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList) =
    P.nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
Module: Mathlib.Algebra.PresentedMonoid.Basic

Goal state before:
pp: α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ closure (range (of rels)) = ⊤

Tactic:
rw [Submonoid.eq_top_iff']

Goal state after:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ ∀ (x : PresentedMonoid rels), x ∈ closure (range (of rels))
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ (∑ j, r i j * g i ^ ↑j).degree < (g i ^ n i).degree

Tactic:
refine (degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 fun j _ => ?_)

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ ⊥ < (g i ^ n i).degree

case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
x✝ : j ∈ Finset.univ
⊢ (r i j * g i ^ ↑j).degree < (g i ^ n i).degree
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz : (z * (algebraMap R (QuadraticAlgebra R a b)) r).re = 0 ∧ (z * (algebraMap R (QuadraticAlgebra R a b)) r).im = im 0
⊢ z = 0

Tactic:
im_zero

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz : (z * (algebraMap R (QuadraticAlgebra R a b)) r).re = 0 ∧ (z * (algebraMap R (QuadraticAlgebra R a b)) r).im = 0
⊢ z = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z = 0
⊢ norm z = 0

Tactic:
simp [hz]

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : inst₁.toAddCommGroup = inst₂.toAddCommGroup
toIntCast_eq✝ : inst₁.toIntCast = inst₂.toIntCast
h_addMonoidWithOne :
  { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ } =
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
⊢ inst₁ = inst₂

Tactic:
injection h_addMonoidWithOne

Goal state after:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : inst₁.toAddCommGroup = inst₂.toAddCommGroup
toIntCast_eq✝ : inst₁.toIntCast = inst₂.toIntCast
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
toNatCast_eq✝ : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toOne_eq✝ : inst₁.toOne = inst₂.toOne
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
a b : α
⊢ (↑(↑f + ↑g)).toFun (a * b) = a * (↑(↑f + ↑g)).toFun b

Tactic:
by
        simp [map_mul_left, mul_add]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ ((erase a) f).support = s

Tactic:
rw [support_erase, hf, Finset.erase_cons]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p ((erase a) f)

Tactic:
apply ih
      rw [support_erase, hf, Finset.erase_cons]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
| X ^ (n + 1) * p

Tactic:
rw [pow_succ]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
| X ^ n * X * p
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := e.star
this : SMul 𝕜 R := Equiv.smul 𝕜 e
⊢ StarModule 𝕜 R

Tactic:
apply e.injective.starModule _ 𝕜 <;> (intros; exact e.apply_symm_apply _)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
n : ℕ
⊢ ↑n = single 1 ↑n

Tactic:
induction n

Goal state after:
case zero
k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
⊢ ↑0 = single 1 ↑0

case succ
k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
n✝ : ℕ
a✝ : ↑n✝ = single 1 ↑n✝
⊢ ↑(n✝ + 1) = single 1 ↑(n✝ + 1)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
x : G
x✝¹ : x ∈ b.coeff.support
y : G
x✝ : y ∈ a.coeff.support
⊢ single (x * y) (a.coeff y * b.coeff x) = single (x * y) (b.coeff x * a.coeff y)

Tactic:
mul_comm (a.coeff y) _

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
x : G
x✝¹ : x ∈ b.coeff.support
y : G
x✝ : y ∈ a.coeff.support
⊢ single (x * y) (b.coeff x * a.coeff y) = single (x * y) (b.coeff x * a.coeff y)
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
G : Type u_4
inst✝³ : AddCommMonoid G
inst✝² : Module R G
inst✝¹ : StarAddMonoid G
inst✝ : StarModule R G
f : E →ₗ[R] F
g : G →ₗ[R] E
⊢ star (toConv (f ∘ₗ g)) = toConv ((star (toConv f)).ofConv ∘ₗ (star (toConv g)).ofConv)

Tactic:
simpa using intrinsicStar_comp _ _

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
⊢ H.hom.c ≫ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c = 𝟙 Y.presheaf

Tactic:
ext U

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ (H.hom.c ≫ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) = (𝟙 Y.presheaf).app (op U)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
⊢ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c ≫ H.hom.c =
    𝟙 ((Presheaf.pushforward C H.hom.base).obj X.presheaf)

Tactic:
ext U

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c ≫ H.hom.c).app (op U) =
    (𝟙 ((Presheaf.pushforward C H.hom.base).obj X.presheaf)).app (op U)