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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
⊢ n < p.mirror.natTrailingDegree

Tactic:
by rwa [mirror_natTrailingDegree]

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
⊢ signVariations 0 = 0

Tactic:
by
  simp [signVariations]

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
have hr0 : r₂ i - r₁ i = 0 := (hg.1.not_dvd_of_degree_lt · hdr).mtr hgid

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_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.lift 0 = 0

Tactic:
by simp [lift]

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.lift 1 = 1

Tactic:
by simp [lift]

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
⊢ inst₁ = inst₂

Tactic:
have h_zero' : inst₁.toZero = inst₂.toZero := congrArg (·.toZero) h_monoid

Goal state after:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
⊢ ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)

Tactic:
have hgi (i : ι) (hi : i ∈ s) : (algebraMap R[X] K (g i))⁻¹ * algebraMap R[X] K (g i) = 1 :=
    inv_mul_cancel₀ (by simpa using (hg i hi).ne_zero)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
have hgi (i : ι) (hi : i ∈ s) : (algebraMap R[X] K (g i))⁻¹ * algebraMap R[X] K (g i) = 1 :=
    inv_mul_cancel₀ (by simpa using (hg i hi).ne_zero)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ (monomial m) a = (monomial n) b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

Tactic:
by
  rw [← Finsupp.single_eq_single_iff m n a b]
  simp only [monomial_def, ← coeff_single, coeff_inj]
  simp only [← ofCoeff_single, SkewMonoidAlgebra.ofCoeff_inj, Finsupp.single_eq_single_iff,
    EmbeddingLike.apply_eq_iff_eq]

Goal state after:
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:
← mem_toSubsemiring,

Goal state after:
R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
⊢ x ∈ S.toSubsemiring ↔ x ∈ T
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.toSubsemiring ↔ x ∈ T

Tactic:
← mem_toSubsemiring,

Goal state after:
R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
⊢ x ∈ S.toSubsemiring ↔ x ∈ T.toSubsemiring
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : CentroidHom α
x✝ : α
⊢ (star (star f)) x✝ = f x✝

Tactic:
by
    rw [star_apply, star_apply, star_star, star_star]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
r : R
⊢ starRingEquiv.toFun ((algebraMap R (FreeAlgebra R X)) r) = (algebraMap R (FreeAlgebra R X)ᵐᵒᵖ) r

Tactic:
by simp [star_algebraMap]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym (b + c) + unsym (b + c) * unsym a)) =
    sym (⅟2 * (unsym a * unsym b + unsym b * unsym a)) + sym (⅟2 * (unsym a * unsym c + unsym c * unsym a))

Tactic:
← sym_add,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym (b + c) + unsym (b + c) * unsym a)) =
    sym (⅟2 * (unsym a * unsym b + unsym b * unsym a) + ⅟2 * (unsym a * unsym c + unsym c * unsym a))
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym (a + b) * unsym c + unsym c * unsym (a + b))) =
    sym (⅟2 * (unsym a * unsym c + unsym c * unsym a)) + sym (⅟2 * (unsym b * unsym c + unsym c * unsym b))

Tactic:
← sym_add,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym (a + b) * unsym c + unsym c * unsym (a + b))) =
    sym (⅟2 * (unsym a * unsym c + unsym c * unsym a) + ⅟2 * (unsym b * unsym c + unsym c * unsym b))
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
⊢ (X.restrictStalkIso h x).inv = Hom.stalkMap (X.ofRestrict h) x

Tactic:
refine colimit.hom_ext fun V => ?_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        V ≫
      (X.restrictStalkIso h x).inv =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        V ≫
      Hom.stalkMap (X.ofRestrict h) x
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ x ∈
    Set.range
      ⇑(ConcreteCategory.hom
          (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom'
              h₂).base)

Tactic:
rw [LocallyRingedSpace.IsOpenImmersion.lift_range]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ x ∈ ⇑(ConcreteCategory.hom (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f).base) ⁻¹' Set.range ⇑i
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ LocallyRingedSpace.IsOpenImmersion
    (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom' h₂)

Tactic:
delta LocallyRingedSpace.IsOpenImmersion.lift; infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.snd f g)

Tactic:
rw [SheafedSpace.isOpenImmersion_iff_hom]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (pullback.snd f g).hom
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.fst g f)

Tactic:
rw [SheafedSpace.isOpenImmersion_iff_hom]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (pullback.fst g f).hom
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case mk.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝¹ : ι
U : Opens ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace
y : ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace
hy : y ∈ ↑U
as✝ : ι
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj { as := as✝ })
h : { as := as✝¹ } ≠ { as := as✝ }
eq :
  (ConcreteCategory.hom
        ((forget C).map (colimit.ι F { as := as✝¹ }) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      y =
    (ConcreteCategory.hom
        ((forget C).map (colimit.ι F { as := as✝ }) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      x
⊢ False

Tactic:
ι_preservesColimitIso_hom_assoc,

Goal state after:
case mk.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝¹ : ι
U : Opens ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace
y : ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace
hy : y ∈ ↑U
as✝ : ι
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj { as := as✝ })
h : { as := as✝¹ } ≠ { as := as✝ }
eq :
  (ConcreteCategory.hom
        (colimit.ι (F ⋙ forget C) { as := as✝¹ } ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      y =
    (ConcreteCategory.hom
        ((forget C).map (colimit.ι F { as := as✝ }) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      x
⊢ False
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case mk.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝¹ : ι
U : Opens ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace
y : ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace
hy : y ∈ ↑U
as✝ : ι
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj { as := as✝ })
h : { as := as✝¹ } ≠ { as := as✝ }
eq :
  (ConcreteCategory.hom
        (colimit.ι (F ⋙ forget C) { as := as✝¹ } ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      y =
    (ConcreteCategory.hom
        ((forget C).map (colimit.ι F { as := as✝ }) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      x
⊢ False

Tactic:
ι_preservesColimitIso_hom_assoc,

Goal state after:
case mk.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝¹ : ι
U : Opens ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace
y : ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace
hy : y ∈ ↑U
as✝ : ι
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj { as := as✝ })
h : { as := as✝¹ } ≠ { as := as✝ }
eq :
  (ConcreteCategory.hom
        (colimit.ι (F ⋙ forget C) { as := as✝¹ } ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      y =
    (ConcreteCategory.hom
        (colimit.ι (F ⋙ forget C) { as := as✝ } ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      x
⊢ False
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this : Module R N := Module.compHom N σ
⊢ (comapFun f y) (LocalizedModule.mk a b) = LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

Tactic:
let := σ.toAlgebra

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝ : Module R N := Module.compHom N σ
this : Algebra R S := σ.toAlgebra
⊢ (comapFun f y) (LocalizedModule.mk a b) = LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
this : Module R N := Module.compHom N σ
⊢ (isLocallyFraction S N).pred (comapFun f U V hUV s)

Tactic:
let := σ.toAlgebra

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
this✝ : Module R N := Module.compHom N σ
this : Algebra R S := σ.toAlgebra
⊢ (isLocallyFraction S N).pred (comapFun f U V hUV s)
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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f' i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i j hij

Tactic:
delta f'

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i j hij
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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f' i k ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i k hik

Tactic:
delta f'

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i k h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i k hik
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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j k hjk ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j k

Tactic:
delta f'

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j k hjk ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j k h
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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j i ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j i

Tactic:
delta f'

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j i ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j i h
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
x y : ↑(∐ D.U)
h : (ConcreteCategory.hom D.π) x = (ConcreteCategory.hom D.π) y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
delta GlueData.π Multicoequalizer.sigmaπ at h

Goal state after:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom
        (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap ≫ (Multicoequalizer.isoCoequalizer D.diagram).inv))
      x =
    (ConcreteCategory.hom
        (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap ≫ (Multicoequalizer.isoCoequalizer D.diagram).inv))
      y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case e'_3
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
e_1✝ : ↑((Opens.toTopCat (of α)).obj (U i)) = ↑((ofOpenSubsets U).U i)
⊢ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) ∘ ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹'
      ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s =
    ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s

Tactic:
Set.preimage_comp

Goal state after:
case e'_3
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
e_1✝ : ↑((Opens.toTopCat (of α)).obj (U i)) = ↑((ofOpenSubsets U).U i)
⊢ ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹'
      ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) ⁻¹' ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s =
    ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s
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 : D.J
⊢ IsOpenEmbedding
    (⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ∘ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)))

Tactic:
exact (TopCat.homeoOfIso (𝖣.gluedIso (PresheafedSpace.forget _)).symm).isOpenEmbedding.comp
      (D.toTopGlueData.ι_isOpenEmbedding i)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ IsPullback f coprod.inl coprod.inl (coprod.map f g)

Tactic:
refine IsOpenImmersion.isPullback _ _ _ _ (by simp) ?_

Goal state after:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl = Scheme.Hom.opensRange coprod.inl