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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
h₁ : P.nextCoeff ≠ 0
this : P.signVariations = P.eraseLead.signVariations + 1
⊢ ((X - C η) * P).eraseLead.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
suffices SignType.sign ((X - C η) * P).nextCoeff = -1 by
        simp +decide [signVariations_eq_eraseLead_add_ite h_mul, h_lC,
          leadingCoeff_eraseLead_eq_nextCoeff, ← sign_eq_zero_iff, this]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
h₁ : P.nextCoeff ≠ 0
this : P.signVariations = P.eraseLead.signVariations + 1
⊢ SignType.sign ((X - C η) * P).nextCoeff = -1
Module: Mathlib.Algebra.Quandle

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

Tactic:
by
  rw [self_distrib, self_distrib, act_act_self_eq, act_self_act_eq]

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k

Tactic:
← i_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.i = -c₁ • q.j

Tactic:
← i_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.j * q.i = -c₁ • q.j
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.j = c₃ • q.i

Tactic:
← i_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.j * q.j = c₃ • q.i
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.j * q.k = (c₂ * c₃) • 1 - c₃ • q.i

Tactic:
← i_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.j * (q.i * q.j) = (c₂ * c₃) • 1 - c₃ • q.i
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.k = -((c₁ * c₃) • 1)

Tactic:
← i_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.j * (q.i * q.j) = -((c₁ * c₃) • 1)
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * ((c₂ • q.j - q.k) * q.j) = -((c₁ * c₃) • 1)

Tactic:
← i_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * ((c₂ • q.j - q.i * q.j) * q.j) = -((c₁ * c₃) • 1)
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case a.inr.inl
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ B.j ∈ ↑B.liftHom.range

Tactic:
use (Basis.self R).j

Goal state after:
case h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ B.liftHom.toRingHom (Basis.self R).j = B.j
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
⊢ f.update a 0 = (erase a) f

Tactic:
ext; simp [coeff_erase_apply, Finsupp.erase_apply, Function.update_apply]

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

Goal state before:
pp: ⊢ (√2)⁻¹ * (√2)⁻¹ = 2⁻¹

Tactic:
rw [← mul_inv]
  simp

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
s : S
a : G
b : k
⊢ (s • single a b).coeff = (single a (s • b)).coeff

Tactic:
by simp;

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
R : Type u_5
inst✝¹ : Monoid R
inst✝ : DistribMulAction R k
b : R
⊢ (mapDomain f) (b • v) = b • (mapDomain f) v

Tactic:
simp_rw [← coeff_inj, coeff_smul, coeff_mapDomain]
  simp [Finsupp.mapDomain_smul]

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

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

Tactic:
induction g with

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (Presheaf.pushforward C (X.ofRestrict ⋯).base).obj (X.restrict ⋯).presheaf

Tactic:
by
          rw [restrict_top_presheaf, ← Presheaf.Pushforward.comp_eq]
          tauto

Goal state after:
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
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (colimitPresheafObjIsoComponentwiseLimit F U).hom ≫ limit.π (componentwiseDiagram F U) (op j) =
    (colimit.ι F j).c.app (op U)

Tactic:
← Iso.eq_inv_comp,

Goal state after:
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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limit.π (componentwiseDiagram F U) (op j) =
    (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U V' ⋯)

Tactic:
subst e₂

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U V ⋯)
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔
    (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (forget.map (f i)))) ∧ ∀ (i : ι), P (f i)

Tactic:
← Scheme.forget_obj,

Goal state after:
P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔
    (∀ (x : forget.obj S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (forget.map (f i)))) ∧ ∀ (i : ι), P (f i)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ lift g f ⋯ ≫ lift f g ⋯ = 𝟙 X

Tactic:
rw [← cancel_mono f]; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ lift g f ⋯ ≫ lift f g ⋯ = 𝟙 X

Tactic:
rw [← cancel_mono f]; simp

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

Goal state before:
pp: X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h : ∀ (i : 𝒰.I₀), IsNilpotent ((ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s)
⊢ IsNilpotent s

Tactic:
by
  choose fn hfn using h
  have : Fintype 𝒰.I₀ := Fintype.ofFinite 𝒰.I₀
  /- the maximum of all `fn i` (exists, because `𝒰.I₀` is finite) -/
  let N : ℕ := Finset.sup Finset.univ fn
  have hfnleN (i : 𝒰.I₀) : fn i ≤ N := Finset.le_sup (Finset.mem_univ i)
  use N
  apply zero_of_zero_cover (𝒰 := 𝒰)
  on_goal 1 => intro i; simp only [map_pow]
  -- This closes both remaining goals at once.
  exact pow_eq_zero_of_le (hfnleN i) (hfn i)

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

Goal state before:
pp: case h_open
X : Scheme
⊢ ∀ u ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}, IsOpen u

Tactic:
rintro _ ⟨a, rfl⟩
    exact IsOpenImmersion.isOpen_range (X.affineBasisCover.f a)

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : ?m.34 := ?m.35
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        ((F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).toLocalizationPresheaf.app U))

Tactic:
change Function.Injective (algebraMap _ (Localization m))

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
⊢ Function.Injective ⇑(algebraMap (↑(F.presheaf.obj U)) (Localization m))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ pullback.fst (f ≫ g) (Scheme.Opens.ι U) ≫ f =
    (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.fst f (g ⁻¹ᵁ U).ι ≫ f

Tactic:
pullbackRestrictIsoRestrict_inv_fst_assoc,

Goal state after:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.fst f (g ⁻¹ᵁ U).ι ≫ f
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V' ⋯)

Tactic:
subst e₂

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V ⋯)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
⊢ resLE f U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ f ⁻¹ᵁ U.ι ''ᵁ O

Tactic:
by
  rw [← comp_preimage, ← resLE_comp_ι f e, comp_preimage, preimage_image_eq]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (U.stalkIso ((resLE f U V e) x)).hom ≫ Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x =
    stalkMap (resLE f U V e) x ≫ (V.stalkIso x).hom

Tactic:
← Iso.eq_inv_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x =
    (U.stalkIso ((resLE f U V e) x)).inv ≫ stalkMap (resLE f U V e) x ≫ (V.stalkIso x).hom
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
⊢ f = g

Tactic:
← cancel_mono Y.toSpecΓ,

Goal state after:
X Y : Scheme
inst✝ : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
⊢ f ≫ Y.toSpecΓ = g ≫ Y.toSpecΓ
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
he : t * (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
t' : ?m.85 := ?m.86
⊢ IsUnit t

Tactic:
change t * t' = _ at he

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit t
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : P.IsLocalAtSource K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f

Tactic:
rw [IsLocalAtSource.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]
  simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
⊢ ∀ {X Y : WalkingMultispan (MultispanShape.prod D.J)} (f : X ⟶ Y),
    (D.diagram.multispan ⋙ F).map f ≫
        (match Y with
          | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
      (match X with
          | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
        (D.mapGlueData F).diagram.multispan.map f

Tactic:
by
      rintro (⟨_, _⟩ | _) _ (_ | _ | _) <;> simp

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    ⇑(ConcreteCategory.hom (D.t i j)) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)) ⁻¹' U

pp: case hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t i j))

Tactic:
Set.preimage_preimage

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    (fun x ↦
        (⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)))
          ((ConcreteCategory.hom (D.t i j)) x)) ⁻¹'
      U

case hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t i j))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
      ofHom
          {
            toFun := fun x ↦
              ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
            continuous_toFun := ⋯ } ≫
        pullbackSnd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j

Tactic:
← Iso.eq_inv_comp,

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
⊢ ofHom
        {
          toFun := fun x ↦
            ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      pullbackSnd (h.V j k).inclusion' (h.V j i).inclusion' =
    (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').inv ≫
      pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
      ofHom
          {
            toFun := fun x ↦
              ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
            continuous_toFun := ⋯ } ≫
        ofHom
            {
              toFun := fun x ↦
                ⟨(⟨↑((ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩,
              continuous_toFun := ⋯ } ≫
          ofHom
            {
              toFun := fun x ↦
                ⟨(⟨↑((ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩,
              continuous_toFun := ⋯ } =
    (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom

Tactic:
← Iso.eq_inv_comp,

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
⊢ ofHom
        {
          toFun := fun x ↦
            ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      ofHom
          {
            toFun := fun x ↦
              ⟨(⟨↑((ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩,
            continuous_toFun := ⋯ } ≫
        ofHom
          {
            toFun := fun x ↦
              ⟨(⟨↑((ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩,
            continuous_toFun := ⋯ } =
    (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').inv ≫
      (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case right.right
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ x ∈ ⇑(fromGlued 𝒰) '' U ∩ Set.range ⇑(𝒰.f (idx 𝒰 x))

Tactic:
exact ⟨hx, 𝒰.covers x⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι := ⋯
this : IsOpenImmersion α
⊢ (V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) (α z)) = (V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) x)

Tactic:
rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.lift_fst_assoc]

Goal state after:
J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)
    ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ⋯
this : IsOpenImmersion α
⊢ (((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ≫ (V F i j).ι) z =
    (V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) x)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X ⊕ ↥Y
⊢ (coprodMk X Y) x ∈
    Set.range
      ⇑({ I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
              f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.f
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) ((coprodMk X Y).symm ((coprodMk X Y) x))))

Tactic:
simp only [Sum.elim_inl, Sum.elim_inr, Set.mem_range]

Goal state after:
case h
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X ⊕ ↥Y
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) ((coprodMk X Y).symm ((coprodMk X Y) x))))
        y =
      (coprodMk X Y) x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ⇑(ConcreteCategory.hom (D.f j k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j).base) ⁻¹' ↑(⋯.functor.obj U) =
    ⇑(ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.left (j, k))).base) ⁻¹' ↑(⋯.functor.obj U)

Tactic:
Set.preimage_preimage

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (fun x ↦ (ConcreteCategory.hom (D.ι j).base) ((ConcreteCategory.hom (D.f j k).base) x)) ⁻¹' ↑(⋯.functor.obj U) =
    ⇑(ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.left (j, k))).base) ⁻¹' ↑(⋯.functor.obj U)