mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Extension R S
T✝ : Type u_3
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
P : Extension R S
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
this✝¹ : Algebra P.Ring P.baseChange.Ring := P.algebraBaseChange T
this✝ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
x : R
⊢ 1 ⊗ₜ[R] (algebraMap R S) x = ((algebraMap S (T ⊗[R] S)).comp (algebraMap P.Ring S)) ((algebraMap R P.Ring) x)

Tactic:
IsScalarTower.algebraMap_apply R P.Ring

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Extension R S
T✝ : Type u_3
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
P : Extension R S
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
this✝¹ : Algebra P.Ring P.baseChange.Ring := P.algebraBaseChange T
this✝ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
x : R
⊢ 1 ⊗ₜ[R] (algebraMap P.Ring S) ((algebraMap R P.Ring) x) =
    ((algebraMap S (T ⊗[R] S)).comp (algebraMap P.Ring S)) ((algebraMap R P.Ring) x)
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f : WithConv (S →ₐ[R] T)
⊢ ((fun f ↦ WithConv.toConv { toRingHom := CommRingCat.Hom.hom (preimage (Over.Hom.left f)), commutes' := ⋯ })
        ((fun f ↦ Hom.asOver (map (CommRingCat.ofHom f.ofConv.toRingHom)) (Spec (CommRingCat.of R))) f)).ofConv =
    f.ofConv

Tactic:
apply AlgHom.coe_ringHom_injective

Goal state after:
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f : WithConv (S →ₐ[R] T)
⊢ ↑((fun f ↦ WithConv.toConv { toRingHom := CommRingCat.Hom.hom (preimage (Over.Hom.left f)), commutes' := ⋯ })
          ((fun f ↦ Hom.asOver (map (CommRingCat.ofHom f.ofConv.toRingHom)) (Spec (CommRingCat.of R))) f)).ofConv =
    ↑f.ofConv
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case e_a
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
      map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv)) =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯ ≫
      (pullbackSpecIso R S S).hom

Tactic:
← Iso.comp_inv_eq

Goal state after:
case e_a
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ (map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
        map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv))) ≫
      (pullbackSpecIso R S S).inv =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (leftZigzagIso η ε).inv = rightZigzag ε.inv η.inv

Tactic:
simp [bicategoricalComp, bicategoricalIsoComp]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (rightZigzagIso η ε).inv = leftZigzag ε.inv η.inv

Tactic:
simp [bicategoricalComp, bicategoricalIsoComp]

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

Goal state before:
pp: W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : WeaklyEtale f
⊢ WeaklyEtale (Scheme.Hom.resLE f V U e)

Tactic:
delta Scheme.Hom.resLE; infer_instance

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

Goal state before:
pp: W X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
⊢ ∀ (f : X ⟶ Y), WeaklyEtale f → MorphismProperty.diagonal (@WeaklyEtale) f

Tactic:
f

Goal state after:
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
⊢ WeaklyEtale f → MorphismProperty.diagonal (@WeaklyEtale) f
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
this✝¹ : Nonempty ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
this✝ : Nontrivial (R ⧸ Ideal.span {r})
this : Nontrivial R
⊢ ⨆ i, ↑i.length + 1 ≤ ⨆ p, ↑p.length

Tactic:
iSup_le_iff

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
this✝¹ : Nonempty ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
this✝ : Nontrivial (R ⧸ Ideal.span {r})
this : Nontrivial R
⊢ ∀ (i : LTSeries ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))), ↑i.length + 1 ≤ ⨆ p, ↑p.length
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
hn : ord R x = ↑n
⊢ (ordMonoidWithZeroHom R) x = ↑(Multiplicative.ofAdd ↑n)

Tactic:
by
  simp [ordMonoidWithZeroHom_eq_ord hx, hn]

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
a : ↥R⁰
⊢ (ordMonoidWithZeroHom R) ↑a ≠ 0

Tactic:
simp [← ordMonoidWithZeroHom_eq_ordMonoidHom]

Goal state after:
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
⊢ 0 ≤ ↑m

Tactic:
Nat.cast_nonneg _

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
⊢ ∀ A_1 ⊆ Set.range (zeroLocus 𝒜), ⋂₀ A_1 ∈ Set.range (zeroLocus 𝒜)

Tactic:
intro Zs h
      rw [Set.sInter_eq_iInter]
      let f : Zs → Set _ := fun i => Classical.choose (h i.2)
      have H : (Set.iInter fun i ↦ zeroLocus 𝒜 (f i)) ∈ Set.range (zeroLocus 𝒜) :=
        ⟨_, zeroLocus_iUnion 𝒜 _⟩
      convert! H using 2
      funext i
      exact (Classical.choose_spec (h i.2)).symm

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
n : ℕ
hn : 0 < n
⊢ ↑(basicOpen 𝒜 (f ^ n)) = ↑(basicOpen 𝒜 f)

Tactic:
simpa using zeroLocus_singleton_pow 𝒜 f n hn

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), (GradedRing.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 f]
          apply Ideal.sum_mem _ fun i _ => H i

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 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
⊢ k' ∈ {x | (fun n ↦ f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))) x}

Tactic:
simp only [Set.mem_image, SetLike.mem_coe, Set.mem_ofPred_eq]

Goal state after:
ι : 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 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f)) x = f ^ k' • val z
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case neg
σ : 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
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : ¬n = 0
⊢ f i - ↑(((DirectSum.decompose 𝒜) (f i)) 0) ∈ Ideal.span (Set.range f)

Tactic:
DirectSum.decompose_of_mem_ne 𝒜 hn hn',

Goal state after:
case neg
σ : 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
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : ¬n = 0
⊢ f i - 0 ∈ Ideal.span (Set.range f)
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ⇑A.subtype '' ↑I ⊆ ↑V.nonunits

Tactic:
rw [← V.image_maximalIdeal]

Goal state after:
K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ⇑A.subtype '' ↑I ⊆ Subtype.val '' ↑(maximalIdeal ↥V)
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝¹ : IsDomain ↑(CommRingCat.of R)
this✝ : ValuationRing ↑(CommRingCat.of R)
this : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ : flip (fun x1 x2 ↦ x1 ⤳ x2) x (lft (closedPoint ↑(CommRingCat.of K)))
h₂ : (pullback.fst i₂ f) x = closedPoint R
⊢ ⋯.HasLift

Tactic:
let e : CommRingCat.of R ≅ (Spec <| .of R).presheaf.stalk (pullback.fst i₂ f x) :=
    (stalkClosedPointIso (.of R)).symm ≪≫
      (Spec <| .of R).presheaf.stalkCongr (.of_eq h₂.symm)

Goal state after:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝¹ : IsDomain ↑(CommRingCat.of R)
this✝ : ValuationRing ↑(CommRingCat.of R)
this : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ : flip (fun x1 x2 ↦ x1 ⤳ x2) x (lft (closedPoint ↑(CommRingCat.of K)))
h₂ : (pullback.fst i₂ f) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
⊢ ⋯.HasLift
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
⊢ ∀ {g : X ⟶ Y} {f' : X' ⟶ X} {g' : X' ⟶ Y'}, IsPullback f' g' g Y'_to_Y → Existence g → Existence g'

Tactic:
f

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
⊢ ∀ {f' : X' ⟶ X} {g' : X' ⟶ Y'}, IsPullback f' g' f Y'_to_Y → Existence f → Existence g'
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case hR
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
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
Y : C
⊢ ∀ ⦃f : Y ⟶ W⦄ (H : (Sieve.coverByImage F W).arrows f),
    Sieve.pullback (Nonempty.some H).lift
        (Sieve.functorPushforward F
          (F.imageSieve ((Nonempty.some H).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some H).map ≫ p₂))) ∈
      J Y

Tactic:
f

Goal state after:
case hR
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
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
Y : C
f : Y ⟶ W
⊢ ∀ (H : (Sieve.coverByImage F W).arrows f),
    Sieve.pullback (Nonempty.some H).lift
        (Sieve.functorPushforward F
          (F.imageSieve ((Nonempty.some H).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some H).map ≫ p₂))) ∈
      J Y
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
this :
  ∀ (X : C) (x : Φ.fiber.obj X) (p₁ p₂ : ToType (P.obj (op X))),
    (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂ →
      (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂
X : C
p₁ p₂ : ToType (P.obj (op X))
Y : C
g : Y ⟶ X
y : Φ.fiber.obj Y
h :
  (ConcreteCategory.hom (Q.map g.op)) ((ConcreteCategory.hom (f.app (op X))) p₁) =
    (ConcreteCategory.hom (Q.map g.op)) ((ConcreteCategory.hom (f.app (op X))) p₂)
⊢ (ConcreteCategory.hom (Φ.toPresheafFiber X ((ConcreteCategory.hom (Φ.fiber.map g)) y) P)) p₁ =
    (ConcreteCategory.hom (Φ.toPresheafFiber X ((ConcreteCategory.hom (Φ.fiber.map g)) y) P)) p₂

Tactic:
simp only [← NatTrans.naturality_apply] at h

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
this :
  ∀ (X : C) (x : Φ.fiber.obj X) (p₁ p₂ : ToType (P.obj (op X))),
    (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂ →
      (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂
X : C
p₁ p₂ : ToType (P.obj (op X))
Y : C
g : Y ⟶ X
y : Φ.fiber.obj Y
h :
  (ConcreteCategory.hom (f.app (op Y))) ((ConcreteCategory.hom (P.map g.op)) p₁) =
    (ConcreteCategory.hom (f.app (op Y))) ((ConcreteCategory.hom (P.map g.op)) p₂)
⊢ (ConcreteCategory.hom (Φ.toPresheafFiber X ((ConcreteCategory.hom (Φ.fiber.map g)) y) P)) p₁ =
    (ConcreteCategory.hom (Φ.toPresheafFiber X ((ConcreteCategory.hom (Φ.fiber.map g)) y) P)) p₂
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁷ : Category.{v', u'} A
inst✝⁶ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁵ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory A FC
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : J.WEqualsLocallyBijective A
inst✝ : (forget A).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ A
⊢ ∀ (f : P ⟶ Q), J.W f → IsIso (Φ.presheafFiber.map f)

Tactic:
f

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁷ : Category.{v', u'} A
inst✝⁶ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁵ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory A FC
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : J.WEqualsLocallyBijective A
inst✝ : (forget A).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ J.W f → IsIso (Φ.presheafFiber.map f)
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: X Y : Scheme
⊢ ∀ (f : X ⟶ Y), IsOpenImmersion f → Etale f

Tactic:
f

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ IsOpenImmersion f → Etale f
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
⊢ liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op

Tactic:
refine Presheaf.IsSheaf.hom_ext
      hG₀ ⟨_, cover_lift F J₀ _
        (J.pullback_stable (F.map ((data X).p₁ j) ≫ (data X).f i₁) S.2)⟩ _ _ ?_

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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
⊢ ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        ⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩),
    (liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op) ≫ (F.op ⋙ G).map I.f.op =
      (liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op) ≫ (F.op ⋙ G).map I.f.op
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Cᵒᵖ ⥤ A
⊢ ∀ (f g : F ⟶ G),
    (∀ (G_1 : Cᵒᵖ ⥤ A),
        ObjectProperty.ofObj
            (fun x ↦
              match x with
              | (X, i) => freeYoneda X (S i))
            G_1 →
          ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g) →
      f = g

Tactic:
f

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ ∀ (g : F ⟶ G),
    (∀ (G_1 : Cᵒᵖ ⥤ A),
        ObjectProperty.ofObj
            (fun x ↦
              match x with
              | (X, i) => freeYoneda X (S i))
            G_1 →
          ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g) →
      f = g
Module: Mathlib.CategoryTheory.Generator.Sheaf

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Sheaf J A
⊢ ∀ (f g : F ⟶ G),
    (∀ (G_1 : Sheaf J A),
        ObjectProperty.ofObj
            (fun x ↦
              match x with
              | (X, i) => freeYoneda J X (S i))
            G_1 →
          ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g) →
      f = g

Tactic:
f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Sheaf J A
f : F ⟶ G
⊢ ∀ (g : F ⟶ G),
    (∀ (G_1 : Sheaf J A),
        ObjectProperty.ofObj
            (fun x ↦
              match x with
              | (X, i) => freeYoneda J X (S i))
            G_1 →
          ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g) →
      f = g
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).toOneHypercover.multicospanShape.L
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).toPreOneHypercover.I₀
c : F.obj X₀ ⟶ (data X).toPreOneHypercover.X j
fac₁ : c ≫ (data X).toPreOneHypercover.f j = F.map b ≫ (data a.Y).f i ≫ a.f
⊢ ((lift hG₀ hG s ≫ G.map a.f.op) ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫
      (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op =
    (s.ι a ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op

Tactic:
refine Presheaf.IsSheaf.hom_ext hG₀
          ⟨_, IsDenseSubsite.imageSieve_mem J₀ J F c⟩ _ _ ?_

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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).toOneHypercover.multicospanShape.L
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).toPreOneHypercover.I₀
c : F.obj X₀ ⟶ (data X).toPreOneHypercover.X j
fac₁ : c ≫ (data X).toPreOneHypercover.f j = F.map b ≫ (data a.Y).f i ≫ a.f
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨F.imageSieve c, ⋯⟩),
    (((lift hG₀ hG s ≫ G.map a.f.op) ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫
          (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op) ≫
        (F.op ⋙ G).map I.f.op =
      ((s.ι a ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op) ≫
        (F.op ⋙ G).map I.f.op