mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H :
  (⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
c : Spec (CommRingCat.of K) ⟶ (G ⊗ G).left
hc : c ≫ (G ⊗ G).hom = 𝟙 (Spec (CommRingCat.of K))
hc₃ : c point ∈ closedPoints ↥(G ⊗ G).left
hc₁ : c point ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}
hc₂ : c point ∉ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
e : (pointEquivClosedPoint (G ⊗ G).hom) ⟨c, hc⟩ = ⟨c point, hc₃⟩
fc : 𝟙_ (Over S) ⟶ 𝟙_ (Over S) ⊗ G := lift (𝟙 (𝟙_ (Over S))) (Over.homMk c hc ≫ snd G G)
this : c ≫ pullback.fst G.hom G.hom = Over.Hom.left η
H₁ : c = Over.Hom.left fc ≫ Over.Hom.left (η ▷ G)
H₂ : fc ≫ η ▷ G ≫ γ = lift η η
⊢ c point ∈ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}

Tactic:
by simp [H₁, H₂, ← Scheme.Hom.comp_apply, Category.assoc, ← Over.comp_left]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
U : (normalization (pullback.snd f fT)).Opens
hU : (toNormalization (pullback.snd f fT)) ↑v ∈ U
right✝ : IsIso (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : ↑U ⟶ ↑U' := resLE fTn U' U ⋯
this : Surjective fTnU
H : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
⊢ IsPullback
    (pullback.map f fT (fromNormalization f) fT (toNormalization f) (𝟙 T) (𝟙 Y) ⋯ ⋯ ≫
      pullback.snd (fromNormalization f) fT)
    (pullback.fst f fT) fT (toNormalization f ≫ fromNormalization f)

Tactic:
by simpa using (.flip <| .of_hasPullback ..)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
⊢ Over.Hom.left (preservesTerminalIso (algSpec R)).inv = 𝟙 (Spec R)

Tactic:
rw [preservesTerminalIso_algSpec]; rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
⊢ Sieve.functorPushforward U.overEquivalence.functor S ∈
      (Opens.grothendieckTopology ↥U) (U.overEquivalence.functor.obj V) ↔
    S ∈ ((Opens.grothendieckTopology X).over U) V

Tactic:
simp only [Opens.mem_grothendieckTopology, Sieve.mem_functorPushforward_functor]
    constructor
    · intro H x hxV
      obtain ⟨W, f, hW, hxW⟩ := H ⟨x, V.hom.le hxV⟩ hxV
      exact ⟨_, ((U.overEquivalence.symm.toAdjunction.homEquiv _ _ ).symm f).left,
        ⟨_, _, 𝟙 _, hW, rfl⟩, _, hxW, rfl⟩
    · intro H x hxV
      obtain ⟨W, f, ⟨W', hW'V, hWW', hSW'V, rfl⟩, hxW⟩ := H x hxV
      exact ⟨_, U.overEquivalence.functor.map hW'V,
        S.downward_closed hSW'V (U.overEquivalence.unitInv.app W'), hWW'.le hxW⟩

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 : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ 𝟙 g ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) =
    γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h)

Tactic:
rw [← whisker_exchange]
        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
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ (α ▷ (r ≫ l) ≫ h ◁ adj.counit) ⊗≫ 𝟙 h =
    𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α

Tactic:
rw [← whisker_exchange]
        bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
| (mateEquiv adj₁ adj₂) α = β

Tactic:
eq_comm,

Goal state after:
B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
| β = (mateEquiv adj₁ adj₂) α
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫
          f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by
      bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom (f ◁ ε.inv)]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom η.inv]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by
      rw [Iso.inv_hom_id]; bicategory
    _ = _ := by
      rw [Iso.inv_hom_id]; bicategory

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:
by
  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
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ R, Y = Spec R) → IsLocallyConstant (finrank f)
hY : ¬∃ R, Y = Spec R
⊢ IsLocallyConstant (finrank f)

pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
hY : ∃ R, Y = Spec R
⊢ IsLocallyConstant (finrank f)

Tactic:
· rw [IsLocallyConstant.iff_exists_open]
    intro y
    obtain ⟨R, g, _, x, rfl⟩ := Y.exists_Spec_apply_eq y
    simp_rw [IsLocallyConstant.iff_exists_open] at this
    obtain ⟨U, hU, hxU, H⟩ := this (pullback.snd f g) ⟨_, rfl⟩ x
    refine ⟨g ''ᵁ ⟨U, hU⟩, (g ''ᵁ ⟨U, hU⟩).2, ⟨x, hxU, rfl⟩, fun y ↦ ?_⟩
    rintro ⟨y', (hyU : y' ∈ U), (rfl : g y' = y)⟩
    rw [← finrank_pullback_snd _ g, ← finrank_pullback_snd _ g]
    exact H y' hyU

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
hY : ∃ R, Y = Spec R
⊢ IsLocallyConstant (finrank f)
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : R
hy : y ∈ nonZeroDivisors R
ha : ¬(algebraMap R K) x / (algebraMap R K) y = 0
⊢ (ordFrac R) ((algebraMap R K) x / (algebraMap R K) y) =
    (MonoidWithZero.inverse.comp
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom)
      ((algebraMap R K) x / (algebraMap R K) y)

Tactic:
simp_all [ordFrac_eq_intValuation _, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap,
    IsDiscreteValuationRing.intValuation_maximalIdeal]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ rightAdjointConjugateSquare.vcomp ((conjugateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) β) =
    (mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β)

Tactic:
calc
    _ = 𝟙 _ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
            (mateEquiv adj₂ adj₃ β) ⊗≫ 𝟙 _ := by
      dsimp only [conjugateEquiv_apply, rightAdjointConjugateSquare.vcomp, rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointConjugateSquare.vcomp]
      bicategory

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

Goal state before:
pp: case zero
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
⊢ ↑(GradedMonoid.GMonoid.gnpow 0 c.den) ∈ x

Tactic:
simp only [coe_gnpow, pow_zero, one_mem]

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ (HomogeneousLocalization.mk { deg := m * (n * m), num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ (n * m), ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal) =
    (HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal)

Tactic:
eq_comm,

Goal state after:
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
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ (HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal) =
    (HomogeneousLocalization.mk { deg := m * (n * m), num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ (n * m), ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal)
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 𝒜
B : Type u_4
τ : Type u_5
inst✝⁷ : CommRing B
inst✝⁶ : SetLike τ B
inst✝⁵ : AddSubgroupClass τ B
ℬ : ι → τ
inst✝⁴ : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst✝³ : CommRing C
inst✝² : SetLike ψ C
inst✝¹ : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst✝ : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
⊢ Quotient.map' (fun x ↦ { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }) ⋯
      (Quotient.mk'' x * Quotient.mk'' y) =
    Quotient.map' (fun x ↦ { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }) ⋯
        (Quotient.mk'' x) *
      Quotient.map' (fun x ↦ { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }) ⋯
        (Quotient.mk'' y)

Tactic:
by
    simp only [← mk_mul, Quotient.map'_mk'', num_mul, map_mul, den_mul]; rfl

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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ (awayMap 𝒜 hg hx) ((fromZeroRingHom 𝒜 (Submonoid.powers f)) a) = (fromZeroRingHom 𝒜 (Submonoid.powers x)) a

Tactic:
ext
  simp only [fromZeroRingHom, val_awayMap]
  convert! IsLocalization.lift_eq _ _

Goal state after:
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 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
e_3✝ : Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f) = (toLocallyRingedSpace 𝒜).restrict ⋯
e_4✝ :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
⊢ Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f) =
    ΓSpec.locallyRingedSpaceAdjunction.unit.app (Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f)) ≫
      Spec.toLocallyRingedSpace.map (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f).op

Tactic:
dsimp [basicOpenToSpec, Scheme.Opens.toSpecΓ]

Goal state after:
case e'_5
σ : 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
e_3✝ : Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f) = (toLocallyRingedSpace 𝒜).restrict ⋯
e_4✝ :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
⊢ Scheme.forgetToLocallyRingedSpace.map
      (((↑(basicOpen 𝒜 f)).toSpecΓ ≫ Spec.map (basicOpen 𝒜 f).topIso.inv) ≫ Spec.map (awayToSection 𝒜 f)) =
    ΓSpec.locallyRingedSpaceAdjunction.unit.app (Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f)) ≫
      Spec.toLocallyRingedSpace.map (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f).op
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 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ Submonoid.powers (f t) ≤ Submonoid.powers x

Tactic:
simp [H]

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

Goal state before:
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)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
this : a ∈ Submodule.span ↥(𝒜 0) ↑(Submonoid.closure (Set.range v))
⊢ mk { deg := n, num := ((decompose 𝒜) a) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    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:
induction this using Submodule.span_induction with
  | mem a ha' =>
    obtain ⟨ai, rfl⟩ := Submonoid.exists_of_mem_closure_range _ _ ha'
    clear ha'
    by_cases H : ∑ i, ai i • dv i = n
    · apply Submodule.subset_span
      refine ⟨j, ai, H.trans ?_, ?_⟩
      · exact DirectSum.degree_eq_of_mem_mem 𝒜 hb'
          (SetLike.pow_mem_graded j hf) hfj
      · ext
        simp only [val_mk, Away.val_mk]
        congr
        refine (DirectSum.decompose_of_mem_same _ ?_).symm
        exact H ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
    · convert! zero_mem (Submodule.span (𝒜 0) _)
      ext
      have : (DirectSum.decompose 𝒜 (∏ i : ι', v i ^ ai i) n).1 = 0 := by
        refine DirectSum.decompose_of_mem_ne _ ?_ H
        exact SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
      simp [this, Localization.mk_zero]
  | zero =>
    convert! zero_mem (Submodule.span (𝒜 0) _)
    ext; simp [Localization.mk_zero]
  | add s t hs ht hs' ht' =>
    convert! add_mem hs' ht'
    ext; simp [← Localization.add_mk_self]
  | smul r x hx hx' =>
    convert! Submodule.smul_mem _ r hx'
    ext
    simp [Algebra.smul_def, algebraMap_eq, fromZeroRingHom, Localization.mk_mul,
      -decompose_mul, coe_decompose_mul_of_left_mem_zero 𝒜 r.2]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst✝¹³ : Semiring A
inst✝¹² : Semiring B
inst✝¹¹ : Semiring C
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : SetLike ω C
inst✝⁷ : AddSubmonoidClass σ A
inst✝⁶ : AddSubmonoidClass τ B
inst✝⁵ : AddSubmonoidClass ω C
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
i : ι
b : B
hb : b ∈ Ideal.span (⇑f '' ↑I.toIdeal)
⊢ ↑(((DirectSum.decompose ℬ) b) i) ∈ Ideal.map f I.toIdeal

Tactic:
induction hb using Submodule.span_induction generalizing i with
    | zero => simp
    | add => simp [*, Ideal.add_mem]
    | mem a ha =>
      obtain ⟨a, ha, rfl⟩ := ha
      rw [← f.map_directSumDecompose]
      exact Ideal.mem_map_of_mem _ (I.2 _ ha)
    | smul a₁ a₂ ha₂ ih =>
      classical rw [smul_eq_mul, DirectSum.decompose_mul, DirectSum.coe_mul_apply]
      exact sum_mem fun ij hij ↦ Ideal.mul_mem_left _ _ <| ih _

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
⊢ ∀ (a : Set A), ∃ s, comapFun f hf ⁻¹' zeroLocus 𝒜 a = zeroLocus ℬ s

Tactic:
exact fun s ↦ ⟨f '' s, by ext; simp⟩

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)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
i : ι
n : ℕ
t' : ↑Γ(M, basicOpen (g i))
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = g i ^ n • f ^ n • s' i
ψ : Module.End ↑R ↑Γ(M, basicOpen (g i))
hψ : (algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ n) * ψ = 1
⊢ g i ^ n • f ^ n • s' i = g i ^ n • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (ψ t')

Tactic:
← ht',

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)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
i : ι
n : ℕ
t' : ↑Γ(M, basicOpen (g i))
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = g i ^ n • f ^ n • s' i
ψ : Module.End ↑R ↑Γ(M, basicOpen (g i))
hψ : (algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ n) * ψ = 1
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' =
    g i ^ n • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (ψ t')
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
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.fst (f S i) (f S j) =
    (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp) ≫ pullback.fst (f S i) (f S j)
fac₂ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.snd (f S i) (f S j) =
    (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp) ≫ pullback.snd (f S i) (f S j)
⊢ (Sieve.functorPushforward F
        ({ I₀ := ι S, X := U S, f := f S, I₁ := fun i j ↦ ι (pullback (f S i) (f S j)),
              Y := fun i j ↦ U (pullback (f S i) (f S j)),
              p₁ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
              w := ⋯ }.sieve₁₀
          p₁ p₂)).arrows
    (r ≫ F.map q)

Tactic:
simp only [Category.assoc, pullback.lift_fst, pullback.lift_snd] at fac₁ 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
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j) = F.map q ≫ F.map p₁
fac₂ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j) = F.map q ≫ F.map p₂
⊢ (Sieve.functorPushforward F
        ({ I₀ := ι S, X := U S, f := f S, I₁ := fun i j ↦ ι (pullback (f S i) (f S j)),
              Y := fun i j ↦ U (pullback (f S i) (f S j)),
              p₁ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
              w := ⋯ }.sieve₁₀
          p₁ p₂)).arrows
    (r ≫ F.map q)