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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : R[X] ⊗[R] M →ₗ[R[X]] PolynomialModule R M := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M := ↑R (eval X) ∘ₗ map R[X] ((TensorProduct.mk R R[X] M) 1)
left : inv ∘ₗ ↑R e = LinearMap.id
⊢ ↑R e ∘ₗ inv = LinearMap.id

Tactic:
ext n x
    simp [e, inv, ← monomial_one_right_eq_X_pow]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (p.homogenize n).IsHomogeneous n

Tactic:
by
  refine MvPolynomial.IsHomogeneous.sum _ _ _ ?_
  simp only [Prod.forall, mem_antidiagonal]
  rintro a b rfl
  apply MvPolynomial.isHomogeneous_monomial
  simp [Finsupp.update_eq_add_single]

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
a : α
⊢ IsChain R (destutter' R a l)

Tactic:
by
  induction l using twoStepInduction generalizing a with
  | nil => simp
  | singleton => simp [apply_ite]
  | cons_cons b c l IH IH2 =>
    simp_rw [destutter'_cons, apply_ite (IsChain R ·), IH, if_true_right] at IH2
    simp_rw [destutter'_cons, apply_ite (IsChain R ·),
      apply_ite (IsChain R <| a :: ·), IH, isChain_cons_cons,
      if_true_right, ite_prop_iff_and, imp_and]
    exact ⟨⟨⟨Function.swap <| fun _ => id, fun _ => IH2 c b⟩,
      Function.swap <| fun _ => IH2 b a⟩, fun _ => IH2 c a⟩

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Tactic:
simp only [destutter', if_neg hbc]

Goal state after:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + q₂ * g) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂

Tactic:
← mul_comm g

Goal state after:
case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + g * q₂) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
p : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (p ^ n).smeval x * (p ^ 1).smeval x = p.smeval x ^ (n + 1)

Tactic:
smeval_pow n,

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
p : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ p.smeval x ^ n * (p ^ 1).smeval x = p.smeval x ^ (n + 1)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y z : R
⊢ x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z

Tactic:
← left_cancel (x ◃⁻¹ y),

Goal state after:
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ (x ◃⁻¹ y) ◃ x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃ (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case mul
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
ih_y :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦y⟧ =
    F ⟦y⟧
⊢ ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x.mul y⟧ =
    F ⟦x.mul y⟧

Tactic:
have hm : ⟦x.mul y⟧ = @Mul.mul (EnvelGroup R) _ ⟦x⟧ ⟦y⟧ := rfl

Goal state after:
case mul
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
ih_y :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦y⟧ =
    F ⟦y⟧
hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧
⊢ ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x.mul y⟧ =
    F ⟦x.mul y⟧
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
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * (∏ x ∈ s, (algebraMap R[X] K) (g x))⁻¹ =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹
⊢ (algebraMap R[X] K) f / ∏ x ∈ s, (algebraMap R[X] K) (g x) =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) / (algebraMap R[X] K) (g x)

Tactic:
div_eq_mul_inv

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[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * (∏ x ∈ s, (algebraMap R[X] K) (g x))⁻¹ =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹
⊢ (algebraMap R[X] K) f * (∏ x ∈ s, (algebraMap R[X] K) (g x))⁻¹ =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝¹ : DecidableEq G'
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
⊢ (f.sum g).support ⊆ f.support.biUnion fun a ↦ (g a (f.coeff a)).support

Tactic:
by
  simp_rw [support, coeff_sum']
  apply Finsupp.support_sum

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 → R → Prop
⊢ ∀ (a b c : RingQuot r), a * (b + c) = a * b + a * c

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [mul_quot, add_quot, left_distrib]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
h : 4 * P = 4 • P
⊢ P = (1 / 4) • (P * P)

Tactic:
rw [idem, h, ← mul_smul]

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
h : 4 * P = 4 • P
⊢ P = (1 / 4 * 4) • P
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
ha : a ≠ 0
⊢ (p.update n a).support = insert n p.support

Tactic:
by classical rw [support_update, if_neg ha]

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
⊢ coeff A n = ncoeff A (-n - 1)

Tactic:
rw [ncoeff_apply, neg_sub, Int.sub_neg, add_sub_cancel_left]

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

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
w : ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (X.continuousPrelocal T).pred fun x ↦ f (i x)
⊢ (X.continuousPrelocal T).pred f

Tactic:
by
      apply continuous_iff_continuousAt.2
      intro x
      specialize w x
      rcases w with ⟨V, m, i, w⟩
      dsimp at w
      rw [continuous_iff_continuousAt] at w
      specialize w ⟨x, m⟩
      simpa using (Opens.isOpenEmbedding_of_le i.le).continuousAt_iff.1 w

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

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
p : ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
specialize p ⟨x.1, m⟩

Goal state after:
X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
p : ∃ V_1, ∃ (_ : ↑⟨↑x, m⟩ ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf =
    (𝟙 (sheafedSpaceObj R)).hom.c

Tactic:
· ext
    dsimp
    rw [comap_id (by simp)]
    simp
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    toStalk (↑R) p ≫ (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).hom.c

Tactic:
by
  rw [StructureSheaf.toStalk, Category.assoc, TopCat.Presheaf.stalkFunctor_map_germ]
  exact Spec_Γ_naturality_assoc f _

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

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

Tactic:
← TopCat.comp_app,

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace C
Y : SheafedSpace C
f : X ⟶ Y.toPresheafedSpace
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((TopCat.Presheaf.pushforward C (isoRestrict f).symm.hom.base).obj (Y.restrict ⋯).presheaf).IsSheaf

Tactic:
apply TopCat.Sheaf.pushforward_sheaf_of_sheaf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace C
Y : SheafedSpace C
f : X ⟶ Y.toPresheafedSpace
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (Y.restrict ⋯).presheaf.IsSheaf
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✝ : JointlySurjective K
𝒰 : Cover K X
h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)
⊢ 𝒰.presieve₀ ∈ (precoverage Q).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]
    exact ⟨𝒰.exists_eq, h⟩

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 j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      ((ConcreteCategory.hom (colimit.ι F i).hom.base) y) =
    (ConcreteCategory.hom
        ((preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      ((ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x))
⊢ False

Tactic:
← TopCat.comp_app,

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

Goal state before:
pp: case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier ⊆ U

Tactic:
· rw [Set.image_subset_iff]; exact hVU

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
x✝¹ x✝ : M
⊢ const (x✝¹ + x✝) 1 U ⋯ = const x✝¹ 1 U ⋯ + const x✝ 1 U ⋯

Tactic:
simp [const_add]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
W : (↑(f ⁻¹ᵁ U)).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
⊢ Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯

Tactic:
rw [Scheme.Hom.appLE, morphismRestrict_app', Scheme.Opens.toScheme_presheaf_map,
    Scheme.Hom.appLE_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsLocalizedModule ⊥ (toOpenₗ R M ⊤) ↔ IsLocalizedModule (Submonoid.powers 1) (toOpenₗ R M (basicOpen 1))

Tactic:
rw [PrimeSpectrum.basicOpen_one, Submonoid.powers_one]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
⊢ X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β

Tactic:
by
  refine LocallyRingedSpace.forgetToSheafedSpace.map_injective
    (Spec.basicOpen_hom_ext w ?_)
  intro r U
  erw [SheafedSpace.comp_hom_c_app, toOpen_comp_comap_assoc]
  dsimp
  rw [Category.assoc]
  erw [toΓSpecSheafedSpace_app_spec, ← X.presheaf.map_comp]
  exact h r

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
⊢ IsUnit ((ConcreteCategory.hom (toStalk R x)) f)

Tactic:
by
  convert! (isUnit_basicOpen f).map ((structurePresheafInCommRingCat R).germ _ x hf).hom
  exact ((structurePresheafInCommRingCat R).germ_res_apply (homOfLE (le_top : basicOpen f ≤ ⊤))
    x hf (algebraMap R Γ(R, ⊤) f)).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X✝ Y✝ : Scheme
U✝ : X✝.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X✝, U✝)
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r) ≤ f ⁻¹ᵁ Y.basicOpen r

Tactic:
simp [Scheme.Hom.appLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: ⊢ ∀ (X : CommRingCatᵒᵖ), IsIso (adjunction.counit.app X)

Tactic:
intro R

Goal state after:
R : CommRingCatᵒᵖ
⊢ IsIso (adjunction.counit.app R)
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 :
  pullback.fst (D.f i j) (D.f i i) ≫ 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))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))

Tactic:
rw [← IsIso.eq_inv_comp, ← Category.assoc, IsIso.comp_inv_eq] at this

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.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed {↑x}
hx₀ : IsClosed {x}
⊢ IsClosed {hU.primeIdealOf x}

Tactic:
primeIdealOf,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed {↑x}
hx₀ : IsClosed {x}
⊢ IsClosed {hU.isoSpec.hom x}
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : hU.fromSpec y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y)

Tactic:
convert StructureSheaf.IsLocalization.to_stalk Γ(X, U) y

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : hU.fromSpec y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y) ↔
    IsLocalization.AtPrime (↑((structureSheaf ↑Γ(X, U)).presheaf.stalk y)) y.asIdeal
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i = pullback.fst (D.f k j) (D.f k i) ≫ D.t k j ≫ D.t j k ≫ D.f k j

Tactic:
𝖣.t_inv_assoc

Goal state after:
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i = pullback.fst (D.f k j) (D.f k i) ≫ D.f k j
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_3
R S : CommRingCat
f : R ⟶ S
r : ↑R
hcomp :
  CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)) ≫
      CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) =
    f ≫ CommRingCat.ofHom (algebraMap (↑S) (Localization.Away ((CommRingCat.Hom.hom f) r)))
⊢ ((Spec S).isoOfEq ⋯ ≪≫ basicOpenIsoSpecAway ((CommRingCat.Hom.hom f) r)).hom ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)) ≫
          CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)) =
    Spec.map f ∣_ basicOpen r ≫
      (basicOpenIsoSpecAway r).hom ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))

Tactic:
simp [hcomp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) := ((ΓSpec.adjunction.homEquiv X (op A)).symm f).unop
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (specTargetImageFactorization f)))

Tactic:
let φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (RingHom.kerLift φ.hom)

Goal state after:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) := ((ΓSpec.adjunction.homEquiv X (op A)).symm f).unop
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (CommRingCat.Hom.hom φ).kerLift
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (specTargetImageFactorization f)))