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

Goal state before:
pp: case zero
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
x✝ : RingQuot r
a✝ : Quot (Rel r)
a b : R
h : Rel r a b
⊢ Quot.mk (Rel r) (a ^ 0) = Quot.mk (Rel r) (b ^ 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_3
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 uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (x y : B),
    x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
      y ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
        (mkRingHom r) x = 0 → (mkRingHom r) y = 0 → (mkRingHom r) (x + y) = 0

Tactic:
intro a

Goal state after:
case refine_3
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 uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a : B
⊢ ∀ (y : B),
    a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
      y ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
        (mkRingHom r) a = 0 → (mkRingHom r) y = 0 → (mkRingHom r) (a + y) = 0
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_4
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 uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (a x : B), x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} → (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0

Tactic:
intro a

Goal state after:
case refine_4
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 uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a : B
⊢ ∀ x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}, (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0
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
⊢ Quot.lift ⇑f ⋯ (toQuot 1) = 1

Tactic:
simp only [← one_quot, map_one]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a : R
⊢ (⇑φ)^[0] a = ofAdd 0 • a

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n i : ℕ
⊢ (erase n p).coeff i = if i = n then 0 else p.coeff i

Tactic:
by
  exact ite_congr rfl (fun _ ↦ rfl) (fun _ ↦ rfl)

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
⊢ a • 0 = 0

Tactic:
by exact congr_arg ofCoeff (smul_zero a)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) a * (liftNC ↑f ⇑g) b

Tactic:
conv_rhs => rw [← sum_single a, ← sum_single b]
  simp_rw [mul_def, map_sum, liftNC_single, sum_mul, mul_sum]
  refine sum_congr fun y hy ↦ sum_congr fun x _hx ↦ ?_
  simp only [AddMonoidHom.coe_coe, map_mul]
  rw [mul_assoc, ← mul_assoc (f (y • b.coeff x)), h_comm hy, mul_assoc, mul_assoc]

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (conjStarAlgAut S R) v = (conjStarAlgAut S R) u ↔ ∃ α, ↑u = α • ↑v

Tactic:
simp_rw [StarAlgEquiv.ext_iff, conjStarAlgAut_apply, ← coe_star, star_eq_inv,
    ← val_inv_toUnits_apply, ← val_toUnits_apply, mul_assoc, ← Units.eq_inv_mul_iff_mul_eq,
    ← mul_assoc, Units.eq_mul_inv_iff_mul_eq, mul_assoc, ← mul_assoc (((toUnits v)⁻¹ : Rˣ) : R),
    ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot, Algebra.mem_bot,
    Set.mem_range, Algebra.algebraMap_eq_smul_one, Units.eq_inv_mul_iff_mul_eq, mul_smul_comm,
    mul_one, eq_comm]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : FaithfulSMul S k
inst✝ : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
⊢ ∀ (a : G →₀ k), { coeff := _s₁ • a } = { coeff := _s₂ • a }

Tactic:
intro a

Goal state after:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : FaithfulSMul S k
inst✝ : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
a : G →₀ k
⊢ { coeff := _s₁ • a } = { coeff := _s₂ • a }
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
⊢ (0 + 1) • x = x

Tactic:
| zero =>

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

Goal state before:
pp: k : Type u_1
G : Type u_2
A : Type u_6
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
inst✝ : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1)
⊢ ∀ (a : G), (↑φ₁).comp (DistribMulActionHom.single a) = (↑φ₂).comp (DistribMulActionHom.single a)

Tactic:
intro a

Goal state after:
k : Type u_1
G : Type u_2
A : Type u_6
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
inst✝ : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1)
a : G
⊢ (↑φ₁).comp (DistribMulActionHom.single a) = (↑φ₂).comp (DistribMulActionHom.single a)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * (ConcreteCategory.hom (X.presheaf.germ V x hxV)) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Tactic:
replace heq : (X.presheaf.germ _ x hxW) ((X.presheaf.map (U.infLELeft V).op) f *
      (X.presheaf.map (U.infLERight V).op) g) = (X.presheaf.germ _ x hxW) 1 := by
    rwa [map_mul, map_one, X.presheaf.germ_res_apply (Opens.infLELeft U V) x hxW f,
      X.presheaf.germ_res_apply (Opens.infLERight U V) x hxW g]

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (f.inv ≫ f.hom).hom = 𝟙 Y.toPresheafedSpace

Tactic:
f.inv_hom_id,

Goal state after:
X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (𝟙 Y.toSheafedSpace).hom = 𝟙 Y.toPresheafedSpace
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
⊢ e.hom.base ≫ e.inv.base = 𝟙 ↑X.toPresheafedSpace

Tactic:
by
  simp only [← comp_base, Iso.hom_inv_id, id_toHom, PresheafedSpace.id_base]

Goal state after:
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)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f) ≤ X.basicOpen f

Tactic:
rw [X.basicOpen_res i f]; exact inf_le_right

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

Goal state before:
pp: case zero
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : 0 < 0 + Nat.succ 0
⊢ X.basicOpen (f ^ (0 + Nat.succ 0)) = X.basicOpen f

Tactic:
| zero =>

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toStalk (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) ≫
      PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p =
    f ≫ toStalk (↑S) p

Tactic:
rw [← algebraMap_germ ⊤ p trivial, ← algebraMap_germ ⊤ (PrimeSpectrum.comap f.hom p) trivial,
    Category.assoc]

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat ↑R).germ ⊤ (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) trivial ≫
        PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: S T : Type u_1
f : S ⟶ T
hf : IsIso f
x : T
⊢ ∃ Y g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
use S, f, ⟨⟩

Goal state after:
case right
S T : Type u_1
f : S ⟶ T
hf : IsIso f
x : T
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f)
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)ᵒᵖ
⊢ s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ eqToHom ⋯ ≫ (eqToHom ⋯).app x) =
    s.snd.c.app x

Tactic:
trans s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 _)

Goal state after:
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)ᵒᵖ
⊢ s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ eqToHom ⋯ ≫ (eqToHom ⋯).app x) =
    s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 ((Opens.map s.snd.base).op.obj x))

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)ᵒᵖ
⊢ s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 ((Opens.map s.snd.base).op.obj x)) = s.snd.c.app x
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
rw [← show _ = (pullback.fst g f).base from
    PreservesPullback.iso_hom_fst Scheme.forgetToTop g f, TopCat.coe_comp, Set.range_comp,
    Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.snd g.base f.base)]
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): was `rw`
  · erw [TopCat.pullback_fst_image_snd_preimage]
    rw [Set.image_univ]
    rfl
  rw [← TopCat.epi_iff_surjective]
  infer_instance

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

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ { I₀ := J, X := obj, f := map }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, ?_⟩
    · obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x
      obtain ⟨i, rfl⟩ := e₁.surjective i
      use i, (e₂ i).inv y
      simp [h]
    · simp_rw [h, MorphismProperty.cancel_left_of_respectsIso]
      intro i
      exact 𝒰.map_prop _

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
⊢ IsIso ((colimit.ι F i).hom.c.app (op (⋯.functor.obj U)))

Tactic:
have h₁ := ι_preservesColimitIso_inv SheafedSpace.forgetToPresheafedSpace F i

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
⊢ IsIso ((colimit.ι F i).hom.c.app (op (⋯.functor.obj U)))
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ ⊤ ≤ x.asIdeal

Tactic:
← hs,

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ Ideal.span (Set.range s) ≤ x.asIdeal
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE ⋯

Tactic:
rw [← cancel_mono W.ι, Category.assoc, Scheme.homOfLE_ι, Scheme.homOfLE_ι, Scheme.homOfLE_ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ≫
      (stalkFunctor CommRingCat ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x)).map
          X.toΓSpecSheafedSpace.hom.c ≫
        stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    X.presheaf.Γgerm x

Tactic:
← algebraMap_germ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),

Goal state after:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen 1)))) ≫
        (structurePresheafInCommRingCat ↑(Γ.obj (op X))).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ⋯) ≫
      (stalkFunctor CommRingCat ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x)).map
          X.toΓSpecSheafedSpace.hom.c ≫
        stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    X.presheaf.Γgerm x
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i)) →
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j))

Tactic:
· rintro ⟨x, hx⟩
    refine ⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), ?_⟩⟩
    rw [D.glue_condition_apply]
    exact hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec '' PrimeSpectrum.zeroLocus s = X.zeroLocus s ∩ ↑U

Tactic:
rw [← hU.fromSpec_preimage_zeroLocus, Set.image_preimage_eq_inter_range, range_fromSpec]

Goal state after:
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
⊢ X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ

Tactic:
refine ht.induction_on _ (by simp) fun {i t} hit ht IH ↦ ?_

Goal state after:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t✝ : Set ι
ht✝ : t✝.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH : X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ
⊢ X.zeroLocus ↑(⨅ i_1 ∈ insert i t, I i_1) = (⋃ i_1 ∈ insert i t, X.zeroLocus ↑(I i_1)) ∪ (↑U)ᶜ
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ pullback (h.V i j).inclusion' (h.V i k).inclusion' ⟶ pullback (h.V j k).inclusion' (h.V j i).inclusion'

Tactic:
refine (pullbackIsoProdSubtype _ _).hom ≫ ofHom ⟨?_, ?_⟩ ≫ (pullbackIsoProdSubtype _ _).inv

Goal state after:
case refine_1
D : GlueData
h : MkCore
i j k : h.J
⊢ { p // (ConcreteCategory.hom (h.V i j).inclusion') p.1 = (ConcreteCategory.hom (h.V i k).inclusion') p.2 } →
    { p // (ConcreteCategory.hom (h.V j k).inclusion') p.1 = (ConcreteCategory.hom (h.V j i).inclusion') p.2 }

case refine_2
D : GlueData
h : MkCore
i j k : h.J
⊢ Continuous ?refine_1
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (prodComparisonIso (pullback f) R S).inv ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.fst R.hom S.hom =
    pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.hom f

Tactic:
← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      Hom.left (prodComparisonIso (pullback f) R S).inv ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.fst R.hom S.hom =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.hom f
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (prodComparisonIso (pullback f) R S).inv ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.snd R.hom S.hom =
    pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst S.hom f

Tactic:
← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      Hom.left (prodComparisonIso (pullback f) R S).inv ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.snd R.hom S.hom =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst S.hom f
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (prodComparisonIso (pullback f) R S).inv ≫ pullback.snd (R ⊗ S).hom f =
    pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.snd S.hom f

Tactic:
← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      Hom.left (prodComparisonIso (pullback f) R S).inv ≫ pullback.snd (R ⊗ S).hom f =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.snd S.hom f
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j ≫ (D.gluedIso (forget C)).inv)) ⁻¹'
      ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv)) '' ↑U =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      ⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Tactic:
rw [TopCat.coe_comp, TopCat.coe_comp, Set.image_comp, Set.preimage_comp, Set.preimage_image_eq]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j)) ⁻¹'
      ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) '' ↑U =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      ⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
          invApp (pullback.snd (D.f j i) (D.f j k))
              ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (Opens.map (D.f j k).base).op.map (eqToHom ⋯).op) =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
simp_rw [← Category.assoc]
        erw [← comp_c_app, ← comp_c_app]
        · simp_rw [Category.assoc]
          dsimp only [Functor.op, unop_op, Quiver.Hom.unop_op]
          rw [eqToHom_map (Opens.map _), eqToHom_op, eqToHom_trans]
          congr

Goal state after: