mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
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
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
have hpgd : ∏ i ∈ s, g i ∣ _ := cop.symm.dvd_of_dvd_mul_left (hf.symm ▸ dvd_mul_left _ _)

Goal state after:
case cons
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
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2
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)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
⊢ (aeval r) (sumIDeriv p) = 0 + (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)

Tactic:
rw [sumIDeriv_apply, map_sum, map_sum, this]

Goal state after:
case inr.refine_2
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)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
⊢ ∑ x ∈ range q ∪ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) =
    0 + (q - 1)! • eval r p' + q ! • ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) (c x)
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ (MulOpposite.op s • z).re = (s • z).re

Tactic:
exact op_smul_eq_smul _ _

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ (MulOpposite.op s • z).im = (s • z).im

Tactic:
exact op_smul_eq_smul _ _

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
ext <;> simp [sq]; field_simp; simp [NNRat.cast_def]

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
act_act_self_eq,

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

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x

pp: R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y

Tactic:
· rw [← left_cancel (x ◃ x), right_inv, self_act_act_eq]

Goal state after:
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime✝ : IsCoprime g₁ g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
hg : ∀ i ∈ Finset.univ, (g i).Monic
hcoprime : (↑Finset.univ).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q : R[X]
r : Bool → R[X]
hr : ∀ i ∈ Finset.univ, (r i).degree < (g i).degree
hf : ↑f / ∏ i, ↑(g i) = ↑q + ∑ i, ↑(r i) / ↑(g i)
⊢ ∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂

Tactic:
refine ⟨q, r true, r false, hr true (Finset.mem_univ true), hr false (Finset.mem_univ false), ?_⟩

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime✝ : IsCoprime g₁ g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
hg : ∀ i ∈ Finset.univ, (g i).Monic
hcoprime : (↑Finset.univ).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q : R[X]
r : Bool → R[X]
hr : ∀ i ∈ Finset.univ, (r i).degree < (g i).degree
hf : ↑f / ∏ i, ↑(g i) = ↑q + ∑ i, ↑(r i) / ↑(g i)
⊢ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑(r true) / ↑g₁ + ↑(r false) / ↑g₂
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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
⊢ ∀ (a b : RingQuot r), a + b = b + a

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [add_quot, add_comm]

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

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

Tactic:
star_star

Goal state after:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : CentroidHom α
x✝ : α
⊢ f x✝ = f x✝
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ g (star (f (star a))) = star (star (g (star (f (star a)))))

Tactic:
star_star

Goal state after:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ g (star (f (star a))) = g (star (f (star a)))
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ star (f (star (g (star (star a))))) = star (f (star (g a)))

Tactic:
star_star

Goal state after:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ star (f (star (g a))) = star (f (star (g a)))
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ star (star a) * ↑(star z) = a * ↑(star z)

Tactic:
star_star

Goal state after:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ a * ↑(star z) = a * ↑(star z)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p * C 0 = q * C 0

Tactic:
C_0,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p * 0 = q * 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p = q

Tactic:
by rw [← mul_one p, ← mul_one q, ← C_1, ← h01, C_0, mul_zero, mul_zero]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
g_hom : Type u_3
R : Type u_4
inst✝⁴ : NonAssocSemiring k
inst✝³ : One G
inst✝² : Semiring R
inst✝¹ : FunLike g_hom G R
inst✝ : OneHomClass g_hom G R
f : k →+* R
g : g_hom
⊢ (liftNC ↑f ⇑g) 1 = 1

Tactic:
simp only [one_def, liftNC_single, AddMonoidHom.coe_coe, map_one, mul_one]

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

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

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
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
· rw [add_eq_left h, add_eq_left (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
⊢ (x + y) ^ n = x ^ n + y ^ n
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Monoid G
inst✝⁴ : CommSemiring k
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
r : k
a : SkewMonoidAlgebra A G
⊢ r • a = (singleOneRingHom.comp (algebraMap k A)) r * a

Tactic:
by ext; simp [Algebra.smul_def, singleOneRingHom, coeff_single_one_mul]

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
E : Type u_6
inst✝⁵ : NonUnitalNonAssocSemiring E
inst✝⁴ : StarRing E
inst✝³ : Module R E
inst✝² : StarModule R E
inst✝¹ : SMulCommClass R E E
inst✝ : IsScalarTower R E E
x : E
⊢ toConv (mulRight R (star (star x))) = toConv (mulRight R x)

Tactic:
star_star

Goal state after:
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
E : Type u_6
inst✝⁵ : NonUnitalNonAssocSemiring E
inst✝⁴ : StarRing E
inst✝³ : Module R E
inst✝² : StarModule R E
inst✝¹ : SMulCommClass R E E
inst✝ : IsScalarTower R E E
x : E
⊢ toConv (mulRight R x) = toConv (mulRight R x)
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
U : Opens ↑↑Y
x : ↑↑X
hx : (ConcreteCategory.hom α.base) x ∈ U
⊢ Y.presheaf.germ U ((ConcreteCategory.hom α.base) x) hx ≫ Hom.stalkMap α x =
    α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx

Tactic:
Hom.stalkMap,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
U : Opens ↑↑Y
x : ↑↑X
hx : (ConcreteCategory.hom α.base) x ∈ U
⊢ Y.presheaf.germ U ((ConcreteCategory.hom α.base) x) hx ≫
      (stalkFunctor C ((ConcreteCategory.hom α.base) x)).map α.c ≫ stalkPushforward C α.base X.presheaf x =
    α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case refine_1
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
⊢ 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x)) ≫ 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x)) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))

Tactic:
Category.id_comp

Goal state after:
case refine_1
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
⊢ 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x)) = 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))
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
⊢ 𝟙 (X.presheaf.stalk x) ≫ 𝟙 (X.presheaf.stalk x) = 𝟙 (X.presheaf.stalk x)

Tactic:
Category.id_comp

Goal state after:
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
⊢ 𝟙 (X.presheaf.stalk x) = 𝟙 (X.presheaf.stalk x)
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)
⊢ IsUnit f

Tactic:
by
  -- We pick a cover of `U` by open sets `V x`, such that `f` is a unit on each `V x`.
  choose V iVU m h_unit using fun x : U => X.isUnit_res_of_isUnit_germ U f x x.2 (h x.1 x.2)
  have hcover : U ≤ iSup V := by
    intro x hxU
    simp only [Opens.mem_iSup]
    tauto
  -- Let `g x` denote the inverse of `f` in `U x`.
  choose g hg using fun x : U => IsUnit.exists_right_inv (h_unit x)
  have ic : IsCompatible (sheaf X).obj V g := by
    intro x y
    apply section_ext X.sheaf (V x ⊓ V y)
    rintro z ⟨hzVx, hzVy⟩
    rw [germ_res_apply, germ_res_apply]
    apply (h z ((iVU x).le hzVx)).mul_right_inj.mp
    rw [← germ_res_apply X.presheaf (iVU x) z hzVx f]
    -- Porting note: change was not necessary in Lean3
    change X.presheaf.germ _ z hzVx _ * (X.presheaf.germ _ z hzVx _) =
      X.presheaf.germ _ z hzVx _ * X.presheaf.germ _ z hzVy (g y)
    rw [← map_mul, hg x, germ_res_apply X.presheaf _ _ _ f,
      ← germ_res_apply X.presheaf (iVU y) z hzVy f, ← map_mul, (hg y), map_one, map_one]
  -- We claim that these local inverses glue together to a global inverse of `f`.
  obtain ⟨gl, gl_spec, -⟩ :
    -- We need to rephrase the result from `ConcreteCategory` to `CommRingCat`.
    ∃ gl : X.presheaf.obj (op U), (∀ i, ((sheaf X).obj.map (iVU i).op) gl = g i) ∧ _ :=
    X.sheaf.existsUnique_gluing' V U iVU hcover g ic
  refine .of_mul_eq_one gl <| X.sheaf.eq_of_locally_eq' V U iVU hcover _ _ fun i ↦ ?_
  -- We need to rephrase the goal from `ConcreteCategory` to `CommRingCat`.
  change ((sheaf X).obj.map (iVU i).op).hom (f * gl) = ((sheaf X).obj.map (iVU i).op) 1
  rw [map_one, map_mul, gl_spec]
  exact hg i

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
⊢ IsClosed (X.zeroLocus s)

Tactic:
by
  apply isClosed_biInter
  intro i _
  simp only [isClosed_compl_iff]
  exact Opens.isOpen (X.basicOpen i)

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

Goal state before:
pp: case naturality
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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X Y : Jᵒᵖ
f : X ⟶ Y
⊢ ((F.map f.unop).c.app
          ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
            ((Opens.map
                    (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
              (op U))) ≫
        𝟙
            (((pushforward C (colimit.ι (F ⋙ forget C) (unop X))).obj
                  ((pushforward C ((F ⋙ forget C).map f.unop)).obj (F.obj (unop Y)).presheaf)).obj
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U))) ≫
          (pushforwardEq ⋯ (F.obj (unop Y)).presheaf).hom.app
            ((Opens.map
                    (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
              (op U))) ≫
      (F.obj (unop Y)).presheaf.map (eqToIso ⋯).hom =
    (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f

Tactic:
Category.id_comp

Goal state after:
case naturality
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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X Y : Jᵒᵖ
f : X ⟶ Y
⊢ ((F.map f.unop).c.app
          ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
            ((Opens.map
                    (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
              (op U))) ≫
        (pushforwardEq ⋯ (F.obj (unop Y)).presheaf).hom.app
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U))) ≫
      (F.obj (unop Y)).presheaf.map (eqToIso ⋯).hom =
    (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tU tV : (fun X ↦ X) ((subsheafToTypes P).presheaf.stalk x)
h : (ConcreteCategory.hom (stalkToFiber P x)) tU = (ConcreteCategory.hom (stalkToFiber P x)) tV
⊢ tU = tV

Tactic:
by
  -- We promise to provide all the ingredients of the proof later:
  let Q :
    ∃ (W : (OpenNhds x)ᵒᵖ) (s : ∀ w : (unop W).1, T w) (hW : P.pred s),
      tU = (subsheafToTypes P).presheaf.germ _ x (unop W).2 ⟨s, hW⟩ ∧
        tV = (subsheafToTypes P).presheaf.germ _ x (unop W).2 ⟨s, hW⟩ :=
    ?_
  · choose W s hW e using Q
    exact e.1.trans e.2.symm
  -- Then use induction to pick particular representatives of `tU tV : stalk x`
  dsimp at tU tV h
  obtain ⟨U, ⟨fU, hU⟩, rfl⟩ := jointly_surjective' tU
  obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := jointly_surjective' tV
  -- Decompose everything into its constituent parts:
  simp only [Functor.whiskeringLeft_obj_obj, Functor.comp_obj, Functor.op_obj,
    subpresheafToTypes_obj, stalkToFiber_ι] at h
  specialize w (unop U) (unop V) fU hU fV hV h
  rcases w with ⟨W, iU, iV, w⟩
  -- and put it back together again in the correct order.
  refine ⟨op W, fun w ↦ fU (iU w : (unop U).1), P.res ?_ _ hU, ?_⟩
  · rcases W with ⟨W, m⟩
    exact iU
  · exact ⟨colimit_sound iU.op (Subtype.ext rfl), colimit_sound iV.op (Subtype.ext (funext w).symm)⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ 𝟙 Γ(X, U) ≫ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op

Tactic:
Category.id_comp

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) =
    𝟙 ((X.restrict h).presheaf.obj (op U)) ≫ (X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))

Tactic:
Category.id_comp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) = (X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) ≫ inv ((X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))) =
    𝟙 ((X.restrict h).presheaf.obj (op U))

Tactic:
rw [IsIso.comp_inv_eq, Category.id_comp]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) = (X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
⊢ (Opens.map g.base).op.obj (op (⋯.functor.obj (unop U))) =
    ⋯.functor.op.obj ((Opens.map (pullback.fst f.base g.base)).op.obj U)

Tactic:
simp only [IsOpenMap.functor, op_inj_iff, Opens.map,
                    Functor.op_obj]
                  apply LE.le.antisymm
                  · rintro _ ⟨_, h₁, h₂⟩
                    use (TopCat.pullbackIsoProdSubtype _ _).inv ⟨⟨_, _⟩, h₂⟩
                    simpa [(TopCat.pullbackIsoProdSubtype_inv_fst_apply),
                      (TopCat.pullbackIsoProdSubtype_inv_snd_apply)]
                  · rintro _ ⟨x, h₁, rfl⟩
                    exact ⟨_, h₁, CategoryTheory.congr_fun pullback.condition x⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X Y S : Type u_2
f : X ⟶ S
⊢ ∀ (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))

Tactic:
g

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X Y S : Type u_2
f : X ⟶ S
g : Y ⟶ S
⊢ ∀ [inst : HasPullback f g], Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))