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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f + g).sum h = f.sum h + g.sum h

Tactic:
by
  rw [show f + g = ⟨f.coeff + g.coeff⟩ by rw [ofCoeff_add, eta]]
  exact Finsupp.sum_add_index h_zero h_add

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

Goal state before:
pp: α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.sum g).sum h = f.sum fun a b ↦ (g a b).sum h

Tactic:
sum_def,

Goal state after:
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.sum g).coeff.sum h = f.sum fun a b ↦ (g a b).sum h
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
a₂ : G'
⊢ (f.coeff.sum fun x1 x2 ↦ (g x1 x2).coeff) a₂ = f.sum fun a₁ b ↦ (g a₁ b).coeff a₂

Tactic:
sum_def,

Goal state after:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
a₂ : G'
⊢ (f.coeff.sum fun x1 x2 ↦ (g x1 x2).coeff) a₂ = f.coeff.sum fun a₁ b ↦ (g a₁ b).coeff a₂
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ ∀ x ∈ f.support, p (SkewMonoidAlgebra.single x (f.coeff x))

Tactic:
simp_all

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

Goal state before:
pp: case zero
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
M : Type u_3
inst✝ : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h : ∀ (a : G) (b : k), f (single a b) = g (single a b)
⊢ f 0 = g 0

Tactic:
simp_all

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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
M : Type u_3
inst✝ : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h : ∀ (a : G) (b : k), f (single a b) = g (single a b)
g✝ : G
a✝ : k
⊢ f (single g✝ a✝) = g (single g✝ a✝)

Tactic:
simp_all

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

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
M : Type u_3
inst✝ : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h : ∀ (a : G) (b : k), f (single a b) = g (single a b)
f✝ g✝ : SkewMonoidAlgebra k G
a✝¹ : f f✝ = g f✝
a✝ : f g✝ = g g✝
⊢ f (f✝ + g✝) = g (f✝ + g✝)

Tactic:
simp_all

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
f : k →+ R
g : G → R
l : SkewMonoidAlgebra k G →+ R
h : ∀ (a : G) (b : k), l (single a b) = f b * g a
a : G
b : k
⊢ l (single a b) = (liftNC f g) (single a b)

Tactic:
simp_all

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

Goal state before:
pp: case single.single.add
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
x : G
a : k
y : G
b : k
f✝ g✝ : SkewMonoidAlgebra k G
a✝¹ : single x a * single y b * f✝ = single x a * (single y b * f✝)
a✝ : single x a * single y b * g✝ = single x a * (single y b * g✝)
⊢ single x a * single y b * (f✝ + g✝) = single x a * (single y b * (f✝ + g✝))

Tactic:
| add =>

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

Goal state before:
pp: case single.add
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
h : SkewMonoidAlgebra k G
x : G
a : k
f✝ g✝ : SkewMonoidAlgebra k G
a✝¹ : single x a * f✝ * h = single x a * (f✝ * h)
a✝ : single x a * g✝ * h = single x a * (g✝ * h)
⊢ single x a * (f✝ + g✝) * h = single x a * ((f✝ + g✝) * h)

Tactic:
| add =>

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

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g h : SkewMonoidAlgebra k G
f✝ g✝ : SkewMonoidAlgebra k G
a✝¹ : f✝ * g * h = f✝ * (g * h)
a✝ : g✝ * g * h = g✝ * (g * h)
⊢ (f✝ + g✝) * g * h = (f✝ + g✝) * (g * h)

Tactic:
| add =>

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

Goal state before:
pp: case pos
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 × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
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 × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : ¬f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
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
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
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
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
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
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
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
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : ¬f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_4
m : Type u_5
n : Type u_6
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n m R
⊢ star (toConv (toLin' A)) = toConv (toLin' (A.map star))

Tactic:
by
  simp [← LinearMap.toMatrix'.injective.eq_iff, LinearMap.toMatrix'_intrinsicStar, WithConv.ext_iff]

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

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : 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
u : U
⊢ (Function.support fun g' ↦ A ((coeff B g') u)).IsPWO

Tactic:
refine Set.IsPWO.mono (((of R).symm (B u)).isPWO_support') ?_

Goal state after:
Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : 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
u : U
⊢ (Function.support fun g' ↦ A ((coeff B g') u)) ⊆ Function.support ((of R).symm (B u)).coeff
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 c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : c ≫ whiskerRight (𝟙 (Opens.map base).op) X.presheaf = c'
⊢ { base := base, c := c } = { base := base, c := c' }

Tactic:
erw [whiskerRight_id', comp_id] at h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : c = c'
⊢ { base := base, c := c } = { base := base, c := c' }
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
eq₁ : (H.hom ≫ H.inv).c.app (op ((Opens.map H.hom.base).obj U)) = eqToHom ⋯
eq₂ :
  Y.presheaf.map (eqToHom ⋯).op ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯).op
⊢ 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:
comp_c_app

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.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫
      H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) =
    eqToHom ⋯
eq₂ :
  Y.presheaf.map (eqToHom ⋯).op ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯).op
⊢ 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.Basic

Goal state before:
pp: case succ
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 0 < n + Nat.succ 0 → X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
⊢ X.basicOpen (f ^ (n + 1) * f ^ Nat.succ 0) = X.basicOpen f

Tactic:
simp_all

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

Goal state before:
pp: case app.op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
carrier✝ : Set ↑↑(Y.restrict ⋯)
is_open'✝ : IsOpen carrier✝
⊢ ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑((opensFunctor f).obj { carrier := carrier✝, is_open' := is_open'✝ }) = carrier✝

Tactic:
erw [Set.preimage_image_eq _ H.base_open.injective]

Goal state after:
case app.op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
carrier✝ : Set ↑↑(Y.restrict ⋯)
is_open'✝ : IsOpen carrier✝
⊢ ↑{ carrier := carrier✝, is_open' := is_open'✝ } = carrier✝
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ autoParam
    (∀ {X_1 Y_1 : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ} (f_1 : X_1 ⟶ Y_1),
      (Y.restrict ⋯).presheaf.map f_1 ≫
          (asIso (f.c.app (op ((opensFunctor f).obj (unop Y_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom =
        (asIso (f.c.app (op ((opensFunctor f).obj (unop X_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom ≫
          ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map f_1)
    NatIso.ofComponents._auto_1

Tactic:
· intro U V i
      dsimp
      simp only [NatTrans.naturality_assoc, TopCat.Presheaf.pushforward_obj_obj,
        TopCat.Presheaf.pushforward_obj_map, Quiver.Hom.unop_op, Category.assoc]
      rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]
      congr 1

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
x : (Opens ↑↑Y)ᵒᵖ
⊢ (((isoRestrict f).hom ≫ Y.ofRestrict ⋯).c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app x = f.c.app x

Tactic:
simp only [eqToHom_refl,
    Functor.whiskerRight_id']

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ (((isoRestrict f).hom ≫ Y.ofRestrict ⋯).c ≫
          𝟙 ((Opens.map ((isoRestrict f).hom ≫ Y.ofRestrict ⋯).base).op ⋙ X.presheaf)).app
      x =
    f.c.app x
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑Γ(Spec R, ⊤)
⊢ (Spec R).basicOpen f = PrimeSpectrum.basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) f)

Tactic:
convert! basicOpen_eq_of_affine ((Scheme.ΓSpecIso R).hom f)
  exact (Iso.hom_inv_id_apply (Scheme.ΓSpecIso R) f).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : LocallyRingedSpace
h : ∀ (x : ↑X.toTopCat), ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ IsOpenImmersion f
⊢ ∀ (x : ↑X.toTopCat), ∃ U R, Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))

Tactic:
intro x
    obtain ⟨R, f, h₁, h₂⟩ := h x
    refine ⟨⟨⟨_, h₂.base_open.isOpen_range⟩, h₁⟩, R, ⟨?_⟩⟩
    apply LocallyRingedSpace.isoOfSheafedSpaceIso
    refine SheafedSpace.forgetToPresheafedSpace.preimageIso ?_
    apply PresheafedSpace.IsOpenImmersion.isoOfRangeEq (PresheafedSpace.ofRestrict _ _) f.1
    exact Subtype.range_coe_subtype

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 V)

Tactic:
rw [show V = f ''ᵁ f ⁻¹ᵁ V from Opens.ext (Set.image_preimage_eq_of_subset hV).symm]

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ opensRange f
⊢ IsIso (app f (f ''ᵁ f ⁻¹ᵁ V))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsLimit (pullbackConeOfLeft f g)

Tactic:
apply PullbackCone.isLimitAux'
  intro s
  use pullbackConeOfLeftLift f g s
  use pullbackConeOfLeftLift_fst f g s
  use pullbackConeOfLeftLift_snd f g s
  intro m _ h₂
  rw [← cancel_mono (pullbackConeOfLeft f g).snd]
  exact h₂.trans (pullbackConeOfLeftLift_snd f g s).symm

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

Goal state before:
pp: case right
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
X : Scheme
R : Presieve X
x✝ : R ∈ (precoverage P).coverings X
x : ↥X
hR : ∀ (x : forget.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (forget.map f))
right✝ : R ∈ P.precoverage.coverings X
Y : Scheme
g : Y ⟶ X
hg : R g
heq : x ∈ Set.range ⇑(ConcreteCategory.hom (forget.map g))
⊢ x ∈ Set.range ⇑g

Tactic:
exact heq

Goal state after:
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]

Goal state after:
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)
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑(𝒰.f i)) ∧ ∀ (i : 𝒰.I₀), Q (𝒰.f i)
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✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ { I₀ := J, X := obj, f := map }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
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✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := obj, f := map }.f i)) ∧
    ∀ (i : { I₀ := J, X := obj, f := map }.I₀), P ({ I₀ := J, X := obj, f := map }.f i)
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
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ (𝒰.add f).presieve₀ ∈ (precoverage P).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
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
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑((𝒰.add f).f i)) ∧ ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)
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
X : Scheme
𝒰 : AffineCover P X
⊢ { I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
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
X : Scheme
𝒰 : AffineCover P X
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)) ∧
    ∀ (i : { I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.I₀),
      P ({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
fg : Y ⟶ X
H : fg = f ≫ g
h : IsOpenImmersion g
V : U.Opens
⊢ f ⁻¹ᵁ V = fg ⁻¹ᵁ g ''ᵁ V

Tactic:
simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
fg : Y ⟶ X
H : fg = f ≫ g
h : IsOpenImmersion g
V : U.Opens
⊢ f ⁻¹ᵁ V = fg ⁻¹ᵁ g ''ᵁ V

Tactic:
by
  simp_all

Goal state after:
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
𝒰 : Cover (precoverage P) X
⊢ { I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
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
𝒰 : Cover (precoverage P) X
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.f i)) ∧
    ∀ (i : { I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.I₀),
      P ({ I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.f i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ (Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv) ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op

Tactic:
simp [-ΓIso_inv]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X✝ Y Z : Scheme
𝒰 : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
⊢ { I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
X✝ Y Z : Scheme
𝒰 : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
⊢ (∀ (x : ↥X),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.f i)) ∧
    ∀ (i : { I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.I₀),
      IsOpenImmersion
        ({ I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.f i)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
h : ∀ (x : ↥X), ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))
⊢ { I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x) }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
h : ∀ (x : ↥X), ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))
⊢ (∀ (x : ↥X),
      ∃ i, x ∈ Set.range ⇑({ I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x) }.f i)) ∧
    ∀ (i : { I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x) }.I₀),
      IsOpenImmersion ({ I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x) }.f i)