mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
⊢ (f.update a b).coeff x = ((erase a) f + single a b).coeff x

Tactic:
by_cases hx : x = a

Goal state after:
case pos
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
hx : x = a
⊢ (f.update a b).coeff x = ((erase a) f + single a b).coeff x

case neg
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
hx : ¬x = a
⊢ (f.update a b).coeff x = ((erase a) f + single a b).coeff x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
⊢ f.update a b = (erase a) f + single a b

Tactic:
ext x; by_cases hx : x = a <;> aesop (add norm coeff_single_apply)

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
x : R
⊢ ({
          toFun := fun f ↦
            { toFun := fun x ↦ Quot.lift ⇑↑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
          invFun := fun F ↦
            ⟨F.comp
                { toFun := fun x ↦ { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ({ toFun := fun x ↦ { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
        x) =
    f x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ ({
          toFun := fun f ↦
            { toFun := fun x ↦ Quot.lift ⇑↑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
          invFun := fun F ↦
            ⟨F.comp
                { toFun := fun x ↦ { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨Ideal.Quotient.mk (Ideal.ofRel r), ⋯⟩)
      ({ toFun := fun x ↦ { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
        x) =
    (Ideal.Quotient.mk (Ideal.ofRel r)) x

Tactic:
rfl

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
s : A → A → Prop
x✝ : S
⊢ { toQuot := Quot.mk (Rel s) ((algebraMap S A) x✝) } = (algebraMap S (RingQuot s)) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ ↑{ toFun := fun x ↦ { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
        commutes' := ⋯ } =
    { toFun := fun x ↦ { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
x : A
⊢ ({
          toFun := fun f' ↦
            { toFun := fun x ↦ Quot.lift ⇑↑f' ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
              commutes' := ⋯ },
          invFun := fun F ↦
            ⟨F.comp
                { toFun := fun x ↦ { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯, commutes' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ({ toFun := fun x ↦ { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
          commutes' := ⋯ }
        x) =
    f x

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ A₁ * B₁ + (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + √2 ^ 3 • 1))) =
    A₁ * B₁ + (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + (2 * (√2)⁻¹ + 4 * ((√2)⁻¹ * 2⁻¹)) • 1)))

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝¹ : Semiring R
a b : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (monomial n) a * C b = (monomial n) (a * (⇑φ)^[n] b)

Tactic:
by
  simp [← monomial_zero_left, monomial_mul_monomial, add_zero]

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

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

Tactic:
by simp only [star_add, map_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
x✝ : ℕ
⊢ Function.update (⇑p.coeff) (ofAdd n) a (ofAdd x✝) = Function.update p.coeff n a x✝

Tactic:
rfl

Goal state after:
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)
x✝ : ∃ α, u = α • v
y : ↥(unitary S)
h : u = y • v
⊢ ↑y • 1 = y • 1

Tactic:
rfl

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : FaithfulSMul S k
inst✝ : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
a : G →₀ k
⊢ { coeff := _s₁ • a } = { coeff := _s₂ • a }

Tactic:
simp_rw [ofCoeff_smul, h]

Goal state after:
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
r : R
m : M
hr : r = 0
⊢ (0, m) = inr (snd (0, m))

Tactic:
rfl

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
⊢ (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
classical
  let F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
  calc
    (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
    _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product]
    _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x,
      f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm
    _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support,
      f.coeff p.1 * p.1 • g.coeff p.2 :=
      (Finset.sum_congr (by ext; simp [Finset.mem_filter, Finset.mem_product, hs, and_comm])
        fun _ _ ↦ rfl)
    _ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
      Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦ by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

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

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ ∏ i ∈ s, trop (f i) = (Multiset.map (fun i ↦ trop (f i)) s.val).prod

Tactic:
rfl

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

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i ∈ s, untrop (f i) = (Multiset.map (fun i ↦ untrop (f i)) s.val).sum

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
⊢ ?m.16 a

Tactic:
have := (Commute.one_left a).add_left (Commute.one_left a)

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute (1 + 1) a
⊢ ?m.16 a
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i ∈ s, trop (f i) = (Multiset.map (fun i ↦ trop (f i)) s.val).sum

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ sInf (untrop ∘ f '' ↑univ) = sInf ((fun i ↦ untrop (f i)) '' ↑univ)

Tactic:
Function.comp_def

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ sInf ((fun x ↦ untrop (f x)) '' ↑univ) = sInf ((fun i ↦ untrop (f i)) '' ↑univ)
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) +
          unsym (a * a) * (unsym a * unsym b + unsym b * unsym a))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))

Tactic:
mul_add (unsym (a * a)),

Goal state after:
case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) +
          (unsym (a * a) * (unsym a * unsym b) + unsym (a * a) * (unsym b * unsym a)))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case refine_2
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ (t • a.sum fun a b_1 ↦ b.sum fun a_1 b ↦ single (a * a_1) (b_1 * a • b)) = t • (a * b)

Tactic:
rfl

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
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
x : V
n : ℤ
⊢ ((HahnModule.of R).symm ((of_coeff f hf) x)).coeff n = (f n) x

Tactic:
rfl

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

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
g : Lex (Γ' × Γ)
⊢ coeff (A.comp B) g = coeff A (ofLex g).2 ∘ₗ coeff B (ofLex g).1

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map α.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U

Tactic:
rfl

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
inst✝ : HasColimit F
U : Opens ↑↑(colimit F)
j k : Jᵒᵖ
f : j ⟶ k
⊢ (Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) =
    op ((Opens.map ((F.map f.unop).base ≫ (colimit.ι F (unop j)).base)).obj U)

Tactic:
rfl

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

Goal state before:
pp: case op
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
U : Opens ↑(colimit (F ⋙ forget C))
⊢ 𝟙 ((F.obj j).presheaf.obj (op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj U))) =
    (𝟙 ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)).app (op U)

Tactic:
rfl

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
⊢ ((pushforward C (colimit.ι (F ⋙ forget C) j)).map (F.map (𝟙 j)).c ≫
        (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf).inv ≫
          (pushforwardEq ⋯ (F.obj j).presheaf).hom).op =
    𝟙 (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))

Tactic:
by
    apply (opEquiv _ _).injective
    refine NatTrans.ext (funext fun U => ?_)
    induction U with
    | op U =>
      simp [opEquiv]
      rfl

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
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
⊢ { base := base, c := c } = { base := base, c := c }

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X.presheaf).app U = 𝟙 (X.presheaf.obj U)

Tactic:
rfl

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
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U

Tactic:
rfl

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (f.toHom ≫ g.toHom) x))

Tactic:
PresheafedSpace.stalkMap.comp

Goal state after:
X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (g.stalkMap ((ConcreteCategory.hom f.base) x) ≫ f.stalkMap x))
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)
⊢ U ≤ iSup V

Tactic:
intro x hxU

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)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ x ∈ iSup V
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case refine_1
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ 0 1 = 1

Tactic:
rfl

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

Goal state before:
pp: case refine_2
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
x✝ y✝ : ↑(X.presheaf.1 U)
⊢ { toFun := 0, map_one' := ⋯ }.toFun (x✝ * y✝) =
    { toFun := 0, map_one' := ⋯ }.toFun x✝ * { toFun := 0, map_one' := ⋯ }.toFun y✝

Tactic:
rfl

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

Goal state before:
pp: case refine_3
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ }).toFun 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case refine_4
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
x✝ y✝ : ↑(X.presheaf.1 U)
⊢ (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ }).toFun (x✝ + y✝) =
    (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ }).toFun x✝ + (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ }).toFun y✝

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
U✝ : TopCat
X : PresheafedSpace C
f✝ : U✝ ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f✝)
U V : (Opens ↑↑X)ᵒᵖ
f : U ⟶ V
⊢ X.presheaf.map (f ≫ (⋯.adjunction.counit.app (unop V)).op) =
    X.presheaf.map ((⋯.adjunction.counit.app (unop U)).op ≫ h.functor.op.map ((Opens.map f✝).op.map f))

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ (Opens.map (Opens.inclusionTopIso ↑X).inv).op ⋙ X.presheaf =
    (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf

Tactic:
rfl

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

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
x✝ : ↑↑(X.restrict ⋯)
⊢ (ConcreteCategory.hom (X.ofRestrict ⋯ ≫ X.toRestrictTop).base) x✝ = (ConcreteCategory.hom (𝟙 (X.restrict ⋯)).base) x✝

Tactic:
rfl

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ (𝟙 (X.restrict ⋯).presheaf).app (op U✝) = (𝟙 (X.restrict ⋯)).c.app (op U✝)

Tactic:
rfl

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

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
x✝ : ↑↑X
⊢ (ConcreteCategory.hom (X.toRestrictTop ≫ X.ofRestrict ⋯).base) x✝ = (ConcreteCategory.hom (𝟙 X).base) x✝

Tactic:
rfl

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

Goal state before:
pp: case φ
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)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
⊢ (colimit.cocone (F ⋙ forget C)).pt ≅ ((forget C).mapCocone (colimitCocone F)).pt

Tactic:
rfl

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ (𝟙 X.presheaf).app (op U✝) = (𝟙 X).c.app (op U✝)

Tactic:
rfl

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

Goal state before:
pp: case naturality
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)
inst✝¹ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X Y : Jᵒᵖ
f : X ⟶ Y
⊢ (F.map f.unop).c.app
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U))) ≫
      (F.obj (unop Y)).presheaf.map
        ((NatIso.op
                  (Opens.mapIso ((F ⋙ forget C).map f.unop ≫ colimit.ι (F ⋙ forget C) (unop X))
                      (colimit.ι (F ⋙ forget C) (unop Y)) ⋯).symm).hom.app
            ((Opens.map
                    (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
              (op U)) ≫
          (eqToIso ⋯).hom) =
    (F.map f.unop).c.app
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U))) ≫
      (F.obj (unop Y)).presheaf.map ((Opens.map (F.map f.unop).base).op.map (eqToIso ⋯).hom ≫ eqToHom ⋯)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
x✝³ x✝² : (TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace)ᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑((sheafedSpaceObj R).presheaf.obj x✝³)
⊢ (CommRingCat.Hom.hom
        ((sheafedSpaceObj R).presheaf.map x✝¹ ≫
          CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom f) (unop x✝²) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x✝²)) ⋯)))
      x✝ =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom f) (unop x✝³) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x✝³)) ⋯) ≫
          ((TopCat.Presheaf.pushforward CommRingCat (topMap f)).obj (sheafedSpaceObj S).presheaf).map x✝¹))
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (RingHom.id ↑((structureSheaf ↑R).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))) x✝ =
    (RingHom.id ↑((structureSheaf ↑R).obj.obj (op U✝))) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (𝟙
          ((sheafedSpaceObj T).presheaf.obj
            ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).hom.base).op.obj (op U✝)))))
      ((CommRingCat.Hom.hom
          (CommRingCat.ofHom
            ((comap (CommRingCat.Hom.hom g) ?h.V ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝) ?h.hVW).comp
              (comap (CommRingCat.Hom.hom f) U✝ ?h.V ?h.hUV))))
        x✝) =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U✝))) x✝

pp: case h.V
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ TopologicalSpace.Opens ↑(PrimeSpectrum.Top ↑S)

pp: case h.hUV
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ ∀ p ∈ ?h.V, PrimeSpectrum.comap (CommRingCat.Hom.hom f) p ∈ U✝

pp: case h.hVW
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ ∀ p ∈ (TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝, PrimeSpectrum.comap (CommRingCat.Hom.hom g) p ∈ ?h.V

Tactic:
rfl

Goal state after: