mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : α
⊢ ↑((fun T ↦ ⟨T 1, ⋯⟩) T) * x✝ = T x✝

Tactic:
← map_mul_right,

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✝ : α
⊢ T (1 * x✝) = T x✝
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✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ (f * g) a✝ * (r * ((f * g) a✝ - (g * f) a✝)) = (g * f) a✝ * (r * ((f * g) a✝ - (g * f) a✝))

Tactic:
← map_mul_right,

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ (f * g) (a✝ * (r * ((f * g) a✝ - (g * f) a✝))) = (g * f) a✝ * (r * ((f * g) a✝ - (g * f) a✝))
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✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ (f * g) (a✝ * (r * ((f * g) a✝ - (g * f) a✝))) = (g * f) a✝ * (r * ((f * g) a✝ - (g * f) a✝))

Tactic:
← map_mul_right,

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ (f * g) (a✝ * (r * ((f * g) a✝ - (g * f) a✝))) = (g * f) (a✝ * (r * ((f * g) a✝ - (g * f) a✝)))
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝¹ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
inst✝ : DecidableEq α
⊢ (f.update a b).coeff a' = if a' = a then b else f.coeff a'

Tactic:
simp [coeff_update, Function.update_apply]

Goal state after:
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 → Prop
inst✝ : Semiring T
r✝ : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r✝ x y → f x = f y
x : RingQuot r✝
a✝ b✝ : R
r : Rel r✝ a✝ b✝
⊢ f a✝ = f b✝

Tactic:
induction r with

Goal state after:
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 → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
x : RingQuot s
a✝ b✝ : A
r : Rel s a✝ b✝
⊢ f a✝ = f b✝

Tactic:
induction r with

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (monomial n) (a * 1) = (monomial n) (a • 1)

Tactic:
by simp [mul_one, smul_eq_mul]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
a : S
b : G →₀ k
⊢ { coeff := a • b } = smul a { coeff := b }

Tactic:
smul

Goal state after:
k : Type u_1
G : Type u_2
inst✝¹ : AddMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
a : S
b : G →₀ k
⊢ { coeff := a • b } = { coeff := a • b }
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)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : ↑v = 0
⊢ ↑u = ↑(1 • v)

Tactic:
simp [this, huv] at huv ⊢

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym (⅟2 * (⅟a * a + 1)) = 1

Tactic:
invOf_mul_self,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym (⅟2 * (1 + 1)) = 1
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym (⅟2 * 2) = 1

Tactic:
invOf_mul_self,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym 1 = 1
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym (⅟2 * (1 + ⅟a * a)) = 1

Tactic:
invOf_mul_self,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym (⅟2 * (1 + 1)) = 1
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 * ⅟2 *
        ((unsym a * unsym b + unsym b * unsym a) * unsym (a * a) +
          unsym (a * a) * (unsym a * unsym b + unsym b * unsym a))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))

Tactic:
add_mul,

Goal state after:
case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) +
          unsym (a * a) * (unsym a * unsym b + unsym b * unsym a))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 * ⅟2 *
      (unsym a * (unsym b * unsym (a * a)) + unsym a * (unsym (a * a) * unsym b) +
        (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a)

Tactic:
add_mul,

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 * ⅟2 *
      (unsym a * (unsym b * unsym (a * a)) + unsym a * (unsym (a * a) * unsym b) +
        (unsym b * unsym (a * a) * unsym a + unsym (a * a) * unsym b * unsym a))
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 * ⅟2 *
      (unsym a * (unsym b * unsym (a * a)) + unsym a * (unsym (a * a) * unsym b) +
        (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a)

Tactic:
rw [add_mul, ← add_assoc, ← mul_assoc, ← mul_assoc]

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym a * unsym (a * a) * unsym b + unsym b * unsym (a * a) * unsym a +
        unsym (a * a) * unsym b * unsym a)
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (fc.app (op U))) s = (ConcreteCategory.hom (gc.app (op U))) s

Tactic:
refine section_ext X.sheaf _ _ _ fun x hx ↦
    show X.presheaf.germ _ x _ _ = X.presheaf.germ _ x _ _ from ?_

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ (Opens.map f).obj (unop (op U))
⊢ (ConcreteCategory.hom (X.presheaf.germ ((Opens.map f).obj (unop (op U))) x hx))
      ((ConcreteCategory.hom (fc.app (op U))) s) =
    (ConcreteCategory.hom (X.presheaf.germ ((Opens.map f).obj (unop (op U))) x hx))
      ((ConcreteCategory.hom (gc.app (op U))) s)
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
⊢ ∀ {Z : SheafedSpace C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h

Tactic:
intro Z ⟨g, gc⟩ ⟨h, hc⟩ e

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
h : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
hc : X.presheaf ⟶ (pushforward C h).obj Z.presheaf
e : { hom := { base := g, c := gc } } ≫ f = { hom := { base := h, c := hc } } ≫ f
⊢ { hom := { base := g, c := gc } } = { hom := { base := h, c := hc } }
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
⊢ ∀ {Z : SheafedSpace C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h

Tactic:
intro Z ⟨g, gc⟩ ⟨h, hc⟩ e

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
h : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
hc : Z.presheaf ⟶ (pushforward C h).obj Y.presheaf
e : f ≫ { hom := { base := g, c := gc } } = f ≫ { hom := { base := h, c := hc } }
⊢ { hom := { base := g, c := gc } } = { hom := { base := h, c := hc } }
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X).c.app U = X.presheaf.map (𝟙 U)

Tactic:
id_c,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X.presheaf).app U = X.presheaf.map (𝟙 U)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case mk
X Y : LocallyRingedSpace
g : X ⟶ Y
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝, prop := prop✝ }.toHom = g.toHom
⊢ { toHom := toHom✝, prop := prop✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
X Y : LocallyRingedSpace
toHom✝¹ : X.Hom Y.toPresheafedSpace
prop✝¹ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝¹.stalkMap x))
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝¹, prop := prop✝¹ }.toHom = { toHom := toHom✝, prop := prop✝ }.toHom
⊢ { toHom := toHom✝¹, prop := prop✝¹ } = { toHom := toHom✝, prop := prop✝ }
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑↑(X.restrict h).toPresheafedSpace
⊢ IsLocalRing ↑((X.restrict h).presheaf.stalk x)

Tactic:
apply @RingEquiv.isLocalRing _ _ _ (X.isLocalRing (f x))

Goal state after:
X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑↑(X.restrict h).toPresheafedSpace
⊢ ↑(X.presheaf.stalk ((ConcreteCategory.hom f) x)) ≃+* ↑((X.restrict h).presheaf.stalk x)
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.hom ≫ H.inv).c.app (op ((Opens.map H.hom.base).obj U)) =
    (𝟙 X).c.app (op ((Opens.map H.hom.base).obj U)) ≫ X.presheaf.map (eqToHom ⋯)
eq₂ :
  Y.presheaf.map (eqToHom ⋯).op ≫ 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 ⋯).op
⊢ 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:
id_c,

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.hom ≫ H.inv).c.app (op ((Opens.map H.hom.base).obj U)) =
    (𝟙 X.presheaf).app (op ((Opens.map H.hom.base).obj U)) ≫ X.presheaf.map (eqToHom ⋯)
eq₂ :
  Y.presheaf.map (eqToHom ⋯).op ≫ 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 ⋯).op
⊢ 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.LocallyRingedSpace

Goal state before:
pp: X✝ X : LocallyRingedSpace
f : ∅ ⟶ X
⊢ f = X.emptyTo

Tactic:
ext ⟨⟩ x

Goal state after:
case h
X✝ X : LocallyRingedSpace
f : ∅ ⟶ X
carrier✝ : Set ↑↑X.toPresheafedSpace
is_open'✝ : IsOpen carrier✝
x : ↑(X.presheaf.obj (op { carrier := carrier✝, is_open' := is_open'✝ }))
⊢ (CommRingCat.Hom.hom
        ((f.c ≫ whiskerRight (eqToHom ⋯) ∅.presheaf).app (op { carrier := carrier✝, is_open' := is_open'✝ })))
      x =
    (CommRingCat.Hom.hom (X.emptyTo.c.app (op { carrier := carrier✝, is_open' := is_open'✝ }))) x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)

Tactic:
have hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V := by
      ext1
      exact Set.preimage_image_eq _ hf.injective

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
⊢ (locallyRingedSpaceMap (𝟙 R)).toHom = (𝟙 (locallyRingedSpaceObj R)).toHom

Tactic:
rw [Spec.locallyRingedSpaceMap_toHom, Spec.sheafedSpaceMap_id]

Goal state after:
R : CommRingCat
⊢ (𝟙 (sheafedSpaceObj R)).hom = (𝟙 (locallyRingedSpaceObj R)).toHom
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case mk
X Y : Scheme
g : X ⟶ Y
toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝ }.base = g.base
h_app : ∀ (U : Y.Opens), { toLRSHom' := toLRSHom'✝ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = app g U
⊢ { toLRSHom' := toLRSHom'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ { toLRSHom' := toLRSHom'✝¹ } = { toLRSHom' := toLRSHom'✝ }
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case mk
X Y : Scheme
g : X ⟶ Y
toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h : { toLRSHom' := toLRSHom'✝ }.toLRSHom = toLRSHom g
⊢ { toLRSHom' := toLRSHom'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h : { toLRSHom' := toLRSHom'✝¹ }.toLRSHom = { toLRSHom' := toLRSHom'✝ }.toLRSHom
⊢ { toLRSHom' := toLRSHom'✝¹ } = { toLRSHom' := toLRSHom'✝ }
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
⊢ f.copyBase g h = f

Tactic:
subst h
  obtain ⟨⟨⟨f₁, f₂⟩, f₃⟩, f₄⟩ := f
  simp only [Hom.copyBase]
  congr
  cat_disch

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

Goal state before:
pp: ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf : ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
hg : ∀ (i : ι) (x : X i), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom (g i i_1))
i : ι
y : X i
⊢ ∃ i_1, (ConcreteCategory.hom (f i)) y ∈ Set.range ⇑(ConcreteCategory.hom (g i_1.fst i_1.snd ≫ f i_1.fst))

Tactic:
obtain ⟨j, z, rfl⟩ := hg i y

Goal state after:
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf : ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
hg : ∀ (i : ι) (x : X i), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom (g i i_1))
i : ι
j : σ i
z : Y i j
⊢ ∃ i_1,
    (ConcreteCategory.hom (f i)) ((ConcreteCategory.hom (g i j)) z) ∈
      Set.range ⇑(ConcreteCategory.hom (g i_1.fst i_1.snd ≫ f i_1.fst))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ (appIso f U).inv ≫ appLE f (f ''ᵁ U) V e = X.presheaf.map (homOfLE ⋯).op

Tactic:
by
  simp only [appLE, appIso_inv_app_assoc, eqToHom_op]
  rw [← Functor.map_comp]
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
T : C
g✝ : T ⟶ S
W : ι → C
p₁ : (i : ι) → W i ⟶ T
p₂ : (i : ι) → W i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g✝ (f i)
Z : C
g : Z ⟶ T
hg : Presieve.ofArrows W p₁ g
⊢ P g

Tactic:
by
    obtain ⟨i⟩ := hg
    exact P.of_isPullback (h i).flip (hf ⟨i⟩)

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
Opens.map_obj,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' ↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } = Set.range ⇑f ∩ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) = Set.range ⇑g ∩ Set.range ⇑f

Tactic:
Opens.map_obj,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' ↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } = Set.range ⇑g ∩ Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst✝¹ : IsOpenImmersion iU
inst✝ : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
e : pullback iV f ≅ U := isoOfRangeEq (pullback.snd iV f) iU ⋯
⊢ e.inv ≫ pullback.snd iV f = iU ≫ 𝟙 X

Tactic:
simp [e]

Goal state after: