mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p✝ q✝ : A[X]
a✝¹ :
  d' ((aeval x) p✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x
a✝ :
  d' ((aeval x) q✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x
⊢ d' ((aeval x) (p✝ + q✝)) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs (p✝ + q✝))) +
      (aeval x) (derivative (p✝ + q✝)) • d' x

Tactic:
simp_all only [map_add, add_smul]

Goal state after:
case add
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p✝ q✝ : A[X]
a✝¹ :
  d' ((aeval x) p✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x
a✝ :
  d' ((aeval x) q✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x
⊢ (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x +
      ((PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) +
        (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) +
      ((aeval x) (derivative p✝) • d' x + (aeval x) (derivative q✝) • d' x)
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
⊢ p.IsMonicOfDegree n ↔ p.natDegree ≤ n ∧ p.coeff n = 1

Tactic:
by
  simp only [isMonicOfDegree_iff']
  refine ⟨fun ⟨H₁, H₂⟩ ↦ ⟨H₁.le, H₁ ▸ Monic.coeff_natDegree H₂⟩, fun ⟨H₁, H₂⟩ ↦ ⟨?_, ?_⟩⟩
  · exact natDegree_eq_of_le_of_coeff_ne_zero H₁ <| H₂ ▸ one_ne_zero
  · exact monic_of_natDegree_le_of_coeff_eq_one n H₁ H₂

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

Goal state before:
pp: case refine_2
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
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀ (x : ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩).domain),
    (withTopOrderIso M) (ofLex (↑↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ x)).orderTop = ArchimedeanClass.mk ↑x
⊢ ∀ (a : M),
    ArchimedeanClass.mk a = (withTopOrderIso M) (ofLex ((f ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) a)).orderTop

Tactic:
simp_rw [LinearPMap.mk_apply] at harch

Goal state after:
case refine_2
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
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch : ∀ (x : ↥⊤), (withTopOrderIso M) (ofLex (f x)).orderTop = ArchimedeanClass.mk ↑x
⊢ ∀ (a : M),
    ArchimedeanClass.mk a = (withTopOrderIso M) (ofLex ((f ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) a)).orderTop
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Module S R
c : S
p : R[X]
n : ℕ
⊢ (c • p).homogenize n = c • p.homogenize n

Tactic:
simp [homogenize, Finset.smul_sum, MvPolynomial.smul_monomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
c : R
p : R[X]
n : ℕ
⊢ (C c * p).homogenize n = MvPolynomial.C c * p.homogenize n

Tactic:
simp only [C_mul', homogenize_smul, MvPolynomial.C_mul']

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
⊢ (ofFn n) v = ∑ i, (monomial ↑i) (v i)

Tactic:
by
  by_cases h : n = 0
  · subst h
    simp [ofFn]
  · rw [as_sum_range' (ofFn n v) n <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr h) v]
    simp [Finset.sum_range]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ MvPolynomial.X 0 ^ m * (MvPolynomial.monomial fun₀ | 1 => n - m) 1 = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)

Tactic:
← MvPolynomial.X_pow_eq_monomial

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m) = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p r : R[X]
hp₀ : p ≠ 0
hr₀ : r ≠ 0
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree

Tactic:
rw [natDegree_mul hp₀ hr₀, homogenize_mul _ _ le_rfl le_rfl]
    apply dvd_mul_right

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
by_cases hab : R a b
    · simpa [destutter_cons_cons, hab] using! hl₁.tail.length_le_length_destutter (hl.cons _)
    · simpa [destutter_cons_cons, hab] using! hl₁.length_le_length_destutter (hl.cons_cons _)

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ eval₂ RingHom.smulOneHom x p = p.smeval x

Tactic:
rw [smeval_eq_sum, eval₂_eq_sum]
  congr 1 with e a
  simp only [RingHom.smulOneHom_apply, smul_one_mul, smul_pow]

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

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

Tactic:
clear *-hgg

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (∏ i ∈ s, g i)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (d + 1 + 1)) (P.coeff (d + 1)) -
      ((monomial (d + 1)) (P.coeff d) - (monomial (d + 1)) (η * P.coeff (d + 1))) =
    X * P - C η * P - ((monomial (d + 1 + 1)) (P.coeff (d + 1)) - (monomial (d + 1)) (η * P.coeff (d + 1))) -
      (monomial (d + 1)) (P.coeff (d + 1 - 1))

Tactic:
Nat.add_sub_cancel

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (d + 1 + 1)) (P.coeff (d + 1)) -
      ((monomial (d + 1)) (P.coeff d) - (monomial (d + 1)) (η * P.coeff (d + 1))) =
    X * P - C η * P - ((monomial (d + 1 + 1)) (P.coeff (d + 1)) - (monomial (d + 1)) (η * P.coeff (d + 1))) -
      (monomial (d + 1)) (P.coeff d)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (star (x✝¹ + x✝)).re = (star x✝¹ + star x✝).re

Tactic:
by simp only [re_star, re_add, im_add]; ring

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y : R}, act' (x ◃ y) = act' x ◃ act' y

Tactic:
intro x y

Goal state after:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) = act' x ◃ act' y
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (L b) (L a)

Tactic:
rw [NonUnitalNonAssocSemiring.mem_center_iff, CentroidHom.centroid_eq_centralizer_mulLeftRight,
    Subsemiring.mem_centralizer_iff, AddMonoid.End.mulRight_eq_mulLeft, Set.union_self]
  aesop

Goal state after:
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✝ : NonAssocSemiring α
T : CentroidHom α
x✝ : α
⊢ (centerToCentroid.toFun ((fun T ↦ ⟨T 1, ⋯⟩) T)) x✝ = T x✝

Tactic:
MulHom.toFun_eq_coe,

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
x✝ : α
⊢ (centerToCentroid.toMulHom ((fun T ↦ ⟨T 1, ⋯⟩) T)) x✝ = T x✝
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : CentroidHom α
a b : α
⊢ star (f (star (a * b))) = star (f (star a)) * b

Tactic:
by simp only [star_mul, map_mul_left, star_star]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support

Tactic:
simp only [update_def, support_eq_skewMonoidAlgebra_support, SkewMonoidAlgebra.support_update]
  split_ifs <;> simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f + g).sum h = f.sum h + g.sum h

Tactic:
show f + g = ⟨f.coeff + g.coeff⟩ by rw [ofCoeff_add, eta]

Goal state after:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { coeff := f.coeff + g.coeff }.sum h = f.sum h + g.sum h
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f + g).sum h = f.sum h + g.sum h

Tactic:
show f + g = ⟨f.coeff + g.coeff⟩ by rw [ofCoeff_add, eta]

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { coeff := f.coeff + g.coeff }.sum h = f.sum h + g.sum h
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
u : ↥(unitary R)
x✝ : R
⊢ ((MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits u))).toFun (star x✝) =
    star (((MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits u))).toFun x✝)

Tactic:
dsimp [ConjAct.units_smul_def]

Goal state after:
S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
u : ↥(unitary R)
x✝ : R
⊢ ↑u * star x✝ * ↑u⁻¹ = star (↑u * x✝ * ↑u⁻¹)
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∀ (a : R), a * (↑(toUnits v)⁻¹ * ↑(toUnits u)) = ↑(toUnits v)⁻¹ * ↑(toUnits u) * a) ↔
    ∃ α, ↑(toUnits u) = α • ↑(toUnits v)

Tactic:
← Subalgebra.mem_center_iff (R := S),

Goal state after:
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ ↑(toUnits v)⁻¹ * ↑(toUnits u) ∈ Subalgebra.center S R ↔ ∃ α, ↑(toUnits u) = α • ↑(toUnits v)
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∀ (a : R), a * (↑(toUnits v)⁻¹ * ↑(toUnits u)) = ↑(toUnits v)⁻¹ * ↑(toUnits u) * a) ↔ ∃ α, u = α • v

Tactic:
← Subalgebra.mem_center_iff (R := S),

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ ↑(toUnits v)⁻¹ * ↑(toUnits u) ∈ Subalgebra.center S R ↔ ∃ α, u = α • v
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)
α : R
x : V
⊢ x ∈ (star f).ofConv.eigenspace α ↔ star x ∈ f.ofConv.eigenspace (star α)

Tactic:
by
  simp_rw [mem_eigenspace_iff, intrinsicStar_apply, star_eq_iff_star_eq, star_smul, eq_comm]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ (eqToHom ⋯ ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x)) ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)

Tactic:
rw [Category.assoc, ← stalkMap.comp, congr_hom _ _ (IsIso.hom_inv_id α), stalkMap.id,
        eqToHom_trans_assoc, eqToHom_refl, Category.id_comp]

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
⊢ IsCompatible (sheaf X).obj V g

Tactic:
intro x y

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
⊢ (ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLELeft (V y)).op)) (g x) =
    (ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLERight (V y)).op)) (g y)
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
U : Opens ↑↑Y
eq₁ :
  H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫
      H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) =
    eqToHom ⋯
eq₂ :
  Y.presheaf.map (eqToHom ⋯) ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯)
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))

Tactic:
eqToHom_map

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫
      H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) =
    eqToHom ⋯
eq₂ :
  eqToHom ⋯ ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯)
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
⊢ f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) = Y.presheaf.map (homOfLE ⋯).op

Tactic:
by
  rw [invApp, ← Category.assoc, IsIso.comp_inv_eq, f.c.naturality]
  congr

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ IsUnit ((algebraMap ↑R ↑((structurePresheafInCommRingCat ↑R).stalk x)) f) ↔ f ∉ x.asIdeal

Tactic:
rw [← isUnit_map_iff (StructureSheaf.stalkIso R x).symm, AlgEquiv.commutes]

Goal state after:
R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ IsUnit ((algebraMap (↑R) (Localization.AtPrime x.asIdeal)) f) ↔ f ∉ x.asIdeal
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫ X.presheaf.map (eqToHom ⋯) =
    app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
by rw [eqToHom_op]; rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
⊢ IsIso ((colimit.ι F i).hom.c.app (op (⋯.functor.obj U)))

Tactic:
by
    have h₁ := ι_preservesColimitIso_inv SheafedSpace.forgetToPresheafedSpace F i
    have h₂ : colimit.ι F i =
      { hom := (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫
        (preservesColimitIso _ F).inv) } :=
      InducedCategory.hom_ext h₁.symm
    have H :
      IsOpenEmbedding
        (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) i ≫
            (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv).base := by
      have := h₁.symm
      convert! sigma_ι_isOpenEmbedding F i
    suffices IsIso <| (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) i ≫
        (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv).c.app <|
      op (H.functor.obj U) by
      convert! this
    rw [PresheafedSpace.comp_c_app,
      ← PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π]
    -- Porting note: this instance created manually to make the `inferInstance` below work
    have : IsIso (preservesColimitIso forgetToPresheafedSpace F).inv.c := inferInstance
    suffices IsIso (limit.π (PresheafedSpace.componentwiseDiagram
      (F ⋙ SheafedSpace.forgetToPresheafedSpace) ((Opens.map
        (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv.base).obj
          (H.functor.obj U))) (op i)) from inferInstance
    apply limit_π_isIso_of_is_strict_terminal
    rintro ⟨j⟩ hj
    dsimp
    convert! (F.obj j).sheaf.isTerminalOfEmpty using 3
    convert! image_preimage_is_empty F i j (fun h => hj (congr_arg op h.symm)) U using 6
    exact congr_arg PresheafedSpace.Hom.base h₁

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen s))))) s ^ n)
      ((toBasicOpenₗ R M s) (LocalizedModule.mk f ⟨(fun x ↦ s ^ x) n, ⋯⟩)) =
    ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen s))))) s ^ n)
      (const f (↑⟨(fun x ↦ s ^ x) n, ⋯⟩) (basicOpen s) ⋯)

Tactic:
rw [← map_pow]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen s))))) (s ^ n))
      ((toBasicOpenₗ R M s) (LocalizedModule.mk f ⟨(fun x ↦ s ^ x) n, ⋯⟩)) =
    ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen s))))) (s ^ n))
      (const f (↑⟨(fun x ↦ s ^ x) n, ⋯⟩) (basicOpen s) ⋯)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(TopCat.Hom.hom U.ι.base) = ↑U

pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective
    (⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base))

Tactic:
· exact Subtype.range_coe

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective
    (⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base))