mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : ↑m = ord R x
⊢ 1 ≤ ↑(Multiplicative.ofAdd ↑m)

Tactic:
WithZero.one_le_coe,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : ↑m = ord R x
⊢ 1 ≤ Multiplicative.ofAdd ↑m
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx : coheight x = 1
hx' : x ∈ U
this : Ring.KrullDimLE 1 ↑(X.presheaf.stalk x)
⊢ (ordHom x hx) ((ConcreteCategory.hom (X.germToFunctionField U)) f) = 1

Tactic:
← algebraMap_germ_eq_germToFunctionField _ hx'

Goal state after:
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx : coheight x = 1
hx' : x ∈ U
this : Ring.KrullDimLE 1 ↑(X.presheaf.stalk x)
⊢ (ordHom x hx)
      ((algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) ((ConcreteCategory.hom (X.presheaf.germ U x hx')) f)) =
    1
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ≅ l₁
⊢ (conjugateEquiv adj₁ adj₂) α.hom ≫ (conjugateEquiv adj₂ adj₁) α.inv = 𝟙 r₁

Tactic:
by
        rw [conjugateEquiv_comp, Iso.inv_hom_id, conjugateEquiv_id]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
⊢ (max₁, max₂) ∈ antidiag

Tactic:
simp only [antidiag, mem_filter, mem_product]

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
⊢ (max₁ ∈ DFinsupp.support ((decompose 𝒜) x) ∧ max₂ ∈ DFinsupp.support ((decompose 𝒜) y)) ∧ True
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case e'_5
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ n, f i ∈ 𝒜 n
hf : Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤
x : A
hx : x ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal
⊢ x = x - ↑(((DirectSum.decompose 𝒜) x) 0)

Tactic:
← GradedRing.proj_apply,

Goal state after:
case e'_5
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ n, f i ∈ 𝒜 n
hf : Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤
x : A
hx : x ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal
⊢ x = x - (GradedRing.proj 𝒜 0) x
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
⊢ IsLocalization.Away (isLocalizationElem hf hg) (Away 𝒜 x)

Tactic:
let := (awayMap 𝒜 hg hx).toAlgebra
  constructor; constructor
  · rintro ⟨r, n, rfl⟩
    rw [map_pow, RingHom.algebraMap_toAlgebra]
    let z : Away 𝒜 x := Away.mk 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) (d + e)
        (g ^ e * f ^ (2 * e + d)) <| by
      convert!
        SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
          (SetLike.pow_mem_graded (2 * e + d) hf) using 2
      ring
    refine (isUnit_iff_exists_inv.mpr ⟨z, ?_⟩).pow _
    ext
    simp only [val_mul, val_one, awayMap_mk, Away.val_mk, z, Localization.mk_mul]
    rw [← Localization.mk_one, Localization.mk_eq_mk_iff, Localization.r_iff_exists]
    use 1
    simp only [OneMemClass.coe_one, one_mul, Submonoid.coe_mul, mul_one, hx]
    ring
  · intro z
    obtain ⟨n, s, hs, rfl⟩ := Away.mk_surjective 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) z
    rcases d with - | d
    · contradiction
    let t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) <| by
      convert! SetLike.mul_mem_graded hs (SetLike.pow_mem_graded _ hg) using 2; simp; ring
    refine ⟨⟨t, ⟨_, ⟨n, rfl⟩⟩⟩, ?_⟩
    ext
    simp only [RingHom.algebraMap_toAlgebra, map_pow, awayMap_mk, val_mul, val_mk, val_pow,
      Localization.mk_pow, Localization.mk_mul, t]
    rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
    exact ⟨1, by simp; ring⟩
  · intro a b e
    obtain ⟨n, a, ha, rfl⟩ := Away.mk_surjective 𝒜 hf a
    obtain ⟨m, b, hb, rfl⟩ := Away.mk_surjective 𝒜 hf b
    replace e := congr_arg val e
    simp only [RingHom.algebraMap_toAlgebra, awayMap_mk, val_mk,
      Localization.mk_eq_mk_iff, Localization.r_iff_exists] at e
    obtain ⟨⟨_, k, rfl⟩, hc⟩ := e
    refine ⟨⟨_, k + m + n, rfl⟩, ?_⟩
    ext
    simp only [val_mul, val_pow, val_mk, Localization.mk_pow,
      Localization.mk_eq_mk_iff, Localization.r_iff_exists, Submonoid.coe_mul, Localization.mk_mul,
      SubmonoidClass.coe_pow, Subtype.exists, exists_prop]
    refine ⟨_, ⟨k, rfl⟩, ?_⟩
    rcases d with - | d
    · contradiction
    subst hx
    convert! congr(f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) * $hc) using 1 <;> ring

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

Goal state before:
pp: case pos
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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ product ∈ q.asIdeal

Tactic:
· apply Ideal.mul_mem_left (α := A⁰_ f) _ _ (hx _)
          rw [(_ : m • n = _)]
          · mem_tac
          · simp only [smul_eq_mul, mul_comm]

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

Goal state before:
pp: case h
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)) := ⋯
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
i j : ι
m : ℕ
hm :
  (f * (g i * g j)) ^ m •
      ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i) -
        (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j)) =
    0
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m • t i) =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m • t j)

Tactic:
apply (M.isSMulRegular_of_le_basicOpen le_rfl).pow m

Goal state after:
case h
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)) := ⋯
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
i j : ι
m : ℕ
hm :
  (f * (g i * g j)) ^ m •
      ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i) -
        (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j)) =
    0
⊢ (fun x ↦ (g i * g j) ^ m • x) ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m • t i)) =
    (fun x ↦ (g i * g j) ^ m • x) ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m • t j))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) := ⋯
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) := ⋯
⊢ val
      ((Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯)
        (HomogeneousLocalization.mk x0 ⊗ₜ[↥(𝒜 0)] HomogeneousLocalization.mk y0)) =
    (HomogeneousLocalization.mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x_1 ↦ x ^ x_1) j, hb'⟩, den_mem := ⋯ }).val

Tactic:
simp only [Algebra.TensorProduct.lift_tmul, awayMapₐ_apply, val_mul,
    val_awayMap_mk, Localization.mk_mul, val_mk, x0, y0]

Goal state after:
case h
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)), num := ⟨a * g ^ (j * (d - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * d), ⋯⟩, den_mem := ⋯ }
⊢ Localization.mk (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)))
      (⟨x ^ (j * (e + 1)), ⋯⟩ * ⟨x ^ (j * d), ⋯⟩) =
    Localization.mk a ⟨x ^ j, ⋯⟩
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
𝒰 : Cover (precoverage P) X.left
h✝ : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
T : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOverProp p f → Presieve Y
V : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOverProp p f → Cover (precoverage P) Y.left
h : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOverProp p f) → Cover.Over S (V f H)
pV : ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp p f) (j : (V f H).I₀), Q ((V f H).X j ↘ S)
hV : ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp p f), T f H = (V f H).toPresieveOverProp ⋯
⊢ (𝒰.toPresieveOverProp p).bind T ∈ {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h}

Tactic:
let 𝒱j (j : 𝒰.I₀) : (Cover (precoverage P) ((𝒰.X j).asOverProp S (p j)).left) :=
      V ((𝒰.f j).asOverProp S) ⟨j⟩

Goal state after:
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
𝒰 : Cover (precoverage P) X.left
h✝ : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
T : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOverProp p f → Presieve Y
V : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOverProp p f → Cover (precoverage P) Y.left
h : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOverProp p f) → Cover.Over S (V f H)
pV : ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp p f) (j : (V f H).I₀), Q ((V f H).X j ↘ S)
hV : ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp p f), T f H = (V f H).toPresieveOverProp ⋯
𝒱j : (j : 𝒰.I₀) → Cover (precoverage P) ((𝒰.X j).asOverProp S ⋯).left := fun j ↦ V (Hom.asOverProp (𝒰.f j) S) ⋯
⊢ (𝒰.toPresieveOverProp p).bind T ∈ {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h}
Module: Mathlib.CategoryTheory.Limits.Elements

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
i : I
⊢ (hom (limit.π ((F ⋙ π A) ⋙ A) i))
      ((preservesLimitIso A (F ⋙ π A)).toEquiv ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd)) =
    (hom (limit.π ((F ⋙ π A) ⋙ A) i)) ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))

Tactic:
have h₁ := congr_hom (preservesLimitIso_hom_π A (F ⋙ π A) i)
    (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
i : I
h₁ :
  (hom ((preservesLimitIso A (F ⋙ π A)).hom ≫ limit.π ((F ⋙ π A) ⋙ A) i))
      ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd) =
    (hom (A.map (limit.π (F ⋙ π A) i))) ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd)
⊢ (hom (limit.π ((F ⋙ π A) ⋙ A) i))
      ((preservesLimitIso A (F ⋙ π A)).toEquiv ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd)) =
    (hom (limit.π ((F ⋙ π A) ⋙ A) i)) ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
⊢ ValuativeCriterion.Existence (toSpecZero 𝒜)

Tactic:
rintro ⟨O, K, i₁, i₂, w⟩

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
⊢ ⋯.HasLift
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this : IsAffine (𝒰.forgetQc.sigma.X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ Surjective (Spec.map φ)

Tactic:
simp only [hφ, f, Cover.sigma_I₀, PUnit.default_eq_unit, Cover.sigma_X, Cover.sigma_f, f]
      have : Surjective (Sigma.desc 𝒰.f) := inferInstanceAs <| Surjective (Sigma.desc 𝒰.forgetQc.f)
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ Y₀ : C₀
a : Y₀ ⟶ X₀
Y : C
i : (data (F.obj X₀)).toPreOneHypercover.I₀
b : F.obj Y₀ ⟶ (data (F.obj X₀)).toPreOneHypercover.X i
fac : b ≫ (data (F.obj X₀)).toPreOneHypercover.f i = F.map a
⊢ (presheafObjObjIso.inv data G₀ X₀ ≫ presheafObjObjIso.hom data G₀ X₀) ≫ G₀.obj.map { Y := Y₀, f := a, hf := ⋯ }.f.op =
    𝟙 (G₀.obj.obj (op X₀)) ≫ G₀.obj.map { Y := Y₀, f := a, hf := ⋯ }.f.op

Tactic:
dsimp at i b fac ⊢

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ Y₀ : C₀
a : Y₀ ⟶ X₀
Y : C
i : (data (F.obj X₀)).I₀
b : F.obj Y₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac : b ≫ (data (F.obj X₀)).f i = F.map a
⊢ (presheafObjObjIso.inv data G₀ X₀ ≫ presheafObjObjIso.hom data G₀ X₀) ≫ G₀.obj.map a.op =
    𝟙 (G₀.obj.obj (op X₀)) ≫ G₀.obj.map a.op
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
⊢ Order.succ (last n) = last n

Tactic:
by
  simp [orderSucc_apply]

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Order.succ i.castSucc = i.succ

Tactic:
by
  simp [orderSucc_apply]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁✝ : i < Order.succ i
hi₁ : i ≤ i
⊢ Arrow.mk (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩)) =
    Arrow.mk (Φ.toSucc ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩))).obj ⟨i, ⋯⟩))

Tactic:
extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i

Goal state after:
case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁✝ : i < Order.succ i
hi₁ : i ≤ i
⊢ Arrow.mk (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩)) = Arrow.mk (Φ.toSucc (iter.F.obj ⟨i, ?inr✝⟩))

case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁✝ : i < Order.succ i
hi₁ : i ≤ i
⊢ i ≤ i
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
g : Arrow C
⊢ Arrow.Hom.right (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (πFunctorObj f g.hom)))

Tactic:
· dsimp

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
⊢ Arrow.Hom.right (Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) ⋯) =
    Arrow.Hom.right
      (Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) ⋯ ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') ⋯)

Tactic:
· dsimp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ A < largerSubobject hG A

Tactic:
dsimp only [largerSubobject]
  rw [dif_neg hA]
  exact (exists_larger_subobject hG A hA).choose_spec.choose

Goal state after: