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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
ih : ∃ q r, (∀ (i : Fin n), (r i).degree < g.degree) ∧ f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ ∃ q r, (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i, r i * g ^ ↑i

Tactic:
obtain ⟨q, r, hr, hf⟩ := ih
    refine ⟨q /ₘ g, Fin.snoc r (q %ₘ g), fun i => ?_, hf.trans ?_⟩
    · cases i using Fin.lastCases with
      | cast i => simpa using hr i
      | last => simpa using degree_modByMonic_lt q hg
    · rw [Fin.sum_univ_castSucc, ← add_rotate', Fin.snoc_last, Fin.val_last,
        ← add_assoc, pow_succ', ← mul_assoc, ← add_mul, mul_comm (q /ₘ g) g,
        modByMonic_add_div q]
      simp

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ eval₂ RingHom.smulOneHom x p = p.smeval x

Tactic:
by
  rw [smeval_eq_sum, eval₂_eq_sum]
  congr 1 with e a
  simp only [RingHom.smulOneHom_apply, smul_one_mul, smul_pow]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
⊢ x * q.smeval y = q.smeval y * x

Tactic:
refine (commute_iff_eq x (q.smeval y)).mp ?_

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
⊢ Commute x (q.smeval y)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

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

Tactic:
simp [signVariations]

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

Goal state before:
pp: α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : PresentedMonoid rels
⊢ x ∈ closure (range (of rels))

Tactic:
induction x with | _ a

Goal state after:
case h
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
a : FreeMonoid α
⊢ (mk rels) a ∈ closure (range (of rels))
Module: Mathlib.Algebra.PresentedMonoid.Basic

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
⊢ φ = ψ

Tactic:
apply MonoidHom.eq_of_eqOn_denseM (closure_range_of _)

Goal state after:
α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
⊢ EqOn (⇑φ) (⇑ψ) (range (of rels))
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
by ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
by ext <;> simp <;> ring

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

Goal state before:
pp: case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ (algebraMap R (QuadraticAlgebra R a b)) (x * r) = 0

Tactic:
hxr,

Goal state after:
case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ (algebraMap R (QuadraticAlgebra R a b)) 0 = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
⊢ z * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → z = 0

Tactic:
hz

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz : z * (algebraMap R (QuadraticAlgebra R a b)) r = 0
⊢ z = 0
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
have hrd {r : (i : ι) → Fin (n i) → R[X]} (hr : ∀ i ∈ s, ∀ j, (r i j).degree < (g i).degree)
      (i : ι) (hi : i ∈ s) : (∑ j, r i j * g i ^ j.1).degree < (g i ^ n i).degree := by
    refine (degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 fun j _ => ?_)
    · rw [bot_lt_iff_ne_bot, degree_ne_bot]
      exact ((hg i hi).pow (n i)).ne_zero
    · refine (degree_mul_le _ _).trans_lt ?_
      rw [degree_eq_natDegree ((hg i hi).pow j.1).ne_zero, (hg i hi).natDegree_pow,
        degree_eq_natDegree ((hg i hi).pow (n i)).ne_zero, (hg i hi).natDegree_pow]
      conv_rhs => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.2 j.neZero.ne)]
      rw [Nat.add_one_mul, Nat.add_comm, Nat.cast_add, ← degree_eq_natDegree (hg i hi).ne_zero]
      refine WithBot.add_lt_add_of_lt_of_le (WithBot.natCast_ne_bot _) (hr i hi j) ?_
      exact Nat.cast_le.2 (Nat.mul_le_mul_right _ (Nat.le_sub_one_of_lt j.isLt))

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
hrd :
  ∀ {r : (i : ι) → Fin (n i) → R[X]},
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) →
      ∀ i ∈ s, (∑ j, r i j * g i ^ ↑j).degree < (g i ^ n i).degree
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ + 1
hp : P ≠ 0
⊢ ∃ x ∈ P.roots, 0 < x

Tactic:
by grind [Multiset.countP_pos]

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

Goal state before:
pp: case mk
R : Type u
inst₂ : NonUnitalRing R
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ }.toNonUnitalNonAssocRing =
    inst₂.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ } = inst₂

Tactic:
cases inst₂

Goal state after:
case mk.mk
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
mul_assoc✝¹ : ∀ (a b c : R), a * b * c = a * (b * c)
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_assoc := mul_assoc✝¹ }.toNonUnitalNonAssocRing =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ }.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_assoc := mul_assoc✝¹ } =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ }
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 : α), Commute a a_1

Tactic:
exact (congr($hc.symm ·))

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a a' : α
f : SkewMonoidAlgebra M α
h : a' ≠ a
⊢ ((erase a) f).coeff a' = f.coeff a'

Tactic:
simp [erase, h]

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

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

Tactic:
← mul_inv

Goal state after:
⊢ (√2 * √2)⁻¹ = 2⁻¹
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
⊢ x * y ∈ ⊥

Tactic:
rw [hx, hy, mem_bot, inr_mul_inr]

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

Goal state before:
pp: R : Type u_1
inst✝ : LinearOrder R
l : List R
⊢ trop l.minimum = (map (trop ∘ WithTop.some) l).sum

Tactic:
by
  induction l with
  | nil => simp
  | cons hd tl IH => simp [List.minimum_cons, ← IH]

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

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ (∀ (x : E), (star f).ofConv x = f.ofConv x) ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)

Tactic:
intrinsicStar_apply,

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ (∀ (x : E), star (f.ofConv (star x)) = f.ofConv x) ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
α : R
x : V
⊢ (star f).ofConv x = α • x ↔ f.ofConv (star x) = star α • star x

Tactic:
intrinsicStar_apply,

Goal state after:
R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
α : R
x : V
⊢ star (f.ofConv (star x)) = α • x ↔ f.ofConv (star x) = star α • star x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case h
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)
F : J ⥤ PresheafedSpace C
j j' : J
f : j ⟶ j'
⊢ (F.map f ≫ { base := colimit.ι (F ⋙ forget C) j', c := limit.π (pushforwardDiagramToColimit F).leftOp (op j') }).c ≫
      whiskerRight (eqToHom ⋯) (F.obj j).presheaf =
    ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) } ≫
        ((Functor.const J).obj (colimit F)).map f).c

Tactic:
ext ⟨⟩

Goal state after:
case h
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)
F : J ⥤ PresheafedSpace C
j j' : J
f : j ⟶ j'
carrier✝ : Set ↑↑(((Functor.const J).obj (colimit F)).obj j')
is_open'✝ : IsOpen carrier✝
⊢ ((F.map f ≫ { base := colimit.ι (F ⋙ forget C) j', c := limit.π (pushforwardDiagramToColimit F).leftOp (op j') }).c ≫
          whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app
      (op { carrier := carrier✝, is_open' := is_open'✝ }) =
    ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) } ≫
            ((Functor.const J).obj (colimit F)).map f).c.app
      (op { carrier := carrier✝, is_open' := is_open'✝ })
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))

Tactic:
have eq₁ := congr_app H.hom_inv_id (op ((Opens.map H.hom.base).obj U))

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  (H.hom ≫ H.inv).c.app (op ((Opens.map H.hom.base).obj U)) =
    (𝟙 X).c.app (op ((Opens.map H.hom.base).obj U)) ≫ X.presheaf.map (eqToHom ⋯)
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ ∀ (x : ↑↑(X.restrict h).toPresheafedSpace), IsLocalRing ↑((X.restrict h).presheaf.stalk x)

Tactic:
intro x
    -- We show that the stalk of the restriction is isomorphic to the original stalk,
    apply @RingEquiv.isLocalRing _ _ _ (X.isLocalRing (f x))
    exact (X.restrictStalkIso h x).symm.commRingCatIsoToRingEquiv

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

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ ¬0 = 1

Tactic:
change (0 : X.presheaf.stalk x) ≠ (1 : X.presheaf.stalk x)

Goal state after:
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ 0 ≠ 1
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x) =
    (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f) *
      (ConcreteCategory.hom (X.presheaf.germ (V y) z hzVy)) (g y)

Tactic:
hg x,

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) 1 =
    (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f) *
      (ConcreteCategory.hom (X.presheaf.germ (V y) z hzVy)) (g y)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
x : ↥X
hx : IsClosed {x}
⊢ height x = 0

Tactic:
simp only [height_eq_zero]
  intro b _
  obtain rfl | h := eq_or_ne b x
  · assumption
  · have := IsClosed.not_specializes hx rfl h
    contradiction

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
U : TopologicalSpace.Opens ↥Y
⊢ (toLRSHom'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op U) = toLRSHom'✝.c.app (op U)

Tactic:
simpa using! h_app U

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
x : ↥X
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := ⇑f, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))

Tactic:
convert! f.prop x using 4

Goal state after:
case e'_7.e'_3.e'_6
X Y : Scheme
f : X.Hom Y
x : ↥X
e_3✝ :
  (↑(Y.presheaf.stalk ((ConcreteCategory.hom (ofHom { toFun := ⇑f, continuous_toFun := ⋯ })) x)) →+*
      ↑(X.presheaf.stalk x)) =
    (↑(Y.presheaf.stalk (f x)) →+* ↑(X.presheaf.stalk x))
e_1✝ :
  Y.presheaf.stalk ((ConcreteCategory.hom (ofHom { toFun := ⇑f, continuous_toFun := ⋯ })) x) = Y.presheaf.stalk (f x)
e_5✝ : ofHom { toFun := ⇑f, continuous_toFun := ⋯ } ≍ f.toLRSHom'.1.base
⊢ f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom = f.toLRSHom'.1.c
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
⊢ (∀ (x : Y), ∃ Y_1 g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)) ↔
    Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
refine ⟨fun hf x ↦ ?_, fun hf x ↦ ⟨X, f, ⟨⟩, by simp [hf.range_eq]⟩⟩

Goal state after:
X Y : Type u
f : X ⟶ Y
hf : ∀ (x : Y), ∃ Y_1 g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)
x : (fun X ↦ X) Y
⊢ ∃ a, (ConcreteCategory.hom f) a = x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).base = s.snd.base

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.snd.c.app x

Tactic:
· change pullback.lift _ _ _ ≫ pullback.snd _ _ = _
    simp

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.snd.c.app 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)

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:
· rw [LocallyRingedSpace.IsOpenImmersion.lift_range]; exact h₁

Goal state after:
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₂)
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: 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.fst f g) a = x

Tactic:
rw [← show _ = (pullback.fst _ _ : pullback f g ⟶ _).base from
        PreservesPullback.iso_hom_fst Scheme.forgetToTop f g]
    have : x ∈ Set.range (pullback.fst f.base g.base) := by
      rw [TopCat.pullback_fst_range f.base g.base]
      use y
    obtain ⟨a, ha⟩ := this
    use (PreservesPullback.iso Scheme.forgetToTop f g).inv a
    rwa [← TopCat.comp_app, Iso.inv_hom_id_assoc]

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

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (SheafedSpace.forgetToPresheafedSpace.map (forgetToSheafedSpace.map (pullback.snd f g)))

Tactic:
← PreservesPullback.iso_hom_snd
      (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g

Goal state after:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso
    ((PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g).hom ≫
      pullback.snd ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Tactic:
by
  refine (Scheme.image_basicOpen (X.ofRestrict U.isOpenEmbedding) r).trans ?_
  rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.isOpenEmbedding_obj_top).op]
  rw [← CommRingCat.comp_apply, ← CategoryTheory.Functor.map_comp, ← op_comp, eqToHom_trans,
    eqToHom_refl, op_id]
  congr
  exact (PresheafedSpace.IsOpenImmersion.ofRestrict_invApp _ _ _).trans
    (CategoryTheory.Functor.map_id _ _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : Opens ↥↑V
⊢ X.homOfLE e ∣_ W ≫ (Scheme.Hom.isoImage V.ι W).hom = (Scheme.Hom.isoImage U.ι (X.homOfLE e ⁻¹ᵁ W)).hom ≫ X.homOfLE ⋯

Tactic:
by
  simp [← cancel_mono (V.ι ''ᵁ W).ι]

Goal state after: