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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
r : R
⊢ eval (f r) (map f (eval q p)) = f (eval r (eval q p))

Tactic:
eval_map,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
r : R
⊢ eval₂ f (f r) (eval q p) = f (eval r (eval q p))
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
⊢ (if p + q = 0 then 0 else ↑(Fintype.card Fq) ^ (p + q).natDegree) ≤
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) + if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

Tactic:
by_cases hp : p = 0; · simp [hp]
      by_cases hq : q = 0; · simp [hq]
      by_cases hpq : p + q = 0
      · simp only [hpq, hp, hq, if_true, if_false]
        exact add_nonneg (pow_pos _).le (pow_pos _).le
      simp only [hpq, hp, hq, if_false]
      exact le_trans (pow_right_mono₀ (by lia) (Polynomial.natDegree_add_le _ _)) (by grind)

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
e : HahnEmbedding.Partial h.some
hdomain : (↑e).domain = ⊤
harch : ∀ (x : ↥(↑e).domain), (withTopOrderIso M) (ofLex (↑↑e x)).orderTop = ArchimedeanClass.mk ↑x
⊢ ∃ f, StrictMono ⇑f ∧ ∀ (a : M), ArchimedeanClass.mk a = (withTopOrderIso M) (ofLex (f a)).orderTop

Tactic:
obtain ⟨⟨fdomain, f⟩, hpartial⟩ := e

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
fdomain : Submodule K M
f : ↥fdomain →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h.some { domain := fdomain, toFun := f }
hdomain : (↑⟨{ domain := fdomain, toFun := f }, hpartial⟩).domain = ⊤
harch :
  ∀ (x : ↥(↑⟨{ domain := fdomain, toFun := f }, hpartial⟩).domain),
    (withTopOrderIso M) (ofLex (↑↑⟨{ domain := fdomain, toFun := f }, hpartial⟩ x)).orderTop = ArchimedeanClass.mk ↑x
⊢ ∃ f, StrictMono ⇑f ∧ ∀ (a : M), ArchimedeanClass.mk a = (withTopOrderIso M) (ofLex (f a)).orderTop
Module: Mathlib.Algebra.Polynomial.Eval.Irreducible

Goal state before:
pp: case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ b.leadingCoeff * ?refine_2.b = 1

Tactic:
mul_comm

Goal state after:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ ?h.b * b.leadingCoeff = 1

case h.b
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ R
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ i r * i a ^ n * i b ^ (N - n) = i b ^ N * (i r * (i a * bi) ^ n)

Tactic:
mul_comm

Goal state after:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ i b ^ (N - n) * (i r * i a ^ n) = i b ^ N * (i r * (i a * bi) ^ n)
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: case e_a.e_a.e_x.e_a.refine_1
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b * bg = 1

Tactic:
mul_comm

Goal state after:
case e_a.e_a.e_x.e_a.refine_1
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ bg * i b = 1
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: case e_a.e_a.e_x.e_a.refine_2
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b * bf = 1

Tactic:
mul_comm

Goal state after:
case e_a.e_a.e_x.e_a.refine_2
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ bf * i b = 1
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
⊢ destutter' R a [b] = if R a b then [a, b] else [a]

Tactic:
split_ifs with h <;> simp! [h]

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

Goal state before:
pp: case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
obtain hac | hac : R a c ∨ Rᶜ a c := em _

Goal state after:
case neg.inl
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_3
inst✝ : Semiring R
r : R
⊢ ∀ (x : R[X]), (leval r) x = (smeval.linearMap R r) x

Tactic:
intro

Goal state after:
R : Type u_3
inst✝ : Semiring R
r : R
x✝ : R[X]
⊢ (leval r) x✝ = (smeval.linearMap R r) x✝
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ q.smeval (-↑n) = ↑(q.smeval (-↑n))

Tactic:
by
  rw [smeval_eq_sum, smeval_eq_sum]
  simp only [Polynomial.smul_pow, sum_def]
  simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : ¬P = 0
⊢ P.nextCoeff ≠ 0

Tactic:
intro

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : ¬P = 0
a✝ : P.nextCoeff = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
⊢ ∃ c₀ cs,
    ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧ ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs

Tactic:
have h₄ := natDegree_eraseLead_add_one h₂

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
⊢ ∃ c₀ cs,
    ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧ ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
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:
trans ((X - C η) * P).eraseLead.signVariations + 1
    · grind [signVariations_eraseLead_mul_X_sub_C, sign_eq_neg_one_iff]
    · suffices SignType.sign ((X - C η) * P).nextCoeff = -1 by
        simp +decide [signVariations_eq_eraseLead_add_ite h_mul, h_lC,
          leadingCoeff_eraseLead_eq_nextCoeff, ← sign_eq_zero_iff, this]
      grind [← sign_eq_neg_one_iff, coeff_X_sub_C_mul, nextCoeff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
h₂ : s₂ ≠ 0
⊢ False

Tactic:
rw [← isSumNonzeroSq_iff_isSumSq h₁] at hs₁

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumNonzeroSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
h₂ : s₂ ≠ 0
⊢ False
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p f

Tactic:
suffices p (single a (f.coeff a) + f.erase a) by rwa [single_add_erase] at this

Goal state after:
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p (single a (f.coeff a) + (erase a) f)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X * p = (p.sum fun a b ↦ (monomial a) (φ b)) * X

Tactic:
by
  simp only [X, mul_def]
  rw [sum_monomial_index (by simp), sum_sum_index (by simp) (by simp)]
  simp [add_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p * 1 = q

Tactic:
← mul_one q,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p * 1 = q * 1
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α β : X ⟶ Y
w : α.hom.base = β.hom.base
⊢ (Opens.map α.hom.base).op = (Opens.map β.hom.base).op

Tactic:
by rw [w]

Goal state after:
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:
by
  -- We can't use `ext` here because it would call `stalk_hom_ext` instead.
  refine colimit.hom_ext fun V => ?_
  induction V with | op V => ?_
  let i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
    homOfLE (Set.image_preimage_subset f _)
  erw [Iso.comp_inv_eq, colimit.ι_map_assoc, colimit.ι_map_assoc, colimit.ι_pre]
  simp_rw [Category.assoc]
  erw [colimit.ι_pre ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf)
      (h.functorNhds x).op]
  erw [← X.presheaf.map_comp_assoc]
  exact (colimit.w ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) i.op).symm

Goal state after:
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
⊢ IsIso (X.restrictStalkIso h x).inv

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X.Hom Y
w : α.base = β.base
⊢ (Opens.map α.base).op = (Opens.map β.base).op

Tactic:
by rw [w]

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * (ConcreteCategory.hom (X.presheaf.germ V x hxV)) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
⊢ (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1

Tactic:
rwa [map_mul, map_one, X.presheaf.germ_res_apply (Opens.infLELeft U V) x hxW f,
      X.presheaf.germ_res_apply (Opens.infLERight U V) x hxW g]

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

Goal state before:
pp: J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
⊢ ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map (f ≫ g)).c ≫
        (Pushforward.comp ((F ⋙ forget C).map (f ≫ g)) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₁).presheaf).inv ≫
          (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op =
    ((pushforward C (colimit.ι (F ⋙ forget C) j₂)).map (F.map f).c ≫
          (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j₂) (F.obj j₁).presheaf).inv ≫
            (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op ≫
      ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map g).c ≫
          (Pushforward.comp ((F ⋙ forget C).map g) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₂).presheaf).inv ≫
            (pushforwardEq ⋯ (F.obj j₂).presheaf).hom).op

Tactic:
by
    apply (opEquiv _ _).injective
    refine NatTrans.ext (funext fun U => ?_)
    dsimp [opEquiv]
    have :
      op ((Opens.map (F.map g).base).obj
          ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj U.unop)) =
        op ((Opens.map (colimit.ι (F ⋙ PresheafedSpace.forget C) j₂)).obj (unop U)) := by
      apply unop_injective
      rw [← Opens.map_comp_obj]
      congr
      exact colimit.w (F ⋙ PresheafedSpace.forget C) g
    simp only [map_comp_c_app, pushforward_obj_obj, pushforward_map_app, comp_base,
      pushforwardEq_hom_app, op_obj, Opens.map_comp_obj, id_comp, assoc, eqToHom_map_comp,
      NatTrans.naturality_assoc, pushforward_obj_map, eqToHom_unop]
    simp [NatTrans.congr (α := (F.map f).c) this]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X ⟶ Y
w : α.base = β.base
⊢ (Opens.map α.base).op = (Opens.map β.base).op

Tactic:
by rw [w]

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

Goal state before:
pp: X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x)))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
r : ↑R
U : TopologicalSpace.Opens (PrimeSpectrum ↑R) := PrimeSpectrum.basicOpen r
⊢ (TopologicalSpace.Opens.map α.hom.base).op.obj (op U) = (TopologicalSpace.Opens.map β.hom.base).op.obj (op U)

Tactic:
by rw [w]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ (CommRingCat.Hom.hom
        (((stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).toRingEquiv.toCommRingCatIso.symm.inv ≫
            PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p) ≫
          (stalkIso (↑S) p).toRingEquiv.toCommRingCatIso.symm.hom))
      ((algebraMap (↑R) (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal)) x) =
    (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) ((CommRingCat.Hom.hom f) x)

Tactic:
dsimp [-RingEquiv.symm_mk]

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ (stalkIso (↑S) p).toRingEquiv.symm
      ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p))
        ((stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p))
          ((algebraMap (↑R) (Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal))) x))) =
    (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) ((CommRingCat.Hom.hom f) x)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom

Tactic:
infer_instance

Goal state after:
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 : Opens ↑↑X
⊢ IsIso (f.c.app (op ((opensFunctor f).obj U)))

Tactic:
infer_instance

Goal state after:
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 : Opens ↑↑X
⊢ IsIso (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U))))

Tactic:
infer_instance

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

Goal state before:
pp: case convert_2
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ IsIso (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: 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ᶜ

Tactic:
simp [Set.compl_inter, ← Set.union_iInter₂, ← Set.iInter₂_union]

Goal state after:
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
inst✝ : HasColimits C
x : ↑↑X
⊢ IsIso
    (Hom.stalkMap (Y.ofRestrict ⋯) ((ConcreteCategory.hom (isoRestrict f).hom.base) x) ≫
      Hom.stalkMap (isoRestrict f).hom x)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ PreservesLimitsOfShape WalkingCospan (LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ IsIso (app f ((LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f)).obj U))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ opensRange f
⊢ IsIso (app f (f ''ᵁ f ⁻¹ᵁ V))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
e :
  (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
      (algebraMap R (Localization.Away f)) =
    algebraMap R S
H : IsIso (CommRingCat.ofHom ↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm)
⊢ IsOpenImmersion
    (Spec.map (CommRingCat.ofHom ↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm) ≫
      Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))

Tactic:
infer_instance

Goal state after:
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
    (have this := ⋯;
    inv (pullback.snd (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom') ≫
      pullback.fst (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom')

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ PresheafedSpace.IsOpenImmersion (X.ofRestrict h)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)

Tactic:
← Scheme.Hom.stalkMap_comp

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap (f ≫ g) x)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap (f ≫ g) x)

Tactic:
infer_instance

Goal state after: