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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
⊢ (monomial n) r * (monomial 1) 1 = (monomial (n + 1)) r

Tactic:
monomial_mul_monomial,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
⊢ (monomial (n + 1)) (r * (⇑φ)^[n] 1) = (monomial (n + 1)) r
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ (monomial n) a * (monomial 1) 1 = (monomial (n + 1)) a

Tactic:
monomial_mul_monomial,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ (monomial (n + 1)) (a * (⇑φ)^[n] 1) = (monomial (n + 1)) a
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

Tactic:
by
    induction f with
    | single x a => induction g with
      | single y b => induction h with
        | single z c => simp [mul_assoc, mul_smul, mul_def]
        | add => simp_all [mul_add]
      | add => simp_all [add_mul, mul_add]
    | add => simp_all [add_mul]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b * (a * a) = a * (b * (a * a))

Tactic:
have commute_half_left := fun a : α => by
      have := (Commute.one_left a).add_left (Commute.one_left a)
      rw [one_add_one_eq_two] at this
      exact this.invOf_left.eq

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ a * b * (a * a) = a * (b * (a * a))
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
⊢ (f * g).coeff x = ∑ᶠ (p : G × G) (_ : p ∈ {p | p.1 * p.2 = x}), f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
by
  have : ({p : G × G | p.1 * p.2 = x}
      ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite := by
    apply Set.Finite.inter_of_right
    apply Set.Finite.subset (Finset.finite_toSet ((f.support).product (g.support)))
    aesop
  rw [← finsum_mem_inter_support, finsum_mem_eq_finite_toFinset_sum _ this]
  classical
  let s := Set.Finite.toFinset (s := ({p : G × G | p.1 * p.2 = x}
    ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2)) this
  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 := by
        apply Finset.sum_congr_of_eq_on_inter <;> aesop
    _ = ∑ 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.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
⊢ Function.Injective ⇑coeff

Tactic:
by
  intro _ _ h
  ext v n
  exact congrFun (congrArg DFunLike.coe (congrFun h n)) v

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ Hom.stalkMap (𝟙 X) x = 𝟙 (X.presheaf.stalk x)

Tactic:
dsimp [Hom.stalkMap]
  ext
  simp

Goal state after:
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
ic : IsCompatible (sheaf X).obj V g
gl : ↑(X.presheaf.obj (op U))
gl_spec : ∀ (i : ↥U), (ConcreteCategory.hom ((sheaf X).obj.map (iVU i).op)) gl = g i
i : ↥U
⊢ (CommRingCat.Hom.hom ((sheaf X).obj.map (iVU i).op)) (f * gl) =
    (ConcreteCategory.hom ((sheaf X).obj.map (iVU i).op)) 1

Tactic:
rw [map_one, map_mul, gl_spec]

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
ic : IsCompatible (sheaf X).obj V g
gl : ↑(X.presheaf.obj (op U))
gl_spec : ∀ (i : ↥U), (ConcreteCategory.hom ((sheaf X).obj.map (iVU i).op)) gl = g i
i : ↥U
⊢ (CommRingCat.Hom.hom ((sheaf X).obj.map (iVU i).op)) f * g i = 1
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case e'_5
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
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op ≍ Y.presheaf.map (𝟙 (op (hf.functor.obj U)))

Tactic:
congr
      · simp only
        congr
      apply Subsingleton.helim
      rw [this]

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
R : CommRingCat
f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X
h₁ : x ∈ Set.range ⇑(ConcreteCategory.hom f.base)
h₂ : IsOpenImmersion f
⊢ SheafedSpace.forgetToPresheafedSpace.obj (X.restrict ⋯).toSheafedSpace ≅
    SheafedSpace.forgetToPresheafedSpace.obj (Spec.toLocallyRingedSpace.obj (op R)).toSheafedSpace

Tactic:
apply PresheafedSpace.IsOpenImmersion.isoOfRangeEq (PresheafedSpace.ofRestrict _ _) f.1

Goal state after:
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
R : CommRingCat
f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X
h₁ : x ∈ Set.range ⇑(ConcreteCategory.hom f.base)
h₂ : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom (X.ofRestrict ⋯).base) = Set.range ⇑(ConcreteCategory.hom f.base)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings Y

Tactic:
rw [Precoverage.mem_comap_iff, Presieve.map_ofArrows,
      Types.ofArrows_mem_jointlySurjectivePrecoverage_iff] at hf ⊢

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ∀ (x : (fun X ↦ X) (F.obj Y)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U

Tactic:
Scheme.Hom.comp_base,

Goal state after:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈
      Set.range
        ⇑(ConcreteCategory.hom
            ((Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))).base ≫
              { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }.base)) ∧
    Set.range
        ⇑(ConcreteCategory.hom
            ((Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))).base ≫
              { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }.base)) ⊆
      ↑U
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this✝ : HasPullback g (f i)
this : F.map (p₁ i) = F.map ⋯.isoPullback.hom ≫ pullbackComparison F g (f i) ≫ pullback.fst (F.map g) (F.map (f i))
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst (F.map g) (F.map (f i))))

Tactic:
Types.range_pullbackFst

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this✝ : HasPullback g (f i)
this : F.map (p₁ i) = F.map ⋯.isoPullback.hom ≫ pullbackComparison F g (f i) ≫ pullback.fst (F.map g) (F.map (f i))
⊢ x ∈ ⇑(ConcreteCategory.hom (F.map g)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(pullback.snd f g ≫ g) = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
Scheme.Hom.comp_base,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom ((pullback.snd f g).base ≫ g.base)) = Set.range ⇑f ∩ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(pullback.fst g f ≫ g) = Set.range ⇑g ∩ Set.range ⇑f

Tactic:
Scheme.Hom.comp_base,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom ((pullback.fst g f).base ≫ g.base)) = Set.range ⇑g ∩ Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case e'_7
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ lift g f H = ?convert_2 ≫ 𝟙 U

pp: case e'_10
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ f = ?convert_2 ≫ g

pp: case convert_2
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ X ⟶ U

Tactic:
· exact (Category.comp_id _).symm

Goal state after:
case e'_10
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ f = lift g f H ≫ g
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ X.homOfLE ⋯ ≫ U.ι = 𝟙 ↑U ≫ U.ι

Tactic:
Scheme.homOfLE_ι,

Goal state after:
X : Scheme
U : X.Opens
⊢ U.ι = 𝟙 ↑U ≫ U.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ ≫ W.ι = X.homOfLE ⋯ ≫ W.ι

Tactic:
Scheme.homOfLE_ι,

Goal state after:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ X.homOfLE e₁ ≫ V.ι = X.homOfLE ⋯ ≫ W.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ X.homOfLE e₁ ≫ V.ι = X.homOfLE ⋯ ≫ W.ι

Tactic:
Scheme.homOfLE_ι,

Goal state after:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ U.ι = X.homOfLE ⋯ ≫ W.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ Set.range ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι) = Set.range ⇑U.ι

Tactic:
Scheme.Hom.comp_base,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ Set.range ⇑(ConcreteCategory.hom ((V.ι ⁻¹ᵁ U).ι.base ≫ V.ι.base)) = Set.range ⇑U.ι
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case e'_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i j : ↥t
⊢ g ↑i ^ (N + 1) • g ↑j ^ N • f ↑j = (g ↑i * g ↑j) ^ N • g ↑i • f ↑j

pp: case refine_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i j : ↥t
⊢ (g ↑i * g ↑j) ^ N • g ↑j • f ↑i = (g ↑i * g ↑j) ^ N • g ↑i • f ↑j

Tactic:
· module

Goal state after:
case refine_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i j : ↥t
⊢ (g ↑i * g ↑j) ^ N • g ↑j • f ↑i = (g ↑i * g ↑j) ^ N • g ↑i • f ↑j
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
⊢ s.fst ≫ f = s.fst ≫ g

Tactic:
have H₂ : s.fst ≫ g = s.snd := by simpa using congr($s.condition ≫ prod.snd)

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
H₂ : s.fst ≫ g = s.snd
⊢ s.fst ≫ f = s.fst ≫ g
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appLE f U V i) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (Scheme.Hom.appTop (X.homOfLE i ≫ f ∣_ U) ≫ X.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι

Tactic:
Scheme.Hom.comp_appTop,

Goal state after:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appLE f U V i) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map ((Scheme.Hom.appTop (f ∣_ U) ≫ Scheme.Hom.appTop (X.homOfLE i)) ≫ X.presheaf.map (eqToHom ⋯).op) ≫
      (↑U).isoSpec.inv ≫ U.ι
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (IsLocalizedModule.lift (Ideal.comap σ y.asIdeal).primeCompl
        (LocalizedModule.mkLinearMap (Ideal.comap σ y.asIdeal).primeCompl M)
        (↑R (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ }) ⋯)
      (LocalizedModule.mk a 1) =
    σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

Tactic:
refine (IsLocalizedModule.lift_apply ..).trans ?_

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (↑R (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ }) a =
    σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
⊢ ∀ {x y : (i : D.J) × ↑(D.U i)}, D.Rel x y → D.Rel y x

Tactic:
by
    rintro a b ⟨x, e₁, e₂⟩
    exact ⟨D.t _ _ x, e₂, by rw [← e₁, D.t_inv_apply]⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Tactic:
simp only [Opens.iSup_def, Set.preimage_iUnion]
      congr! 1
      · refine congr_arg (Set.iUnion ·) ?_
        ext1 x
        exact congr_arg Opens.carrier (hU.fromSpec_preimage_basicOpen _)
      · exact congr_arg Opens.carrier hU.fromSpec_preimage_self

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_2
R S : CommRingCat
f : R ⟶ S
r : ↑R
⊢ (Arrow.mk (Spec.map f ∣_ basicOpen r)).right ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).right

Tactic:
exact basicOpenIsoSpecAway r

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
this : (Opens.map f.base).obj (imageBasicOpen f g U s) = (Opens.map g.base).obj (imageBasicOpen f g U s)
⊢ ⇑(ConcreteCategory.hom (↾⇑(ConcreteCategory.hom f.base))) ⁻¹' (imageBasicOpen f g U s).carrier =
    ⇑(ConcreteCategory.hom (↾⇑(ConcreteCategory.hom g.base))) ⁻¹' (imageBasicOpen f g U s).carrier

Tactic:
by injection this

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑X.isoSpec.inv ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
rw [← toSpecΓ_preimage_zeroLocus, ← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base,
    X.isoSpec_inv_toSpecΓ]
  rfl

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U ⊆ Set.range ⇑(ConcreteCategory.hom (D.f j i))

Tactic:
← D.preimage_range i j

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U ⊆
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.ι i))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π
y : ↑↑Y.toPresheafedSpace
h : ↑(s.pt.presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.desc (Hom.toShHom s.π) e).hom.base)
        ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y))) →+*
  ↑((coequalizerCofork f g).pt.presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y)) :=
  CommRingCat.Hom.hom
    (PresheafedSpace.Hom.stalkMap (coequalizer.desc (Hom.toShHom s.π) e).hom
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y))
x✝ : IsLocalHom ((CommRingCat.Hom.hom ((coequalizerCofork f g).π.stalkMap y)).comp h)
⊢ IsLocalHom h

Tactic:
by
    apply isLocalHom_of_comp _ ((coequalizerCofork f g).π.1.stalkMap _).hom

Goal state after: