mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toAdd.add x y) h

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

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toAdd.add x y) h

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

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toAdd.add x y) h

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

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toAdd.add x y) h

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

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toAdd.add x y) h

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

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toAdd.add x y) h

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

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toAdd.add x y) h

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

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toAdd.add x y) h

Goal state after:
case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ AddMonoid.End.mulRight a = L a ∧ L a ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑AddMonoid.End.mulRight) ↔
    ∀ (b : α), Commute (L b) (L a)

Tactic:
Subsemiring.mem_centralizer_iff,

Goal state after:
α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ (AddMonoid.End.mulRight a = L a ∧ ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑AddMonoid.End.mulRight, g * L a = L a * g) ↔
    ∀ (b : α), Commute (L b) (L 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✝ : NonAssocSemiring α
T : CentroidHom α
⊢ T 1 ∈ Subsemiring.center α

Tactic:
by constructor <;> simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ T 1 ∈ StarSubsemiring.center α

Tactic:
by constructor <;> simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
⊢ (v.sum fun a ↦ single (f a)).coeff = Finsupp.mapDomain f v.coeff

Tactic:
Finsupp.mapDomain,

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
⊢ (v.sum fun a ↦ single (f a)).coeff = v.coeff.sum fun a ↦ Finsupp.single (f a)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case single.single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
h : SkewMonoidAlgebra k G
x : G
a : k
y : G
b : k
⊢ single x a * single y b * h = single x a * (single y b * h)

Tactic:
| single y b =>

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

Goal state before:
pp: case e_g.e_g
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x x✝³ : G
x✝² : k
x✝¹ : G
x✝ : k
⊢ (single (x✝³ * x✝¹) (x✝² * x✝³ • x✝)).coeff x = if x✝³ * x✝¹ = x then x✝² * x✝³ • x✝ else 0

Tactic:
exact coeff_single_apply

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ 0 * x✝ = 0

Tactic:
rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero,
        mul_zero, sym_zero]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ x✝ * 0 = 0

Tactic:
rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero,
        mul_zero, sym_zero]

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

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁴ : Semiring β
inst✝³ : Monoid α
inst✝² : Monoid α₂
inst✝¹ : FunLike F α α₂
inst✝ : MonoidHomClass F α α₂
f : F
⊢ (mapDomain ⇑f) (single 1 1) = single 1 1

Tactic:
mapDomain_single,

Goal state after:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁴ : Semiring β
inst✝³ : Monoid α
inst✝² : Monoid α₂
inst✝¹ : FunLike F α α₂
inst✝ : MonoidHomClass F α α₂
f : F
⊢ single (f 1) 1 = single 1 1
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ (x.sum fun a b ↦ y.sum fun a₂ b₂ ↦ (mapDomain ⇑f) (single (a * a₂) (b * a • b₂))) =
    ((mapDomain ⇑f) x).sum fun a₁ b₁ ↦ ((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)

Tactic:
mapDomain_single,

Goal state after:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ (x.sum fun a b ↦ y.sum fun a₂ b₂ ↦ single (f (a * a₂)) (b * a • b₂)) =
    ((mapDomain ⇑f) x).sum fun a₁ b₁ ↦ ((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)
Module: Mathlib.Algebra.Tropical.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddAbove s
this : Set.range untrop = Set.univ
⊢ ¬BddAbove (untrop '' s)

Tactic:
contrapose hs

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddAbove (untrop '' s)
⊢ BddAbove s
Module: Mathlib.Algebra.Tropical.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ ¬BddBelow (untrop '' s)

Tactic:
contrapose hs

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddBelow (untrop '' s)
⊢ BddBelow 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.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)

Tactic:
erw [← PresheafedSpace.stalkMap_germ_apply ⟨f, fc⟩, ← PresheafedSpace.stalkMap_germ_apply ⟨f, gc⟩]

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 ({ base := f, c := fc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := fc }.base) x) hx))
        s) =
    (ConcreteCategory.hom ({ base := f, c := gc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := gc }.base) x) hx))
        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 : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
e : { hom := { base := g, c := gc } } ≫ f = { hom := { base := g, c := hc } } ≫ f
x : ↑↑Z.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap f.hom ((ConcreteCategory.hom g) x) ≫
      PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom x =
    PresheafedSpace.Hom.stalkMap f.hom ((ConcreteCategory.hom g) x) ≫
      𝟙 (X.presheaf.stalk ((ConcreteCategory.hom { hom := { base := g, c := hc } }.hom.base) x)) ≫
        PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom x

Tactic:
Category.id_comp,

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 hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
e : { hom := { base := g, c := gc } } ≫ f = { hom := { base := g, c := hc } } ≫ f
x : ↑↑Z.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap f.hom ((ConcreteCategory.hom g) x) ≫
      PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom x =
    PresheafedSpace.Hom.stalkMap f.hom ((ConcreteCategory.hom g) x) ≫
      PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom x
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 : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom ((ConcreteCategory.hom f.hom.base) ⋯.choose) ≫
      PresheafedSpace.Hom.stalkMap f.hom ⋯.choose =
    (𝟙
          (Z.presheaf.stalk
            ((ConcreteCategory.hom { hom := { base := g, c := hc } }.hom.base)
              ((ConcreteCategory.hom f.hom.base) ⋯.choose))) ≫
        PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom
          ((ConcreteCategory.hom f.hom.base) ⋯.choose)) ≫
      PresheafedSpace.Hom.stalkMap f.hom ⋯.choose

Tactic:
Category.id_comp,

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 hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom ((ConcreteCategory.hom f.hom.base) ⋯.choose) ≫
      PresheafedSpace.Hom.stalkMap f.hom ⋯.choose =
    PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom ((ConcreteCategory.hom f.hom.base) ⋯.choose) ≫
      PresheafedSpace.Hom.stalkMap f.hom ⋯.choose
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this :
  X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (𝟙 U))) f) =
    unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)

Tactic:
X.presheaf.map_id,

Goal state after:
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this :
  X.basicOpen ((ConcreteCategory.hom (𝟙 (X.presheaf.obj U))) f) =
    unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g

Tactic:
by
  ext x
  by_cases hx : x ∈ U
  · simp [mem_basicOpen (hx := hx)]
  · simp [mt (basicOpen_le X _ ·) hx]

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

Goal state before:
pp: case app
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 : Jᵒᵖ
x : ↑((F ⋙ forget C).obj (unop X))
⊢ colimit.ι (F ⋙ forget C) (unop X) ≫
      (colimit.isoColimitCocone
              {
                cocone :=
                  {
                    pt :=
                      { carrier := Limits.colimit (F ⋙ forget C),
                        presheaf := limit (pushforwardDiagramToColimit F).leftOp },
                    ι :=
                      {
                        app := fun j ↦
                          { base := colimit.ι (F ⋙ forget C) j,
                            c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) },
                        naturality := ⋯ } },
                isColimit := colimitCoconeIsColimit F }).symm.hom.base =
    (colimit.ι F (unop X)).base

Tactic:
exact ι_preservesColimitIso_inv (forget C) F (unop X)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            (homOfLE hrU).op))
        s) =
    y
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
set s' := (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).map
      (homOfLE hrU).op s with h

Goal state after:
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            (homOfLE hrU).op))
        s) =
    y
s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
        (structureSheaf ↑S).obj).obj
    (op (PrimeSpectrum.basicOpen r))) :=
  (ConcreteCategory.hom
      (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
            (structureSheaf ↑S).obj).map
        (homOfLE hrU).op))
    s
h :
  s' =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      s
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))

Tactic:
X.presheaf.map_id,

Goal state after:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Scheme.Spec.map (𝟙 Γ(X, U)).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ IsIso f

Tactic:
by
  rw [isIso_iff_isOpenImmersion_and_epi_base]
  refine ⟨inferInstance, ?_⟩
  rw [TopCat.epi_iff_surjective, ← Set.range_eq_univ]
  exact TopologicalSpace.Opens.ext_iff.mp hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations A ↑x
ha : a ∈ (sectionsSubmodule A U).carrier
hb : b ∈ (sectionsSubmodule A U).carrier
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R A).pred fun x ↦ (a * b) (i x)

Tactic:
obtain ⟨Va, ma, ia, ra, sa, wa⟩ := ha x
    obtain ⟨Vb, mb, ib, rb, sb, wb⟩ := hb x
    refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ra * rb, sa * sb, fun x ↦ ?_⟩
    obtain ⟨hsax, hsa⟩ := wa ⟨x.1, x.2.1⟩
    obtain ⟨hsbx, hsb⟩ := wb ⟨x.1, x.2.2⟩
    exact ⟨x.1.asIdeal.primeCompl.mul_mem hsax hsbx,
      congr($hsa * $hsb).trans (LocalizedModule.mk_mul_mk ..)⟩

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
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen f
x : ↥(unop (op U))
⊢ ↑(const 0 f U hu) x = ↑0 x

Tactic:
by simp; rfl

Goal state after: