mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ (F.comp (id C)).mapId ≍ F.mapId

Tactic:
rw [heq_iff_eq]

Goal state after:
case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ (F.comp (id C)).mapId = F.mapId
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ (F.comp (id C)).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor

Tactic:
rw [heq_iff_eq]

Goal state after:
case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ (F.comp (id C)).toLaxFunctor =
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver ((id B).comp F).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor

Tactic:
rw [heq_iff_eq]

Goal state after:
case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver ((id B).comp F).toPrefunctor =
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((id B).comp F).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

Tactic:
rw [heq_iff_eq]

Goal state after:
case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((id B).comp F).toPrelaxFunctorStruct =
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ ((id B).comp F).mapId ≍ F.mapId

Tactic:
rw [heq_iff_eq]

Goal state after:
case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ ((id B).comp F).mapId = F.mapId
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ ((id B).comp F).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor

Tactic:
rw [heq_iff_eq]

Goal state after:
case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ ((id B).comp F).toLaxFunctor =
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case map
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @Prefunctor.map B inst✝³.toQuiver E inst✝.toQuiver ((F.comp G).comp H).toPrefunctor ≍
    @Prefunctor.map B inst✝³.toQuiver E inst✝.toQuiver (F.comp (G.comp H)).toPrefunctor

Tactic:
rw [heq_iff_eq]

Goal state after:
case map
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @Prefunctor.map B inst✝³.toQuiver E inst✝.toQuiver ((F.comp G).comp H).toPrefunctor =
    @Prefunctor.map B inst✝³.toQuiver E inst✝.toQuiver (F.comp (G.comp H)).toPrefunctor
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case map₂
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @PrelaxFunctorStruct.map₂ B inst✝³.toQuiver (fun a b ↦ (homCategory a b).toQuiver) E inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((F.comp G).comp H).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝³.toQuiver (fun a b ↦ (homCategory a b).toQuiver) E inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) (F.comp (G.comp H)).toPrelaxFunctorStruct

Tactic:
rw [heq_iff_eq]

Goal state after:
case map₂
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @PrelaxFunctorStruct.map₂ B inst✝³.toQuiver (fun a b ↦ (homCategory a b).toQuiver) E inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((F.comp G).comp H).toPrelaxFunctorStruct =
    @PrelaxFunctorStruct.map₂ B inst✝³.toQuiver (fun a b ↦ (homCategory a b).toQuiver) E inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) (F.comp (G.comp H)).toPrelaxFunctorStruct
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapId
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ ((F.comp G).comp H).mapId ≍ (F.comp (G.comp H)).mapId

Tactic:
rw [heq_iff_eq]

Goal state after:
case mapId
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ ((F.comp G).comp H).mapId = (F.comp (G.comp H)).mapId
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapComp
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @LaxFunctor.mapComp B inst✝³ E inst✝ ((F.comp G).comp H).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝³ E inst✝ (F.comp (G.comp H)).toLaxFunctor

Tactic:
rw [heq_iff_eq]

Goal state after:
case mapComp
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @LaxFunctor.mapComp B inst✝³ E inst✝ ((F.comp G).comp H).toLaxFunctor =
    @LaxFunctor.mapComp B inst✝³ E inst✝ (F.comp (G.comp H)).toLaxFunctor
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝ R A : CommRingCat
inst✝¹ : Algebra ↑R ↑A
inst✝ : Algebra.FiniteType ↑R ↑A
⊢ LocallyOfFiniteType (Spec A ↘ Spec R)

Tactic:
specOverSpec_over,

Goal state after:
R✝ R A : CommRingCat
inst✝¹ : Algebra ↑R ↑A
inst✝ : Algebra.FiniteType ↑R ↑A
⊢ LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A)))
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≫ g ⟶ h ≫ r₂
⊢ (mateEquiv adj₁ adj₂).symm β = 𝟙 (g ≫ l₂) ⊗≫ adj₁.unit ▷ g ▷ l₂ ⊗≫ l₁ ◁ β ▷ l₂ ⊗≫ l₁ ◁ h ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ h)

Tactic:
by
  rw [mateEquiv_symm_apply, Adjunction.homEquiv₂_symm_apply, Adjunction.homEquiv₁_symm_apply]
  bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ Algebra.FormallySmooth p.ResidueField (p.Fiber ↑S)

Tactic:
rw [← RingHom.formallySmooth_algebraMap]

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ (algebraMap p.ResidueField (p.Fiber ↑S)).FormallySmooth
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case h_option
R : Type u_1
inst✝² : CommRing R
σ : Type u_3
inst✝¹ : Finite σ
α✝ : Type u_3
inst✝ : Fintype α✝
IH : ringKrullDim R + ↑(Fintype.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim R + ↑(Fintype.card α✝) + 1 ≤ ringKrullDim (MvPolynomial (Option α✝) R)

Tactic:
IH,

Goal state after:
case h_option
R : Type u_1
inst✝² : CommRing R
σ : Type u_3
inst✝¹ : Finite σ
α✝ : Type u_3
inst✝ : Fintype α✝
IH : ringKrullDim R + ↑(Fintype.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim (MvPolynomial α✝ R) + 1 ≤ ringKrullDim (MvPolynomial (Option α✝) R)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ I ≤ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker

Tactic:
have : Submodule.map (mul R R a) I = a • I := rfl
    rw [le_ker_iff_map, Submodule.map_comp, this, Submodule.mkQ_map_self]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
ih : ord R (x ^ n) = n • ord R x
⊢ ord R (x ^ (n + 1)) = (n + 1) • ord R x

Tactic:
rw [pow_succ, ord_mul, ih, succ_nsmul]

Goal state after:
case succ.hb
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
ih : ord R (x ^ n) = n • ord R x
⊢ x ∈ nonZeroDivisors R
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
⊢ ord R x = (IsDiscreteValuationRing.addVal R) x

Tactic:
obtain ⟨m, α, rfl⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hx hϖ

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ord R (↑α * ϖ ^ m) = (IsDiscreteValuationRing.addVal R) (↑α * ϖ ^ m)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₃ : l₃ ⊣ r₃
⊢ (conjugateEquiv (adj₁.comp (adj₂.comp adj₃)) ((adj₁.comp adj₂).comp adj₃)) (α_ l₁ l₂ l₃).hom = (α_ r₃ r₂ r₁).hom

Tactic:
simp [← cancel_epi (ρ_ ((r₃ ≫ r₂) ≫ r₁)).hom, ← cancel_mono (λ_ (r₃ ≫ r₂ ≫ r₁)).inv,
    conjugateEquiv_apply, mateEquiv_eq_iff, Adjunction.homEquiv₁_symm_apply,
    Adjunction.homEquiv₂_apply]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₃ : l₃ ⊣ r₃
⊢ (adj₁.unit ⊗≫
        l₁ ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₃.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₃) ≫ r₃ ≫ r₂)) ▷ r₁ ⊗≫
          𝟙 ((l₁ ≫ l₂ ≫ l₃) ≫ (r₃ ≫ r₂) ≫ r₁)) ≫
      (α_ l₁ (l₂ ≫ l₃) ((r₃ ≫ r₂) ≫ r₁)).hom ≫
        l₁ ◁ (α_ l₂ l₃ ((r₃ ≫ r₂) ≫ r₁)).hom ≫
          l₁ ◁ l₂ ◁ l₃ ◁ (α_ r₃ r₂ r₁).hom ≫
            l₁ ◁ l₂ ◁ l₃ ◁ (λ_ (r₃ ≫ r₂ ≫ r₁)).inv ≫
              l₁ ◁ (α_ l₂ l₃ (𝟙 d ≫ r₃ ≫ r₂ ≫ r₁)).inv ≫ (α_ l₁ (l₂ ≫ l₃) (𝟙 d ≫ r₃ ≫ r₂ ≫ r₁)).inv =
    ((adj₁.unit ⊗≫ l₁ ◁ adj₂.unit ▷ r₁ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ r₂ ≫ r₁)) ⊗≫
        ((α_ l₁ l₂ (𝟙 c ≫ r₂ ≫ r₁)).hom ≫
            l₁ ◁ l₂ ◁ (α_ (𝟙 c) r₂ r₁).inv ≫
              l₁ ◁ l₂ ◁ adj₃.unit ▷ r₂ ▷ r₁ ≫
                l₁ ◁ l₂ ◁ (α_ (l₃ ≫ r₃) r₂ r₁).hom ≫ (α_ l₁ l₂ ((l₃ ≫ r₃) ≫ r₂ ≫ r₁)).inv) ⊗≫
          𝟙 (((l₁ ≫ l₂) ≫ l₃) ≫ r₃ ≫ r₂ ≫ r₁)) ≫
      (λ_ (((l₁ ≫ l₂) ≫ l₃) ≫ r₃ ≫ r₂ ≫ r₁)).inv ≫
        (α_ (𝟙 a) ((l₁ ≫ l₂) ≫ l₃) (r₃ ≫ r₂ ≫ r₁)).inv ≫
          (α_ (𝟙 a ≫ (l₁ ≫ l₂) ≫ l₃) r₃ (r₂ ≫ r₁)).inv ≫
            (α_ ((𝟙 a ≫ (l₁ ≫ l₂) ≫ l₃) ≫ r₃) r₂ r₁).inv ≫
              (α_ (𝟙 a) ((l₁ ≫ l₂) ≫ l₃) r₃).hom ▷ r₂ ▷ r₁ ≫
                (α_ (𝟙 a) (((l₁ ≫ l₂) ≫ l₃) ≫ r₃) r₂).hom ▷ r₁ ≫
                  (α_ (𝟙 a) ((((l₁ ≫ l₂) ≫ l₃) ≫ r₃) ≫ r₂) r₁).hom ≫
                    (λ_ (((((l₁ ≫ l₂) ≫ l₃) ≫ r₃) ≫ r₂) ≫ r₁)).hom ≫
                      (α_ l₁ l₂ l₃).hom ▷ r₃ ▷ r₂ ▷ r₁ ≫
                        (ρ_ (l₁ ≫ l₂ ≫ l₃)).inv ▷ r₃ ▷ r₂ ▷ r₁ ≫
                          (α_ (((l₁ ≫ l₂ ≫ l₃) ≫ 𝟙 d) ≫ r₃) r₂ r₁).hom ≫
                            (α_ ((l₁ ≫ l₂ ≫ l₃) ≫ 𝟙 d) r₃ (r₂ ≫ r₁)).hom ≫ (α_ (l₁ ≫ l₂ ≫ l₃) (𝟙 d) (r₃ ≫ r₂ ≫ r₁)).hom
Module: Mathlib.RingTheory.GradedAlgebra.RingHom

Goal state before:
pp: ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
σ : Type u_6
τ : Type u_7
ψ : Type u_8
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Semiring C
inst✝² : SetLike σ A
inst✝¹ : SetLike τ B
inst✝ : SetLike ψ C
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
g : ℬ →+*ᵍ 𝒞
f₁ f₂ : 𝒜 →+*ᵍ ℬ
hg : Function.Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : A
⊢ g (f₁ x) = g (f₂ x)

Tactic:
rw [← comp_apply, h, comp_apply]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
n : ℤ
⊢ n.castDef.val = ↑n

Tactic:
cases n

Goal state after:
case ofNat
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
a✝ : ℕ
⊢ (Int.ofNat a✝).castDef.val = ↑(Int.ofNat a✝)

case negSucc
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
a✝ : ℕ
⊢ (Int.negSucc a✝).castDef.val = ↑(Int.negSucc a✝)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)
⊢ ↑f.num ∉ 𝔭

Tactic:
exact fun h ↦ mul_mem c.2 (mul_mem f.den_mem s.2)
      (hc ▸ Ideal.mul_mem_left _ c.1 (Ideal.mul_mem_right b _ h))

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
⊢ a + b ∈ carrier f_deg q

Tactic:
refine fun i => (q.2.mem_or_mem ?_).elim id id
  change (HomogeneousLocalization.mk ⟨_, _, _, _⟩ : A⁰_ f) ∈ q.1; dsimp only [Subtype.coe_mk]
  simp_rw [← pow_add, map_add, add_pow, mul_comm, ← nsmul_eq_mul]
  let g : ℕ → A⁰_ f := fun j => (m + m).choose j •
      if h2 : m + m < j then (0 : A⁰_ f)
      else
        if h1 : j ≤ m then
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i a ^ j * proj 𝒜 i b ^ (m - j), ?_⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f) *
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i b ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f)
        else
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i a ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f) *
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i a ^ (j - m) * proj 𝒜 i b ^ (m + m - j), ?_⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f)
  rotate_left
  · rw [(_ : m * i = _)]
    apply GradedMonoid.toGradedMul.mul_mem <;> mem_tac
    rw [← add_smul, Nat.add_sub_of_le h1]; rfl
  · rw [(_ : m * i = _)]
    apply GradedMonoid.toGradedMul.mul_mem (i := (j - m) • i) (j := (m + m - j) • i) <;> mem_tac
    rw [← add_smul]; congr; lia
  convert_to ∑ i ∈ range (m + m + 1), g i ∈ q.1; swap
  · refine q.1.sum_mem fun j _ => nsmul_mem ?_ _; split_ifs
    exacts [q.1.zero_mem, q.1.mul_mem_left _ (hb i), q.1.mul_mem_right _ (ha i)]
  rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk]
  change _ = (algebraMap (HomogeneousLocalization.Away 𝒜 f) (Localization.Away f)) _
  dsimp only [Subtype.coe_mk]; rw [map_sum, mk_sum]
  apply Finset.sum_congr rfl fun j hj => _
  intro j hj
  change _ = HomogeneousLocalization.val _
  rw [HomogeneousLocalization.val_smul]
  split_ifs with h2 h1
  · exact ((Finset.mem_range.1 hj).not_ge h2).elim
  all_goals simp only [HomogeneousLocalization.val_mul,
    HomogeneousLocalization.val_mk, Localization.mk_mul, ← smul_mk]; congr 2
  · dsimp; rw [mul_assoc, ← pow_add, add_comm (m - j), Nat.add_sub_assoc h1]
  · simp_rw [pow_add]; rfl
  · dsimp; rw [← mul_assoc, ← pow_add, Nat.add_sub_of_le (le_of_not_ge h1)]
  · simp_rw [pow_add]; rfl

Goal state after:
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ Function.Injective toSubring

Tactic:
rintro ⟨a, b⟩ ⟨c, d⟩ rfl; rfl

Goal state after:
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case inr
K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
this : Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv} ≠ ⊤
⊢ ∃ V, R ≤ V.toLocalSubring ∧ x ∉ V

Tactic:
have ⟨V, hV⟩ := Ideal.image_subset_nonunits_valuationSubring (A := B.toSubring) _ this

Goal state after:
case inr
K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
this : Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv} ≠ ⊤
V : ValuationSubring K
hV :
  B.toSubring ≤ V.toSubring ∧
    ⇑B.toSubring.subtype '' ↑(Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv}) ⊆
      ↑V.nonunits
⊢ ∃ V, R ≤ V.toLocalSubring ∧ x ∉ V
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: R : Type u_1
K : Type u_3
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : IsLocalRing R
f : R →+* K
B : ValuationSubring K
hB : LocalSubring.range f ≤ B.toLocalSubring
⊢ IsLocalHom (f.codRestrict B.toSubring ⋯)

Tactic:
exact @RingHom.isLocalHom_comp _ _ _ _ _ _ _ _ hB.2 (.of_surjective _ f.rangeRestrict_surjective)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
m : ι → ι → ℕ
hm :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m i j • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m i j • t j)
K : ℕ := ⨆ i, ⨆ j, m i j
i j : ι
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)

Tactic:
have : m i j ≤ K :=
        le_ciSup_of_le (Finite.bddAbove_range _) i (le_ciSup (Finite.bddAbove_range _) _)

Goal state after:
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
m : ι → ι → ℕ
hm :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m i j • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m i j • t j)
K : ℕ := ⨆ i, ⨆ j, m i j
i j : ι
this : m i j ≤ K
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)