mathlib-initiative/mathlib-tactics huggingface dataset:
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 η) * 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_mul,

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)
⊢ (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)
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝¹ : Monoid S
inst✝ : MulAction S R
x✝² x✝¹ : S
x✝ : QuadraticAlgebra R a b
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by ext <;> simp [mul_smul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ LinearMap.det (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) = norm z

Tactic:
rw [← LinearMap.det_toMatrix <| basis ..]
  have : !![z.re, a * z.im; z.im, z.re + b * z.im].det = z.norm := by
    simp [norm]
    ring
  convert! this
  apply LinearEquiv.eq_symm_apply _ |>.mp
  ext1 w
  apply basis .. |>.repr.injective
  apply DFunLike.coe_injective
  rw [LinearMap.toMatrix_symm, Matrix.repr_toLin]
  ext i
  fin_cases i
    <;> simp
    <;> ring

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
x : ι
hx : x ∈ s
⊢ 1 ^ n x = 1

Tactic:
one_pow

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
x : ι
hx : x ∈ s
⊢ 1 = 1
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1

Tactic:
act_one

Goal state after:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = (x ◃ y) ◃ x
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x y : S
h : (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
⊢ x ◃ y ◃ 1 = x ◃ y

Tactic:
act_one

Goal state after:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
h : (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
⊢ x ◃ y = x ◃ y
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x : S
⊢ x ◃ 1 ◃ 1 = x ◃ 1

Tactic:
act_one

Goal state after:
S : Type u_1
inst✝ : UnitalShelf S
x : S
⊢ x ◃ 1 = x ◃ 1
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y

Tactic:
act_one

Goal state after:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = x ◃ x ◃ y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toDistrib R)

Tactic:
intro _ _ h

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : a₁✝.toDistrib = a₂✝.toDistrib
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
intro _ _ h

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalSemiring R)

Tactic:
intro _ _ h

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonAssocSemiring R)

Tactic:
intro _ _ h

Goal state after:
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalSemiring R)

Tactic:
intro _ _ h

Goal state after:
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonAssocSemiring R)

Tactic:
intro _ _ h

Goal state after:
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalRing R)

Tactic:
intro _ _ h

Goal state after:
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonAssocRing R)

Tactic:
intro _ _ h

Goal state after:
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toSemiring R)

Tactic:
intro _ _ h

Goal state after:
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
⊢ ∀ (g : G) (r : k), g • r = r

Tactic:
exact fun _ _ ↦ smul_algebraMap _ (algebraMap k k _)

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (b + a) (a + c)

Tactic:
add_comm a c

Goal state after:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (b + a) (c + a)
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝ } * 0 = 0

Tactic:
simp only [mul_quot, ← zero_quot, mul_zero]

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

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : Semiring R
a : R
⊢ (C a).coeff n = if n = 0 then a else 0

Tactic:
convert! coeff_monomial using 2; simp [eq_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
c : R
h : c ≠ 0
⊢ (C c * X).support = {1}

Tactic:
rw [C_mul_X_eq_monomial, support_monomial 1 h]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : SkewPolynomial R
n : ℕ
⊢ (-p).coeff n = -p.coeff n

Tactic:
by
  simp [← add_eq_zero_iff_eq_neg, ← coeff_add, neg_add_cancel p]

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
⊢ Finset.map toAdd.toEmbedding
      (if a = 0 then (SkewMonoidAlgebra.support p).erase (ofAdd n)
      else insert (ofAdd n) (SkewMonoidAlgebra.support p)) =
    if a = 0 then (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p)).erase n
    else insert n (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p))

Tactic:
split_ifs

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
h✝ : a = 0
⊢ Finset.map toAdd.toEmbedding ((SkewMonoidAlgebra.support p).erase (ofAdd n)) =
    (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p)).erase n

case neg
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
h✝ : ¬a = 0
⊢ Finset.map toAdd.toEmbedding (insert (ofAdd n) (SkewMonoidAlgebra.support p)) =
    insert n (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p))
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), ↑v * a * ↑(star v) = ↑u * a * ↑(star u)) ↔ ∃ α, ↑u = α • ↑v

Tactic:
star_eq_inv,

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)
⊢ (∀ (a : R), ↑v * a * ↑v⁻¹ = ↑u * a * ↑u⁻¹) ↔ ∃ α, ↑u = α • ↑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), ↑v * a * ↑(star v) = ↑u * a * ↑(star u)) ↔ ∃ α, u = α • v

Tactic:
star_eq_inv,

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)
⊢ (∀ (a : R), ↑v * a * ↑v⁻¹ = ↑u * a * ↑u⁻¹) ↔ ∃ α, u = α • v
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : a ≤ b
⊢ untrop a = untrop a

case neg
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop b = untrop b
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : a ≤ b
⊢ untrop b = untrop b

case neg
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop a = untrop a
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ y ^ n = x ^ n + y ^ n

Tactic:
add_eq_right (pow_le_pow_left' h _)

Goal state after:
case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ y ^ n = y ^ n
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym 1 * unsym x✝ + unsym x✝ * unsym 1)) = x✝

Tactic:
unsym_one,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (1 * unsym x✝ + unsym x✝ * 1)) = x✝
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym x✝ * unsym 1 + unsym 1 * unsym x✝)) = x✝

Tactic:
unsym_one,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym x✝ * 1 + 1 * unsym x✝)) = x✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
⊢ (single x r * f).coeff y = r * x • f.coeff z

Tactic:
by
  classical
  have : (f.sum fun a b ↦ ite (x * a = y) (0 * x • b) 0) = 0 := by simp
  calc
    (single x r * f).coeff y =
        sum f fun a b ↦ ite (x * a = y) (r * x • b) 0 :=
      (coeff_mul _ _ _).trans <| sum_single_index this
    _ = f.sum fun a b ↦ ite (a = z) (r * x • b) 0 := by simp [H]
    _ = if z ∈ f.support then r * x • f.coeff z else 0 := (f.support.sum_ite_eq' _ _)
    _ = _ := by split_ifs with h <;> simp [support] at h <;> simp [h]

Goal state after:
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
⊢ Function.Injective ⇑coeff

Tactic:
intro _ _ h

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
a₁✝ a₂✝ : HVertexOperator Γ R V W
h : coeff a₁✝ = coeff a₂✝
⊢ a₁✝ = a₂✝
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₂ :
  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:
eq₂,

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)) ≫
      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 ⋯) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
j : J
⊢ (colimitCocone F).ι.app j ≫ desc F s = s.ι.app j

Tactic:
by
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): the original proof is just
  -- `ext <;> dsimp [desc, descCApp] <;> simpa`,
  -- but this has to be expanded a bit
  ext U
  · simp [desc]
  · simp only [op_obj, desc, descCApp, Presheaf.comp_app, comp_c_app, colimitCocone_ι_app_c, assoc]
    rw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc]
    simp

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

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U))).inv ≫
        ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U)) ≫
          (F.obj j).presheaf.map (eqToHom ⋯) ≫
            ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
colimitCocone_ι_app_c,

Goal state after:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U))).inv ≫
        (limit.π (pushforwardDiagramToColimit F).leftOp (op j)).app
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U)) ≫
          (F.obj j).presheaf.map (eqToHom ⋯) ≫
            ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
⊢ ∃ R f_1, x ∈ Set.range ⇑(ConcreteCategory.hom f_1.base) ∧ LocallyRingedSpace.IsOpenImmersion f_1

Tactic:
obtain ⟨R, i, _, h₁, h₂⟩ :=
    Scheme.exists_affine_mem_range_and_range_subset (U := ⟨_, H.base_open.isOpen_range⟩) ⟨x, rfl⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ ∃ R f_1, x ∈ Set.range ⇑(ConcreteCategory.hom f_1.base) ∧ LocallyRingedSpace.IsOpenImmersion f_1
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ x ∈
    Set.range
      ⇑(ConcreteCategory.hom
          (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom'
              h₂).base)

Tactic:
LocallyRingedSpace.IsOpenImmersion.lift_range

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ x ∈ ⇑(ConcreteCategory.hom (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f).base) ⁻¹' Set.range ⇑i
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥U
⊢ (U.stalkIso x).inv ≫ 𝟙 ((↑U).presheaf.stalk x) = Hom.stalkMap U.ι x

Tactic:
Iso.inv_comp_eq

Goal state after:
X : Scheme
U : X.Opens
x : ↥U
⊢ 𝟙 ((↑U).presheaf.stalk x) = (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ unop (op (basicOpen (g' * g)))
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy⟩

Tactic:
rw [PrimeSpectrum.basicOpen_mul] at hy
    obtain ⟨hgy, H⟩ := hfg ⟨y, hg'U hy.1⟩
    refine (LocalizedModule.mk_eq.mpr ⟨1, ?_⟩).trans H.symm
    simp [Submonoid.smul_def, ← smul_assoc]; ring_nf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ appLE (resLE f U V e) O W e' = appLE f (U.ι ''ᵁ O) (V.ι ''ᵁ W) ⋯

Tactic:
dsimp [appLE, resLE]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ (app (f ∣_ U) O ≫ app (X.homOfLE e) ((f ∣_ U) ⁻¹ᵁ O)) ≫ X.presheaf.map (homOfLE ⋯).op =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ X.isoSpec.hom ≫ Spec.map (Hom.appTop f) = f ≫ Y.isoSpec.hom

Tactic:
by
  simp only [isoSpec, asIso_hom, Scheme.toSpecΓ_naturality]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
⊢ (↑U).OpenCover

Tactic:
refine Cover.copy (𝒰.pullback₁ U.ι) 𝒰.I₀ _ (𝒰.f · ∣_ U) (Equiv.refl _)
    (fun i ↦ IsOpenImmersion.isoOfRangeEq (Opens.ι _) (pullback.snd _ _) ?_) ?_

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ Set.range ⇑(𝒰.f i ⁻¹ᵁ U).ι = Set.range ⇑(pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀) i)))

case refine_2
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
⊢ ∀ (i : 𝒰.I₀),
    𝒰.f i ∣_ U =
      (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι (pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀) i))) ⋯).hom ≫
        (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f ((Equiv.refl 𝒰.I₀) i)