mathlib-initiative/mathlib-tactics huggingface dataset:
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) ◃ x = x ◃ y

Tactic:
rw [h, ← Shelf.self_distrib, act_one]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
x : G
⊢ ((lift k G A) F) ((of k G) x) = F x

Tactic:
of_apply,

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
x : G
⊢ ((lift k G A) F) (single x 1) = F x
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel.refl
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
a b x✝¹ y✝ : R
hab : Rel r x✝¹ y✝
c d x✝ : R
⊢ Relation.EqvGen (Rel r) (y✝ * x✝) (y✝ * x✝)

Tactic:
exact Relation.EqvGen.refl _

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl.refl
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
a b x✝¹ c d x✝ : R
⊢ Relation.EqvGen (Rel r) (x✝¹ * x✝) (x✝¹ * x✝)

Tactic:
exact Relation.EqvGen.refl _

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel.refl
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
a b x✝¹ y✝ : R
hab : Rel r x✝¹ y✝
c d x✝ : R
⊢ Relation.EqvGen (Rel r) (y✝ + x✝) (y✝ + x✝)

Tactic:
exact Relation.EqvGen.refl _

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl.refl
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
a b x✝¹ c d x✝ : R
⊢ Relation.EqvGen (Rel r) (x✝¹ + x✝) (x✝¹ + x✝)

Tactic:
exact Relation.EqvGen.refl _

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
x : G
lx : IsLeftRegular x
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
y : G
hy : y ∈ image (fun x_1 ↦ x * x_1) f.support
⊢ ∃ a ∈ f.support, x * a = y

Tactic:
simpa only [Finset.mem_image, exists_prop] using hy

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
x : G
rx : IsRightRegular x
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
y : G
hy : y ∈ image (fun x_1 ↦ x_1 * x) f.support
⊢ ∃ a ∈ f.support, a * x = y

Tactic:
simpa only [Finset.mem_image, exists_prop] using hy

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x y : R
w : r x y
⊢ (mkRingHom r) x = (mkRingHom r) y

Tactic:
by
  simp [mkRingHom_def, Quot.sound (Rel.of w)]

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

Goal state before:
pp: A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = ↑S
x : R
hx : x ∈ s
⊢ star x ∈ (S.copy s hs).carrier

Tactic:
change star x ∈ s

Goal state after:
A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = ↑S
x : R
hx : x ∈ s
⊢ star x ∈ s
Module: Mathlib.Algebra.Star.Subsemiring

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
H : 1 = 0
⊢ support 0 = ∅

Tactic:
support_zero

Goal state after:
R : Type u_1
inst✝ : Semiring R
H : 1 = 0
⊢ ∅ = ∅
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f g : ℕ → R → S
⊢ p.sum (f + g) = p.sum f + p.sum g

Tactic:
by
  simp [sum_def, Finset.sum_add_distrib]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
⊢ StarModule 𝕜 R

Tactic:
by
  let := e.star
  let := e.smul 𝕜
  apply e.injective.starModule _ 𝕜 <;> (intros; exact e.apply_symm_apply _)

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

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
u : ↥(unitary R)
x✝ : R
⊢ ↑u * star x✝ * ↑u⁻¹ = star (↑u * x✝ * ↑u⁻¹)

Tactic:
simp [mul_assoc, ← Unitary.star_eq_inv]

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

Goal state before:
pp: case pos
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), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : y ∈ f.support
⊢ f.coeff y * y • r = f.coeff y * y • r

Tactic:
simp [support] at h

Goal state after:
case pos
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), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : ¬f.coeff y = 0
⊢ f.coeff y * y • r = f.coeff y * y • r
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case neg
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), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : y ∉ f.support
⊢ 0 = f.coeff y * y • r

Tactic:
simp [support] at h

Goal state after:
case neg
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), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : f.coeff y = 0
⊢ 0 = f.coeff y * y • r
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case pos
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
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : z ∈ f.support
⊢ r * x • f.coeff z = r * x • f.coeff z

Tactic:
simp [support] at h

Goal state after:
case pos
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
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : ¬f.coeff z = 0
⊢ r * x • f.coeff z = r * x • f.coeff z
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case neg
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
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : z ∉ f.support
⊢ 0 = r * x • f.coeff z

Tactic:
simp [support] at h

Goal state after:
case neg
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
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : f.coeff z = 0
⊢ 0 = r * x • f.coeff z
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
r : k
⊢ r • (of k G) g = single g r

Tactic:
of_apply,

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
r : k
⊢ r • single g 1 = single g r
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : Nontrivial k
a b : G
h : (of k G) a = (of k G) b
⊢ a = b

Tactic:
of_apply,

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : Nontrivial k
a b : G
h : single a 1 = single b 1
⊢ a = b
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
F : J ⥤ PresheafedSpace C
j : J
U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ
⊢ ((opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))
            (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
          ((pushforward C (colimit.ι (F ⋙ forget C) j)).map (F.map (𝟙 j)).c ≫
              (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf).inv ≫
                (pushforwardEq ⋯ (F.obj j).presheaf).hom).op).app
      U =
    ((opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))
            (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
          (𝟙 (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))).app
      U

Tactic:
induction U with

Goal state after:
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
inst✝ : IsIso α
x : ↑↑X
⊢ ∃ inv,
    Hom.stalkMap α x ≫ inv = 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x)) ∧
      inv ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)

Tactic:
let β : Y ⟶ X := CategoryTheory.inv α
    have h_eq : (α ≫ β).base x = x := by rw [IsIso.hom_inv_id α, id_base, TopCat.id_app]
    -- Intuitively, the inverse of the stalk map of `α` at `x` should just be the stalk map of `β`
    -- at `α x`. Unfortunately, we have a problem with dependent type theory here: Because `x`
    -- is not *definitionally* equal to `β (α x)`, the map `stalk_map β (α x)` has not the correct
    -- type for an inverse.
    -- To get a proper inverse, we need to compose with the `eqToHom` arrow
    -- `X.stalk x ⟶ X.stalk ((α ≫ β).base x)`.
    refine
      ⟨eqToHom (show X.presheaf.stalk x = X.presheaf.stalk ((α ≫ β).base x) by rw [h_eq]) ≫
          (β.stalkMap (α.base x) :),
        ?_, ?_⟩
    · rw [← Category.assoc, congr_point α x ((α ≫ β).base x) h_eq.symm, Category.assoc]
      erw [← stalkMap.comp β α (α.base x)]
      rw [congr_hom _ _ (IsIso.inv_hom_id α), stalkMap.id, eqToHom_trans_assoc, eqToHom_refl,
        Category.id_comp]
    · rw [Category.assoc, ← stalkMap.comp, congr_hom _ _ (IsIso.hom_inv_id α), stalkMap.id,
        eqToHom_trans_assoc, eqToHom_refl, Category.id_comp]

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

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

Tactic:
induction U with

Goal state after:
case app.op
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : Opens ↑↑(Y.restrict ⋯)
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op U)))) = op U
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case h
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'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = toLRSHom'✝.c

Tactic:
· exact TopCat.Presheaf.ext (fun U ↦ by simpa using! h_app U)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
⊢ U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop U)))

Tactic:
induction U with

Goal state after:
case op
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : Opens ↑↑Y
⊢ op U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op U))))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp h')

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.univ
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
⊢ f ''ᵁ f ⁻¹ᵁ U = opensRange f ⊓ U

Tactic:
by
  apply Opens.ext
  simp [Set.image_preimage_eq_range_inter]

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

Goal state before:
pp: case h
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
a : ↑(pullback f.base g.base)
ha : (ConcreteCategory.hom (pullback.fst f.base g.base)) a = x
⊢ (ConcreteCategory.hom
        ((PreservesPullback.iso forgetToTop f g).inv ≫
          (PreservesPullback.iso forgetToTop f g).hom ≫ pullback.fst (forgetToTop.map f) (forgetToTop.map g)))
      a =
    x

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
case h
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
a : ↑(pullback f.base g.base)
ha : (ConcreteCategory.hom (pullback.fst f.base g.base)) a = x
⊢ (ConcreteCategory.hom (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) a = x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.snd.c.app x

Tactic:
· change (_ ≫ _ ≫ _) ≫ _ = _
    simp_rw [Category.assoc]
    erw [s.snd.c.naturality_assoc]
    erw [← s.pt.presheaf.map_comp, ← s.pt.presheaf.map_comp]
    trans s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 _)
    · congr 1
    · simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop f g).hom)

Tactic:
rw [← TopCat.epi_iff_surjective]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop f g).hom
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop g f).hom)

Tactic:
rw [← TopCat.epi_iff_surjective]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop g f).hom
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
x : ↥X
r : ↑⋯.choose
⊢ Set.range ⇑(X.affineBasisCover.f ⟨x, r⟩) = ⇑(X.affineCover.f x) '' (PrimeSpectrum.basicOpen r).carrier

Tactic:
simp only [affineBasisCover, Precoverage.ZeroHypercover.bind_toPreZeroHypercover, Set.range_comp,
    PreZeroHypercover.bind_f, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp]

Goal state after:
X : Scheme
x : ↥X
r : ↑⋯.choose
⊢ ⇑(TopCat.Hom.hom (X.affineCover.f x).base) ''
      Set.range ⇑(TopCat.Hom.hom ((affineBasisCoverOfAffine (Classical.choose ⋯)).f r).base) =
    (fun a ↦ (X.affineCover.f x) a) '' (PrimeSpectrum.basicOpen r).carrier
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : U ≤ U'
⊢ resLE f U V e ≫ Y.homOfLE i = resLE f U' V ⋯

Tactic:
by
  simp_rw [← resLE_id, resLE_comp_resLE, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : Scheme.Spec.essImage Y
⊢ Scheme.Spec.essImage X

Tactic:
exact Functor.essImage.ofIso (asIso f).symm h

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app hU.fromSpec U =
    (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ Scheme.Hom.app hU.fromSpec U

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app hU.fromSpec U = Scheme.Hom.app hU.fromSpec U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ f = g

Tactic:
← IsOpenImmersion.lift_fac U.ι f (by simpa [Set.range_subset_iff] using fun x hx ↦ hUf.ge hx),

Goal state after:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ IsOpenImmersion.lift U.ι f ⋯ ≫ U.ι = g
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ X.zeroLocus ↑(⨅ i ∈ t, I i) = ⋃ i ∈ t, X.zeroLocus ↑(I i)

Tactic:
zeroLocus_biInf I ht,

Goal state after:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ = ⋃ i ∈ t, X.zeroLocus ↑(I i)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
⊢ IsColimit (coequalizerCofork f g)

Tactic:
by
  refine Cofork.IsColimit.mk' _ (fun s ↦ ?_)
  have e : f.toShHom ≫ s.π.toShHom = g.toShHom ≫ s.π.toShHom := by
    simp only [← comp_toShHom, s.condition]
  refine ⟨⟨(coequalizer.desc s.π.toShHom e).hom, fun x ↦ ?_⟩,
    ⟨Hom.ext' (Functor.congr_map SheafedSpace.forgetToPresheafedSpace
      (coequalizer.π_desc (Hom.toShHom s.π) e)),
      fun {m} hm ↦ LocallyRingedSpace.forgetToSheafedSpace.map_injective
        (coequalizer.hom_ext ((LocallyRingedSpace.forgetToSheafedSpace.congr_map hm).trans
      ((coequalizer.π_desc _ _).symm)))⟩⟩
  rcases (TopCat.epi_iff_surjective
    (coequalizer.π f.toShHom g.toShHom).hom.base).mp inferInstance x with ⟨y, rfl⟩
  -- Porting note: was `apply isLocalHom_of_comp _ (PresheafedSpace.stalkMap ...)`, this
  -- used to allow you to provide the proof that `... ≫ ...` is a local ring homomorphism later,
  -- but this is no longer possible
  set h := _
  change IsLocalHom h
  suffices _ : IsLocalHom (((coequalizerCofork f g).π.1.stalkMap _).hom.comp h) by
    apply isLocalHom_of_comp _ ((coequalizerCofork f g).π.1.stalkMap _).hom
  rw [← CommRingCat.hom_ofHom h, ← CommRingCat.hom_comp]
  erw [← PresheafedSpace.stalkMap.comp]
  apply isLocalHom_stalkMap_congr _ _ (coequalizer.π_desc s.π.toShHom e).symm y
  change IsLocalHom (s.π.stalkMap y).hom
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryFan X 0
m : s.pt ⟶ X
h₁ : m ≫ 𝟙 X = s.fst
x✝ : m ≫ 0 = s.snd
⊢ m = s.fst

Tactic:
simpa using h₁

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryCofan X 0
m : X ⟶ s.pt
h₁ : 𝟙 X ≫ m = s.inl
x✝ : 0 ≫ m = s.inr
⊢ m = s.inl

Tactic:
simpa using h₁

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ (((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData LocallyRingedSpace.forgetToSheafedSpace).ι i ≫
            D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv).hom.base ≫
      (LocallyRingedSpace.forgetToSheafedSpace.map D.isoLocallyRingedSpace.inv).hom.base =
    (D.ι i).base

Tactic:
D.toLocallyRingedSpaceGlueData.ι_isoSheafedSpace_inv i,

Goal state after:
D : GlueData
i : D.J
⊢ (LocallyRingedSpace.Hom.toShHom (D.toLocallyRingedSpaceGlueData.ι i)).hom.base ≫
      (LocallyRingedSpace.forgetToSheafedSpace.map D.isoLocallyRingedSpace.inv).hom.base =
    (D.ι i).base
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom)

Tactic:
rw [← TopCat.epi_iff_surjective]

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ Epi (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom