mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem'✝ : f' ∈ c✝
hf' : ↑f' = f
x' : ↥f.domain
hx' : ↑f x' = toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩)))
hmem' : ↑x' ∈ (sSupFun hc).domain
⊢ ∃ y, ↑(sSupFun hc) y = toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x)))

Tactic:
refine ⟨⟨x'.val, hmem'⟩, ?_⟩

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)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem'✝ : f' ∈ c✝
hf' : ↑f' = f
x' : ↥f.domain
hx' : ↑f x' = toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩)))
hmem' : ↑x' ∈ (sSupFun hc).domain
⊢ ↑(sSupFun hc) ⟨↑x', hmem'⟩ = toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x)))
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
r : R
⊢ 0 < 1

Tactic:
exact zero_lt_one

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
⊢ 0 < 1

Tactic:
exact zero_lt_one

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
a b : R
h : f = X ^ 2 + C a * X + C b
⊢ ∃ a b, f = X ^ 2 + C (-a) * X + C b

Tactic:
exact ⟨-a, b, (neg_neg a).symm ▸ h⟩

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

Goal state before:
pp: case isUnit_or_isUnit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
⊢ f = g * h → IsUnit g ∨ IsUnit h

Tactic:
fgh

Goal state after:
case isUnit_or_isUnit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
⊢ IsUnit g ∨ IsUnit h
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ g ∣ f

Tactic:
fgh

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ g ∣ g * h
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ h ∣ f

Tactic:
fgh

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ h ∣ g * h
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ IsChain R (a :: l)

Tactic:
← h

Goal state after:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ IsChain R (destutter' R a l)
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ IsChain R (a :: l)

Tactic:
rw [← h]
    exact l.isChain_destutter' R a

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
⊢ (destutter' R c l).length + 1 ≤ (destutter' R c l).length + 1

Tactic:
le_refl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬X + C (q.coeff 0) ∣ p

Tactic:
← sub_neg_eq_add,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬X - -C (q.coeff 0) ∣ p
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
k i : ℕ
hi : i ∈ ((⇑derivative)^[k] p).support
⊢ (C ((i + k).choose k • p.coeff (i + k)) * X ^ i).natDegree ≤ p.natDegree - k

Tactic:
exact (natDegree_C_mul_le _ _).trans <| (natDegree_X_pow_le _).trans <|
    (le_natDegree_of_mem_supp _ hi).trans <| natDegree_iterate_derivative _ _

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (List.map (⇑SignType.sign) (List.map (fun x ↦ -x) P.coeffList)))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1

Tactic:
simp only [List.map_map, List.filter_map]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign ∘ fun x ↦ -x)
            (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign ∘ fun x ↦ -x) P.coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign) (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A) {p' : A[X]},
        map (algebraMap R A) p = (X - C r) ^ (q - 1) * p' →
          (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) gp

Tactic:
have hc (k) (hk : q ≤ k) : ∀ (r : A), aeval r (derivative^[k] p) = q ! • aeval r (c k) := by
    simp_rw [c, dif_pos hk]
    exact (aeval_iterate_derivative_of_ge A p q hk).choose_spec.2

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A) {p' : A[X]},
        map (algebraMap R A) p = (X - C r) ^ (q - 1) * p' →
          (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) gp
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case h.left
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)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
have : P.natDegree + 2 = ((X - C η) * P).coeffList.length := by simp [X_sub_C_ne_zero, h₃, h₇]

Goal state after:
case h.left
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)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this✝ : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
this : P.natDegree + 2 = ((X - C η) * P).coeffList.length
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
h : IsRelPrime p p.mirror
⊢ Irreducible p

Tactic:
by
  refine irreducible_of_mirror hp.not_isUnit (fun q hpq => ?_) h
  have hq : IsUnitTrinomial q := (isUnitTrinomial_iff'' hpq).mp hp
  obtain ⟨k, m, n, hkm, hmn, u, v, w, hp⟩ := hp
  obtain ⟨k', m', n', hkm', hmn', x, y, z, hq⟩ := hq
  have hk : k = k' := by
    rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ←
      trinomial_natTrailingDegree hkm hmn u.ne_zero, ← hp, ← natTrailingDegree_mul_mirror, hpq,
      natTrailingDegree_mul_mirror, hq, trinomial_natTrailingDegree hkm' hmn' x.ne_zero]
  have hn : n = n' := by
    rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natDegree hkm hmn w.ne_zero, ←
      hp, ← natDegree_mul_mirror, hpq, natDegree_mul_mirror, hq,
      trinomial_natDegree hkm' hmn' z.ne_zero]
  subst hk
  subst hn
  rcases eq_or_eq_neg_of_sq_eq_sq (y : ℤ) (v : ℤ)
      ((Int.isUnit_sq y.isUnit).trans (Int.isUnit_sq v.isUnit).symm) with
    (h1 | h1)
  · rw [h1] at hq
    rcases irreducible_aux3 hkm hmn hkm' hmn' u v w x z hp hq hpq with (h2 | h2)
    · exact Or.inl h2
    · exact Or.inr (Or.inr (Or.inl h2))
  · rw [h1] at hq
    rw [trinomial_def] at hp
    rw [← neg_inj, neg_add, neg_add, ← neg_mul, ← neg_mul, ← neg_mul, ← C_neg, ← C_neg, ← C_neg]
      at hp
    rw [← neg_mul_neg, ← mirror_neg] at hpq
    rcases irreducible_aux3 hkm hmn hkm' hmn' (-u) (-v) (-w) x z hp hq hpq with (rfl | rfl)
    · exact Or.inr (Or.inl rfl)
    · exact Or.inr (Or.inr (Or.inr p.mirror_neg))

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

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
⊢ (∃ b_1, norm x * b_1 = 1 ∧ b_1 * norm x = 1) → ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1

Tactic:
rintro ⟨r, hr, hr'⟩

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : norm x * r = 1
hr' : r * norm x = 1
⊢ ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 0
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = -1
h✝ : ¬P.eraseLead = 0
this✝ : ((X - C η) * P).eraseLead.signVariations + 1 = ((X - C η) * P).signVariations
this : ((X - C η) * P).eraseLead.eraseLead.signVariations ≤ ((X - C η) * P).eraseLead.signVariations
⊢ ((X - C η) * P.eraseLead).signVariations ≤ ((X - C η) * P).eraseLead.signVariations

Tactic:
rwa [← eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero hη.ne']

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 0
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = -1
h✝ : ¬P.eraseLead = 0
this✝ : ((X - C η) * P).eraseLead.signVariations + 1 = ((X - C η) * P).signVariations
this : ((X - C η) * P).eraseLead.eraseLead.signVariations ≤ ((X - C η) * P).eraseLead.signVariations
⊢ P.nextCoeff = 0
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k

Tactic:
rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case mul
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
ih_y :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦y⟧ =
    F ⟦y⟧
hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧
⊢ ∀ (x y : EnvelGroup R), F (Mul.mul x y) = F x * F y

Tactic:
exact F.map_mul

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₁ : IsSumNonzeroSq s₁
h₂ : IsSumNonzeroSq s₂
⊢ IsSumNonzeroSq (s₁ + s₂)

Tactic:
by
  induction h₁ <;> simp_all [sq_add, add_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s : R
hs : s ≠ 0
h : IsSumSq s
⊢ IsSumNonzeroSq s

Tactic:
by
    induction h with
    | zero => grind
    | @sq_add a s hs ih =>
    rcases eq_or_ne a 0 with (rfl | ne_a)
    · simp_all
    · rcases eq_or_ne s 0 with (rfl | ne_s)
      · simpa using IsSumNonzeroSq.sq ne_a
      · exact IsSumNonzeroSq.sq_add ne_a (ih ne_s)

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

Goal state before:
pp: R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toSemiring = inst₂.toSemiring
⊢ inst₁ = inst₂

Tactic:
have h₂ : inst₁.toNonAssocRing = inst₂.toNonAssocRing := by
    ext : 1 <;> assumption

Goal state after:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toSemiring = inst₂.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case mpr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS → a ∈ NonUnitalSubsemiring.center α

Tactic:
· rintro ⟨hc, ⟨T, hT⟩⟩
    have e1 (d : α) : T d = a * d := congr($hT d)
    have e2 (d : α) : T d = d * a := congr($(hT.trans hc.symm) d)
    constructor
    case comm => exact (congr($hc.symm ·))
    case left_assoc => simpa [e1] using (map_mul_right T · ·)
    case right_assoc => simpa [e2] using (map_mul_left T · ·)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝¹ : DecidableEq G'
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
⊢ (f.coeff.sum fun x1 x2 ↦ (g x1 x2).coeff).support ⊆ f.coeff.support.biUnion fun a ↦ (g a (f.coeff a)).coeff.support

Tactic:
apply Finsupp.support_sum

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
p q : SkewMonoidAlgebra k G
⊢ p = q ↔ ∀ (n : G), p.coeff n = q.coeff n

Tactic:
rcases p with ⟨f : G →₀ k⟩
  rcases q with ⟨g : G →₀ k⟩
  simpa [coeff] using DFunLike.ext_iff (f := f) (g := g)

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

Goal state before:
pp: case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ x + y ≤ x + z

Tactic:
add_eq_right hy

Goal state after:
case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ y ≤ x + z
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
x : R
⊢ IsUnit (x • 1 - (star f).ofConv) ↔ IsUnit (star x • 1 - f.ofConv)

Tactic:
← isUnit_intrinsicStar_iff

Goal state after:
R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
x : R
⊢ IsUnit (star (toConv (x • 1 - (star f).ofConv))).ofConv ↔ IsUnit (star x • 1 - f.ofConv)
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
⊢ (of R) (A.compHahnSeries B (u + v)).ofIterate =
    (of R) (A.compHahnSeries B u).ofIterate + (of R) (A.compHahnSeries B v).ofIterate

Tactic:
ext g

Goal state after:
Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
g : Lex (Γ' × Γ)
⊢ ((of R).symm ((of R) (A.compHahnSeries B (u + v)).ofIterate)).coeff g =
    ((of R).symm ((of R) (A.compHahnSeries B u).ofIterate + (of R) (A.compHahnSeries B v).ofIterate)).coeff g
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
x : U
⊢ (of R) (A.compHahnSeries B (r • x)).ofIterate = (RingHom.id R) r • (of R) (A.compHahnSeries B x).ofIterate

Tactic:
ext g

Goal state after:
Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
x : U
g : Lex (Γ' × Γ)
⊢ ((of R).symm ((of R) (A.compHahnSeries B (r • x)).ofIterate)).coeff g =
    ((of R).symm ((RingHom.id R) r • (of R) (A.compHahnSeries B x).ofIterate)).coeff g
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
unop✝ : Opens ↑↑Z
⊢ g.c.app (op unop✝) ≫
      Y.presheaf.map ((Opens.map g.base).map (homOfLE ⋯).op.unop).op ≫
        Y.presheaf.map (eqToHom ⋯ ≫ (⋯.functor.map (eqToHom ⋯)).op) =
    g.c.app (op unop✝) ≫ Y.presheaf.map (⋯.adjunction.counit.app ((Opens.map g.base).obj unop✝)).op

Tactic:
← Y.presheaf.map_comp

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
unop✝ : Opens ↑↑Z
⊢ g.c.app (op unop✝) ≫
      Y.presheaf.map (((Opens.map g.base).map (homOfLE ⋯).op.unop).op ≫ eqToHom ⋯ ≫ (⋯.functor.map (eqToHom ⋯)).op) =
    g.c.app (op unop✝) ≫ Y.presheaf.map (⋯.adjunction.counit.app ((Opens.map g.base).obj unop✝)).op
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : ↑x ∈ X.basicOpen s
n : ℕ
hf : s ^ n * f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Tactic:
by
  rw [Scheme.mem_basicOpen X s x x.2] at hx
  have hu : IsUnit (X.presheaf.germ _ x x.2 (s ^ n)) := by
    rw [map_pow]
    exact IsUnit.pow n hx
  rw [← hu.mul_right_eq_zero, ← map_mul, hf, map_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ CoverPreserving (Opens.grothendieckTopology ↥Y) (Opens.grothendieckTopology ↥X) (Opens.map f.base)

Tactic:
exact coverPreserving_opens_map f.base

Goal state after: