mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ (fun γ ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
      ((fun β ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
    𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h

Tactic:
by
        bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ (fun γ ↦ γ ▷ l ≫ (α_ h r l).hom ≫ h ◁ adj.counit ≫ (ρ_ h).hom)
      ((fun α ↦ (ρ_ g).inv ≫ g ◁ adj.unit ≫ (α_ g l r).inv ≫ α ▷ r) α) =
    𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ (α ▷ (r ≫ l) ≫ h ◁ adj.counit) ⊗≫ 𝟙 h

Tactic:
by
        bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
γ : g ⟶ h ≫ r
⊢ (fun α ↦ (ρ_ g).inv ≫ g ◁ adj.unit ≫ (α_ g l r).inv ≫ α ▷ r)
      ((fun γ ↦ γ ▷ l ≫ (α_ h r l).hom ≫ h ◁ adj.counit ≫ (ρ_ h).hom) γ) =
    𝟙 g ⊗≫ (g ◁ adj.unit ≫ γ ▷ (l ≫ r)) ⊗≫ h ◁ adj.counit ▷ r ⊗≫ 𝟙 (h ≫ r)

Tactic:
by
        bicategory

Goal state after:
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
s : Finset S
hs : Submodule.span R ↑s = ⊤
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, Function.Surjective ⇑f

Tactic:
have hf : Function.Surjective f := by
      have := (Submodule.span_le (p := LinearMap.range f.toLinearMap)).mpr hsf
      rwa [hs, top_le_iff, LinearMap.range_eq_top] at this

Goal state after:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
s : Finset S
hs : Submodule.span R ↑s = ⊤
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
hf : Function.Surjective ⇑f
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, Function.Surjective ⇑f
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ [Function.Surjective ⇑(algebraMap R S), Function.Bijective ⇑(LinearMap.mul' R S),
      ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1].TFAE

Tactic:
tfae_have 1 → 2 := LinearMap.mul'_bijective_of_surjective _ _
  tfae_have 2 → 3 := fun H p ↦ by
    have h : rankAtStalk (S ⊗[R] S) p = rankAtStalk S p ^ 2 := by
      simp [rankAtStalk_tensorProduct, sq]
    by_contra! hc
    apply Nat.succ_succ_ne_one 0
    rw [← Nat.pow_eq_self_iff hc, ← h, Module.rankAtStalk_eq_of_equiv
      (AlgEquiv.ofBijective (Algebra.TensorProduct.lmul' R (S := S)) H).toLinearEquiv]
  tfae_have 3 → 1 := Module.algebraMap_surjective_of_rankAtStalk_le_one
  tfae_finish

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

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : IsAffine S
inst✝¹ : Flat f
inst✝ : IsFinite f
s : ↥S
⊢ finrank f s = IsAffine.finrank f s

Tactic:
rw [show s = (𝟙 S : S ⟶ S) s from rfl, finrank_eq_finrank_snd_of_isAffine,
    IsAffine.finrank_snd]

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ 1 ≤ finrank (pullback.snd f g) y

Tactic:
hzr.symm

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ 1 ≤ finrank (pullback.snd f g) ((pullback.snd f g) z)
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e₁ : pullback (𝟙 Y) ⋙ pullback f ≅ pullback (f ≫ 𝟙 Y) := pullbackComp f (𝟙 Y)
e₂ : pullback (𝟙 Y) ⋙ pullback f ≅ 𝟭 Y.Modules ⋙ pullback f := Functor.isoWhiskerRight (pullbackId Y) (pullback f)
e₃ : 𝟭 Y.Modules ⋙ pullback f ≅ pullback f := (pullback f).leftUnitor
⊢ (pullbackComp f (𝟙 Y)).inv ≫ Functor.whiskerRight (pullbackId Y).hom (pullback f) ≫ (pullback f).leftUnitor.hom =
    eqToHom ⋯

Tactic:
change e₁.inv ≫ e₂.hom ≫ e₃.hom = _

Goal state after:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback (𝟙 Y) ⋙ pullback f ≅ pullback (f ≫ 𝟙 Y) := pullbackComp f (𝟙 Y)
e₂ : pullback (𝟙 Y) ⋙ pullback f ≅ 𝟭 Y.Modules ⋙ pullback f := Functor.isoWhiskerRight (pullbackId Y) (pullback f)
e₃ : 𝟭 Y.Modules ⋙ pullback f ≅ pullback f := (pullback f).leftUnitor
⊢ e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom ⋯
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
e₃ : pullback f ⋙ 𝟭 X.Modules ≅ pullback f := (pullback f).rightUnitor
⊢ (pullbackComp (𝟙 X) f).inv ≫ (pullback f).whiskerLeft (pullbackId X).hom ≫ (pullback f).rightUnitor.hom = eqToHom ⋯

Tactic:
change e₁.inv ≫ e₂.hom ≫ e₃.hom = _

Goal state after:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
e₃ : pullback f ⋙ 𝟭 X.Modules ≅ pullback f := (pullback f).rightUnitor
⊢ e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom ⋯
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (pullbackComp (𝟙 X) f).inv ≫ (pullback f).whiskerLeft (pullbackId X).hom ≫ (pullback f).rightUnitor.hom = eqToHom ⋯

Tactic:
by
  let e₁ := pullbackComp (𝟙 _) f
  let e₂ := Functor.isoWhiskerLeft (pullback f) (pullbackId _)
  let e₃ := (pullback f).rightUnitor
  change e₁.inv ≫ e₂.hom ≫ e₃.hom = _
  have : e₁.hom = e₂.hom ≫ e₃.hom :=
    congr_arg Iso.hom (SheafOfModules.pullback_comp_id.{u} f.toRingCatSheafHom)
  simp [← this]

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

Goal state before:
pp: case surj
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
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := ⋯
⊢ ∀ (z : Away 𝒜 x), ∃ x_1, z * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1

Tactic:
intro z

Goal state after:
case surj
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
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
z : Away 𝒜 x
⊢ ∃ x_1, z * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range fun i ↦ ↑i.snd)

Tactic:
intro z

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
⊢ z ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal → z ∈ Ideal.span (Set.range fun i ↦ ↑i.snd)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case pos
ι : 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
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : Subsingleton (Away 𝒜 f)
⊢ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} = ⊤

pp: case neg
ι : 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
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
⊢ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} = ⊤

Tactic:
· exact Subsingleton.elim _ _

Goal state after:
case neg
ι : 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
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
⊢ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} = ⊤
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
⊢ Function.Injective ⇑(IsLocalization.liftAlgHom ⋯)

Tactic:
intro x y e

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x y : Localization.AtPrime P
e : (IsLocalization.liftAlgHom ⋯) x = (IsLocalization.liftAlgHom ⋯) y
⊢ x = y
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_2.refine_2
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 : ℕ
⊢ f ^ (i - n) ∈ 𝒜 (m • (i - n))

Tactic:
(_ : m • (i - n) = _)

Goal state after:
case refine_2.refine_2
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 : ℕ
⊢ f ^ (i - n) ∈ 𝒜 ?m.461

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 : ℕ
⊢ m • (i - n) = ?m.461
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
⊢ Subtype.val ∘ ⇑(g.rangeRestrict.comp f) = ⇑(algebraMap R K)

Tactic:
← h

Goal state after:
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
⊢ Subtype.val ∘ ⇑(g.rangeRestrict.comp f) = ⇑(g.comp f)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case surj
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := ⋯
⊢ ∀ (z : AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal),
    ∃ x_1,
      z * (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) ↑x_1.2 =
        (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) x_1.1

Tactic:
intro z

Goal state after:
case surj
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
z : AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal
⊢ ∃ x_1,
    z * (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) ↑x_1.2 =
      (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) x_1.1
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 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
⊢ Function.Surjective ⇑(Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯)

Tactic:
intro z

Goal state after:
σ : 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
z : Away 𝒜 x
⊢ ∃ a, (Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯) a = z
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S : Scheme
⊢ qcPrecoverage.IsStableUnderComposition

Tactic:
refine .of_preZeroHypercoverFamily fun {X} E F hE hF ↦ ?_
  simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢
  infer_instance

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

Goal state before:
pp: S : Scheme
⊢ qcPrecoverage.IsStableUnderSup

Tactic:
refine .of_preZeroHypercoverFamily fun {X} E F hE hF ↦ ?_
  simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢
  infer_instance

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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
Z : C
a₁ : α
⊢ ∀ (a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }

Tactic:
a₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
Z : C
a₁ a₂ : α
⊢ ∀ (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
x✝¹ x✝ : Under j₀
g : x✝¹ ⟶ x✝
⊢ ((Functor.const (Under j₀)).obj (X.obj j₀)).map g ≫ X.map x✝.hom = X.map x✝¹.hom ≫ (Under.forget j₀ ⋙ X).map g

Tactic:
by
        dsimp
        simp only [Category.id_comp, ← X.map_comp, Under.w]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = ⨆ j, Subobject.mk (F.obj j).obj.hom
⊢ IsColimit ((Over.forget X).mapCocone c)

Tactic:
← h

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
⊢ IsColimit ((Over.forget X).mapCocone c)
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
h : i = j
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b

pp: case neg
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
h : ¬i = j
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b

Tactic:
· subst h
      rw [(cancel_mono _).mp hab]

Goal state after:
case neg
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
h : ¬i = j
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
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
⊢ J.Subcanonical

Tactic:
refine .of_isSheaf_yoneda_obj _ fun Y ↦ ?_

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
⊢ Presieve.IsSheaf J (CategoryTheory.yoneda.obj 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
⊢ Presheaf.IsSheaf J
    ((F ⋙ CategoryTheory.uliftYoneda.{v, v', u_1} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v v'))).obj F.op).obj Y)

Tactic:
refine F.op_comp_isSheaf_of_isSheaf J K _ ?_

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 K (CategoryTheory.uliftYoneda.{v, v', u_1}.obj (F.obj Y))
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
i : J
hi₀ : i = s.top
⊢ HasColimitsOfShape α C

Tactic:
induction i using SuccOrder.limitRecOn with
    | isMin i hi =>
      subst hi₀
      exact (hi.not_lt (s.lt_top (Classical.arbitrary _))).elim
    | succ i hi _ =>
      obtain ⟨a, rfl⟩ := (s.mem_range_iff_rel (b := i)).2 (by
        simpa only [← hi₀] using Order.lt_succ_of_not_isMax hi)
      have : OrderTop α :=
        { top := a
          le_top b := by
            rw [← s.le_iff_le]
            exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b) }
      infer_instance
    | isSuccLimit i hi =>
      subst hi₀
      exact hasColimitsOfShape_of_isSuccLimit' C s hi

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone transfiniteCompositions.{w, v, u}

Tactic:
by
  intro W₁ W₂ h X Y f hf
  rw [transfiniteCompositions_iff] at hf
  obtain ⟨J, _, _, _, _, hf⟩ := hf
  exact transfiniteCompositionsOfShape_le_transfiniteCompositions _ _ _
    (transfiniteCompositionsOfShape_monotone J h _ hf)

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

Goal state before:
pp: case succ
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
hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ Order.succ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂

Tactic:
have h₀ := Order.le_succ j

Goal state after:
case succ
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
hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ Order.succ j
h₀ : j ≤ Order.succ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂