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

Goal state before:
pp: case succ.inr.inr.refine_2
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 + 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

pp: case succ.inl.refine_2
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
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
· /- P starts with [+,+,...]. (X-C)*P starts with [+,?,...]. After dropping the lead of P, this
      becomes [+,...] and [+,...]. So the sign variations on P are unchanged when we induct, while
      (X-C)*P can only lose at most one sign change. -/
    grind [sign_eq_one_iff, signVariations_X_sub_C_mul_eraseLead_le]

Goal state after:
case succ.inl.refine_2
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
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = y

Tactic:
trans (x ◃ x) ◃⁻¹ x ◃ x

Goal state after:
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x

R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
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:
by
  rw [← i_mul_j, mul_assoc, j_mul_i, mul_sub, i_mul_k, neg_smul, mul_smul_comm, i_mul_j]
  linear_combination (norm := module)

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.k * q.j = c₃ • q.i

Tactic:
by
  rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝ : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
x : H
⊢ (equivMapDomain f l).coeff x = ((mapDomain ⇑f) l).coeff x

Tactic:
simp_rw [coeff_equivMapDomain, Finsupp.equivMapDomain_apply, coeff_mapDomain,
    Finsupp.mapDomain_equiv_apply]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst✝² : Semiring k
inst✝¹ : AddCommMonoid A
inst✝ : Module k A
e : G ≃ H
c : k
x : SkewMonoidAlgebra A G
⊢ equivMapDomain e (c • x) = c • equivMapDomain e x

Tactic:
simp_rw [equivMapDomain_eq_mapDomain, mapDomain_smul]

Goal state after:
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 0) = 0

Tactic:
by simp only [← zero_quot, map_zero]

Goal state after:
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
f : A ≃ₐ[S] B
rel : A → A → Prop
x y : A
h_rel : rel x y
⊢ (rel on ⇑f.symm) (↑↑f x) (↑↑f y)

Tactic:
simpa [Function.onFun]

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

Tactic:
rw [hs] at hx ⊢

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.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ g (star (f (star a))) = star ((star g) (f (star a)))

Tactic:
rw [star_apply, star_star]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ star (f ((star g) (star a))) = star (f (star (g a)))

Tactic:
rw [star_apply, star_star]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a n : ℕ
h : a.AtLeastTwo
⊢ (OfNat.ofNat a).coeff (n + 1) = 0

Tactic:
rw [← Nat.cast_ofNat]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a n : ℕ
h : a.AtLeastTwo
⊢ (↑(OfNat.ofNat a)).coeff (n + 1) = 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X ^ 0 = (monomial 0) 1

Tactic:
simp only [pow_zero, monomial_zero_left, ← CRingHom_eq_C, map_one]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝ : AddCommMonoid k'
f : G →₀ k
g : G → k → G' →₀ k'
⊢ { coeff := f.sum g }.coeff = ({ coeff := f }.sum fun x1 x2 ↦ { coeff := g x1 x2 }).coeff

Tactic:
simp only [coeff_sum']

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddGroupWithOne k
inst✝ : One G
z : ℤ
⊢ ↑z = single 1 ↑z

Tactic:
cases z <;> simp

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)
⊢ (∀ (a : R), a * ↑(toUnits v)⁻¹ = ↑(toUnits v)⁻¹ * ↑(toUnits u) * a * ↑(toUnits u)⁻¹) ↔
    ∃ α, ↑(toUnits u) = α • ↑(toUnits v)

Tactic:
Units.eq_mul_inv_iff_mul_eq,

Goal state after:
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)
⊢ (∀ (a : R), a * ↑(toUnits v)⁻¹ * ↑(toUnits u) = ↑(toUnits v)⁻¹ * ↑(toUnits u) * a) ↔
    ∃ α, ↑(toUnits u) = α • ↑(toUnits v)
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∀ (a : R), a * ↑(toUnits v)⁻¹ = ↑(toUnits v)⁻¹ * ↑(toUnits u) * a * ↑(toUnits u)⁻¹) ↔ ∃ α, u = α • v

Tactic:
Units.eq_mul_inv_iff_mul_eq,

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∀ (a : R), a * ↑(toUnits v)⁻¹ * ↑(toUnits u) = ↑(toUnits v)⁻¹ * ↑(toUnits u) * a) ↔ ∃ α, u = α • v
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ x + y = y ↔ y ≤ x

Tactic:
rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_right_iff]

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a

Tactic:
rintro ⟨rfl, rfl⟩
    simp

Goal state after:
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
      congr 2
      rw [mul_add]
      abel

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

Goal state before:
pp: R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
n : ℕ
⊢ untrop (if n + 1 = 0 then 0 else 1) = untrop ((if n = 0 then 0 else 1) + 1)

Tactic:
cases n <;> simp

Goal state after:
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
      congr 2
      rw [mul_add]
      abel

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pullback

Goal state before:
pp: C : Type v₁
inst✝¹¹ : SmallCategory C
D : Type v₁
inst✝¹⁰ : SmallCategory D
G : C ⥤ D
A : Type u₁
inst✝⁹ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
FA : A → A → Type u_1
CA : A → Type v₁
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : PreservesLimits (forget A)
inst✝⁵ : HasColimits A
inst✝⁴ : HasLimits A
inst✝³ : PreservesFilteredColimits (forget A)
inst✝² : (forget A).ReflectsIsomorphisms
inst✝¹ : G.IsContinuous J K
inst✝ : RepresentablyFlat G
⊢ PreservesFiniteLimits (G.sheafPullback A J K)

Tactic:
by
  apply sheafPullbackConstruction.preservesFiniteLimits

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
F : J ⥤ PresheafedSpace C
j : J
U : (Opens ↑↑(F.obj j))ᵒᵖ
⊢ (F.map (𝟙 j)).c.app U = (Pushforward.id (F.obj j).presheaf).inv.app U ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom.app U

Tactic:
by
  simp [PresheafedSpace.congr_app (F.map_id j)]

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

Goal state before:
pp: case inr
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
h : n > 0
⊢ X.toRingedSpace.basicOpen (f ^ n) = ⊥

Tactic:
hn

Goal state after:
case inr
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
h : n > 0
⊢ X.toRingedSpace.basicOpen 0 = ⊥
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case h
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := ⋯
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
x : ↑X
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
⊢ P.pred fun x ↦ gl ((Opens.leSupr U i) x)

Tactic:
convert! (sf i).property using 1

Goal state after:
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
x : ↑X
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
⊢ (fun x ↦ gl ((Opens.leSupr U i) x)) = ↑(sf i)
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
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ (X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop V)))) =
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
      Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
IsIso.comp_inv_eq

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯) =
    ((X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
        Y.presheaf.map ((opensFunctor f).op.map i)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V)))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
⊢ X.zeroLocus (s * t) = X.zeroLocus s ∪ X.zeroLocus t

Tactic:
simp only [← Set.image2_mul, zeroLocus_def, Set.biInter_image2]

Goal state after:
X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
⊢ ⋂ a ∈ s, ⋂ b ∈ t, (X.basicOpen (a * b)).carrierᶜ =
    (⋂ f ∈ s, (X.basicOpen f).carrierᶜ) ∪ ⋂ f ∈ t, (X.basicOpen f).carrierᶜ
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑I.radical = X.zeroLocus ↑I

Tactic:
refine (X.zeroLocus_mono I.le_radical).antisymm ?_
  simp only [Set.subset_def, mem_zeroLocus_iff, SetLike.mem_coe]
  rintro x H f ⟨n, hn⟩ hx
  rcases n.eq_zero_or_pos with rfl | hn'
  · exact H f (by simpa using I.mul_mem_left f hn) hx
  · exact H _ hn (X.basicOpen_pow f hn' ▸ hx)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings Y

Tactic:
Precoverage.mem_comap_iff,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.map F (Presieve.ofArrows X f) ∈ Types.jointlySurjectivePrecoverage.coverings (F.obj S)
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.map F (Presieve.ofArrows P p₁) ∈ Types.jointlySurjectivePrecoverage.coverings (F.obj Y)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: R : CommRingCat
f g : ↑R
⊢ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (f * g)))) =
    Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))

Tactic:
simp only [← Spec.map_comp, ← CommRingCat.ofHom_comp]

Goal state after:
R : CommRingCat
f g : ↑R
⊢ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (f * g)))) =
    Spec.map
      (CommRingCat.ofHom ((IsLocalization.Away.awayToAwayRight f g).comp (algebraMap (↑R) (Localization.Away f))))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ∣_ U ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f

Tactic:
delta morphismRestrict

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (f ≫ g) ∣_ U = f ∣_ g ⁻¹ᵁ U ≫ g ∣_ U

Tactic:
delta morphismRestrict

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ IsIso (f ∣_ U)

Tactic:
delta morphismRestrict

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ IsIso ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
inst✝ : IsOpenImmersion f
⊢ IsOpenImmersion (f ∣_ U)

Tactic:
delta morphismRestrict

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
inst✝ : IsOpenImmersion f
⊢ IsOpenImmersion ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op))
      ((ConcreteCategory.hom (X.toRingedSpace.presheaf.map (homOfLE ⋯).op)) r)

Tactic:
rw [← CommRingCat.comp_apply, ← Functor.map_comp]

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))) r
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_2
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i : ↥t
⊢ (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
    const ((fun i ↦ g ↑i ^ N • f ↑i) i) ((fun i ↦ g ↑i ^ (N + 1)) i) (basicOpen ((fun i ↦ g ↑i ^ (N + 1)) i)) ⋯

Tactic:
· convert! congr((structureSheafInType R M).presheaf.map (homOfLE ?_).op $((H i).symm)) using 1
    · refine Subtype.ext <| funext fun x ↦ LocalizedModule.mk_eq.mpr ⟨1, ?_⟩
      simp [Submonoid.smul_def, pow_succ', mul_smul]
    · simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ

Tactic:
rw [Set.preimage_compl, Opens.carrier_eq_coe]

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ (⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ↑(basicOpen i))ᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
this :
  (D.t i j ≫ D.t j i) ≫ inv (pullback.fst (D.f i j) (D.f i i)) =
    inv (pullback.fst (D.f i j) (D.f i i)) ≫ 𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))

Tactic:
IsIso.comp_inv_eq

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
this :
  D.t i j ≫ D.t j i =
    (inv (pullback.fst (D.f i j) (D.f i i)) ≫ 𝟙 (pullback (D.f i j) (D.f i i))) ≫ pullback.fst (D.f i j) (D.f i i)
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
Module: Mathlib.Topology.Gluing

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

Tactic:
exact Set.preimage_mono (Set.image_subset_range _ _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ X.toSpecΓ ≫
      Spec.map
        (CommRingCat.ofHom
          ((Ideal.Quotient.lift I (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop)) hI).comp (Ideal.Quotient.mk I))) =
    f

Tactic:
Ideal.Quotient.lift_comp_mk

Goal state after:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))) = f
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
⊢ ↑D.glued.toPresheafedSpace ≅
    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued

Tactic:
refine (PresheafedSpace.forget _).mapIso ?_ ≪≫
    GlueData.gluedIso _ (PresheafedSpace.forget.{_, _, u} _)

Goal state after:
D : GlueData
⊢ D.glued.toPresheafedSpace ≅ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.glued
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
· apply glued_cover_cocycle_snd

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
inst✝ : IsEmpty ↥X
U : X.Opens
⊢ Subsingleton ↑Γ(X, U)

Tactic:
obtain rfl : U = ⊥ := Subsingleton.elim _ _; infer_instance

Goal state after: