mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
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)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j)
⊢ f ^ N • (ConcreteCategory.hom (M.presheaf.map (homOfLE hfgigi).op)) (s' i) -
      (ConcreteCategory.hom (M.presheaf.map (homOfLE hfgigj ≫ homOfLE ⋯).op)) (t j) =
    0

Tactic:
← M.presheaf.map_comp_apply,

Goal state after:
case refine_1
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)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j)
⊢ f ^ N • (ConcreteCategory.hom (M.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE hfgigi).op))) s -
      (ConcreteCategory.hom (M.presheaf.map (homOfLE hfgigj ≫ homOfLE ⋯).op)) (t j) =
    0
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
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit ((mapId 𝒜 ⋯) (HomogeneousLocalization.mk z)).val ↔
    HomogeneousLocalization.mk z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x

Tactic:
ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit ((mapId 𝒜 ⋯) (HomogeneousLocalization.mk z)).val ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
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)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j)
⊢ f ^ N • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s -
      f ^ N • (ConcreteCategory.hom (M.presheaf.map (homOfLE hfgigj).op)) (s' j) =
    0

Tactic:
← M.presheaf.map_comp_apply,

Goal state after:
case refine_1
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)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j)
⊢ f ^ N • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s -
      f ^ N • (ConcreteCategory.hom (M.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE hfgigj).op))) s =
    0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h.refine_2
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)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
a : ToType ({ obj := M.presheaf, property := ⋯ }.obj.obj (op V))
ha : ∀ (i : ι), (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) a = f ^ K • t i
i : ι
⊢ (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) a) =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) (f ^ (N + K) • s)

Tactic:
← M.presheaf.map_comp_apply,

Goal state after:
case h.refine_2
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)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
a : ToType ({ obj := M.presheaf, property := ⋯ }.obj.obj (op V))
ha : ∀ (i : ι), (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) a = f ^ K • t i
i : ι
⊢ (ConcreteCategory.hom (M.presheaf.map ((homOfLE hf).op ≫ (homOfLE ⋯).op))) a =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) (f ^ (N + K) • s)
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
⊢ (S.i₂ ≫ pullback.fst f f) ≫ f = S'.i₂

Tactic:
by simp [S']

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

Goal state before:
pp: case refine_1.refine_1
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)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
i j : ι
this : Function.Injective ⇑(ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯).op))
⊢ (ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯).op))
      ((ConcreteCategory.hom (M.presheaf.map ⋯.hom.op)) (f ^ K • t i)) =
    (ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯).op))
      ((ConcreteCategory.hom (M.presheaf.map ⋯.hom.op)) (f ^ K • t j))

Tactic:
← M.presheaf.map_comp_apply,

Goal state after:
case refine_1.refine_1
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)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
i j : ι
this : Function.Injective ⇑(ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯).op))
⊢ (ConcreteCategory.hom (M.presheaf.map (⋯.hom.op ≫ (eqToHom ⋯).op))) (f ^ K • t i) =
    (ConcreteCategory.hom (M.presheaf.map (⋯.hom.op ≫ (eqToHom ⋯).op))) (f ^ K • t j)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t) = 0

Tactic:
← M.presheaf.map_comp_apply,

Goal state after:
case refine_1
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
⊢ (ConcreteCategory.hom (M.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) t = 0
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_3
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))
T : Scheme
⊢ ∀ (E : (propQCPrecoverage P).ZeroHypercover T), Presieve.IsSheafFor F E.presieve₀

Tactic:
(𝒰 : Scheme.Cover _ _)

Goal state after:
case refine_3
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))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: case refine_2
X : Scheme
⊢ ∀ {R S : CommRingCat} (f : R ⟶ S),
    Flat (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))

Tactic:
· intro R S f hf₁ hf₂
    have : IsRegularEpi (Spec.map f) :=
      isRegularEpi_of_flat_of_surjective_of_isAffine _
    exact .singleton_of_isRepresentable_of_effectiveEpi _ _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ π a ≫ H.desc (aux e ⋯) = e a

Tactic:
by
      have := H.fac (aux e h) ⟨Over.mk (π a), a, 𝟙 _, by simp⟩
      dsimp [aux] at this; rw [this]; clear this
      conv_rhs => rw [← Category.id_comp (e a)]
      apply h
      generalize_proofs h1 h2
      rw [h2.choose_spec, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : Surjective f
inst✝ : LocallyOfFinitePresentation f
⊢ Presieve.singleton f ∈ fppfPrecoverage.coverings Y

Tactic:
rw [← Presieve.ofArrows_pUnit.{0}]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : Surjective f
inst✝ : LocallyOfFinitePresentation f
⊢ (Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∈ fppfPrecoverage.coverings Y
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
⊢ Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type, Presheaf.isSheaf_of_iso_iff
    ((Functor.FullyFaithful.ofFullyFaithful F).compUliftYonedaCompWhiskeringLeft.app Y).symm]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
⊢ Presheaf.IsSheaf J
    ((F ⋙ CategoryTheory.uliftYoneda.{v, v', u_1} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v v'))).obj F.op).obj Y)
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑(Order.succ i) = ↑⟨Order.succ ↑i, ⋯⟩

Tactic:
simp only [coe_succ_of_not_isMax hi]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
g : ⊥ ⟶ j
⊢ W (hf.F.map g)

Tactic:
obtain rfl : g = homOfLE bot_le := rfl

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
⊢ W (hf.F.map (homOfLE ⋯))
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case succ.inr.inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂

Tactic:
· by_cases h' : k₁ ≤ j
          · apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
            simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
              arrowSucc_eq, hsucc]
          · simp only [not_le] at h'
            obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
            rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]

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

Goal state before:
pp: case succ.inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ Order.succ j
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h : ¬k₂ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂

Tactic:
obtain h₂ | rfl := h₂.lt_or_eq
        · exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)
        · by_cases h' : k₁ ≤ j
          · apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
            simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
              arrowSucc_eq, hsucc]
          · simp only [not_le] at h'
            obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
            rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]

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

Goal state before:
pp: 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
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (inductiveSystem iter).obj ⟨i, hi⟩ = iter'.F.obj ⟨i, hk⟩

Tactic:
apply congr_obj

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

Goal state before:
pp: 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
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ arrowSucc (functor hj iter) i hi = Φ.toSuccArrow ((functor hj iter).obj ⟨i, ⋯⟩)

Tactic:
rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i)
        ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj,
      ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
      arrowSucc_eq, functor_obj _ _ _ hi]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
wlog hle : padicValRat p q ≤ padicValRat p r generalizing q r

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)

Tactic:
rw [min_eq_right h, add_comm]; exact le_padicValRat_add_of_le (by rwa [add_comm]) h

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ↑x = 0 ↔ x = 0

Tactic:
← coe_zero,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ↑x = ↑0 ↔ x = 0
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
i : ℕ
hi : i ∈ S'
⊢ i ∈ Finset.cons s S' Hnot

Tactic:
by rw [Finset.cons_eq_insert, Finset.mem_insert]; exact Or.inr hi

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
| padicValNat p n !

Tactic:
← one_mul (padicValNat p n !)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
| 1 * padicValNat p n !
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ‖x‖ < 1
⊢ ↑p ∣ x

Tactic:
← norm_lt_one_iff_dvd

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ‖x‖ < 1
⊢ ‖x‖ < 1
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
a✝ : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ c.fst ≫ φ = 𝟙 c.pt

Tactic:
by
      rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id]

Goal state after: