mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
⊢ (LinearMap.toMatrix ((degreeLT.basis R m).prod (degreeLT.basis R n)) (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n)

Tactic:
by
  ext i (j | j)
  · suffices (if j.1 ≤ i then g.coeff (i - j) else 0) =
      if j ≤ i.1 ∧ ↑i ≤ j + n then g.coeff (i - j) else 0 by
        simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']
    rw [ite_and]
    split_ifs with h₁ h₂ <;> try rfl
    exact coeff_eq_zero_of_natDegree_lt (by lia)
  · suffices (if j.1 ≤ i then f.coeff (i - j) else 0) =
      if j ≤ i.1 ∧ ↑i ≤ j + m then f.coeff (i - j) else 0 by
        simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']
    rw [ite_and]
    split_ifs with h₁ h₂ <;> try rfl
    exact coeff_eq_zero_of_natDegree_lt (by lia)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  f.sylvesterMap g hf hg ∘ₗ (Matrix.toLin b₂ b₁) (f.sylvester g m n).adjugate =
    (f.sylvester g m n).det • (Matrix.toLin b₂ b₂) 1
⊢ f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g = f.resultant g m n • LinearMap.id

Tactic:
Matrix.toLin_one,

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  f.sylvesterMap g hf hg ∘ₗ (Matrix.toLin b₂ b₁) (f.sylvester g m n).adjugate = (f.sylvester g m n).det • LinearMap.id
⊢ f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g = f.resultant g m n • LinearMap.id
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  (Matrix.toLin b₂ b₁) (f.sylvester g m n).adjugate ∘ₗ f.sylvesterMap g hf hg =
    (f.sylvester g m n).det • (Matrix.toLin b₁ b₁) 1
⊢ f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg = f.resultant g m n • LinearMap.id

Tactic:
Matrix.toLin_one,

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  (Matrix.toLin b₂ b₁) (f.sylvester g m n).adjugate ∘ₗ f.sylvesterMap g hf hg = (f.sylvester g m n).det • LinearMap.id
⊢ f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg = f.resultant g m n • LinearMap.id
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q✝ : Ideal S
inst✝² : q✝.IsPrime
inst✝¹ : q✝.LiesOver p
inst✝ : QuasiFiniteAt R q✝
s : S
hsq : s ∉ q✝
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q✝ → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q✝ → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
f : R[X] := X * minpoly R s
q : p.ResidueField[X]
hq' : ¬X - C 0 ∣ q
hqm : q.Monic
m' : ℕ := rootMultiplicity 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s))
hq : Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) = (X - C 0) ^ m' * q
⊢ (aeval s) f = 0

Tactic:
simp [f]

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
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H✝ : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H✝
H : (toNormalization f ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r = opensRange (X.homOfLE ⋯)
⊢ IsIso (app (toNormalization f) ((normalization f).basicOpen r))

Tactic:
have := (inferInstance : IsIso ((toNormalization f ∣_ V y).app
      (Scheme.homOfLE _ hrV).opensRange))

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H✝ : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H✝
H : (toNormalization f ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r = opensRange (X.homOfLE ⋯)
this : IsIso (app (toNormalization f ∣_ V y) (opensRange ((normalization f).homOfLE hrV)))
⊢ IsIso (app (toNormalization f) ((normalization f).basicOpen r))
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
⊢ Function.Injective ⇑f

Tactic:
simp [f]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
s : S
x : ↥I
⊢ f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ[R] x)

Tactic:
simp [f]

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
⊢ IsOpenImmersion f

Tactic:
let U : Y.Opens := ⟨Set.range f.base, f.isOpenMap.isOpen_range⟩
    -- needed to prevent `wlog` to go in a typeclass loop
    have hU : IsOpenImmersion U.ι := U.instIsOpenImmersionι
    let f' := hU.lift U.ι f (by simp [U])
    have heq : f = f' ≫ U.ι := by simp [f']
    have hflat : Flat f' :=
      of_postcomp (W := @Flat) f' U.ι hU (by rwa [← heq])
    have hfinpres : LocallyOfFinitePresentation f' :=
      of_postcomp (W := @LocallyOfFinitePresentation) f' U.ι hU (by rwa [← heq])
    have hmono : Mono f' := mono_of_mono_fac heq.symm
    rw [heq]
    have := this f' ⟨fun ⟨x, ⟨y, hy⟩⟩ ↦
      ⟨y, by apply U.ι.injective; simp [← Scheme.Hom.comp_apply, f', hy]⟩⟩
    infer_instance

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
a : S
s : Finset S
has : a ∉ 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
ha : IsIntegral R a
this✝ : Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
this : Free S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
algInst✝ : Algebra S' S := f.toAlgebra
⊢ Polynomial.eval₂ (↑(Algebra.ofId S' S)) a (Polynomial.map (algebraMap R S') (minpoly R a)) = 0

Tactic:
simp [← Polynomial.aeval_def]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⋯
this : Function.Surjective (Function.invFun ι)
⊢ ↑n + 1 ≤ ringKrullDim R + (↑n + 1)

Tactic:
· exact WithBot.le_add_self Order.bot_lt_krullDim.ne' _

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
⊢ (ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫ (λ_ r₂).hom =
    (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ r₂).hom

Tactic:
mateEquiv_apply'

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
⊢ (ρ_ r₁).inv ≫
      (𝟙 (r₁ ≫ 𝟙 c) ⊗≫
          r₁ ◁ 𝟙 c ◁ adj₂.unit ⊗≫ r₁ ◁ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ r₂ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₂ ⊗≫ 𝟙 (𝟙 d ≫ r₂)) ≫
        (λ_ r₂).hom =
    (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ r₂).hom
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ (ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₁) ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ≫ (λ_ r₁).hom = 𝟙 r₁

Tactic:
mateEquiv_apply'

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ (ρ_ r₁).inv ≫
      (𝟙 (r₁ ≫ 𝟙 c) ⊗≫
          r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
⊢ (ρ_ r).inv ≫ (mateEquiv adj (Adjunction.id c)) ((λ_ (𝟙 c)).hom ≫ α ≫ (ρ_ l).inv) ≫ (λ_ (𝟙 c)).hom =
    (ρ_ r).inv ≫ r ◁ α ≫ adj.counit

Tactic:
mateEquiv_apply'

Goal state after:
B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
⊢ (ρ_ r).inv ≫
      (𝟙 (r ≫ 𝟙 c) ⊗≫
          r ◁ 𝟙 c ◁ (Adjunction.id c).unit ⊗≫
            r ◁ ((λ_ (𝟙 c)).hom ≫ α ≫ (ρ_ l).inv) ▷ 𝟙 c ⊗≫ adj.counit ▷ 𝟙 c ▷ 𝟙 c ⊗≫ 𝟙 (𝟙 c ≫ 𝟙 c)) ≫
        (λ_ (𝟙 c)).hom =
    (ρ_ r).inv ≫ r ◁ α ≫ adj.counit
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso α

Tactic:
by
  suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
    by simpa only [Equiv.apply_symm_apply] using this
  infer_instance

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 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}

Tactic:
vanishingIdeal,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ ↑(⨅ x ∈ t, x.asHomogeneousIdeal) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}
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
I : ProjectiveSpectrum 𝒜
⊢ I ∈ (zeroLocus 𝒜 {f})ᶜ ↔ f ∉ I.asHomogeneousIdeal

Tactic:
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ f ∉ ↑I.asHomogeneousIdeal ↔ f ∉ I.asHomogeneousIdeal
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
⊢ ↑F ⊆ ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))

Tactic:
intro s

Goal state after:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
s : S
⊢ s ∈ ↑F → s ∈ ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))
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 : Away 𝒜 f
⊢ val ((awayMap 𝒜 hg hx) a) = (awayMapAux 𝒜 ⋯) a

Tactic:
by
  let e := RingEquiv.ofLeftInverse (f := algebraMap (Away 𝒜 x) (Localization.Away x))
    (h := (val_injective _).hasLeftInverse.choose_spec)
  dsimp [awayMap]
  convert_to! (e (e.symm ⟨awayMapAux 𝒜 (f := f) ⟨_, hx⟩ a,
    range_awayMapAux_subset 𝒜 hg hx ⟨_, rfl⟩⟩)).1 = _
  rw [e.apply_symm_apply]

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

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (Scheme.Opens.ι (PrimeSpectrum.basicOpen (f i.snd.fst)))
      ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
        ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x)) ∈
    ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f i.snd.fst))))) ''
      ↑((TopologicalSpace.Opens.map
              (Spec.map
                  (CommRingCat.ofHom
                    ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                      (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base).obj
          (PrimeSpectrum.basicOpen (Away.isLocalizationElem ⋯ hr)))
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ ↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen (f r))

Tactic:
TopologicalSpace.Opens.map_coe,

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (Scheme.Opens.ι (PrimeSpectrum.basicOpen (f i.snd.fst)))
      ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
        ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x)) ∈
    ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f i.snd.fst))))) ''
      ↑((TopologicalSpace.Opens.map
              (Spec.map
                  (CommRingCat.ofHom
                    ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                      (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base).obj
          (PrimeSpectrum.basicOpen (Away.isLocalizationElem ⋯ hr)))
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ ⇑X.toSpecΓ ⁻¹' ↑(PrimeSpectrum.basicOpen (f r))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case e_y
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
⊢ f ^ a = ↑⟨f ^ (a - ∑ i, dv i * (ai i / d)), ⋯⟩ * ↑(∏ i, ⟨f ^ dv i, ⋯⟩ ^ (ai i / d))

Tactic:
· simp only [SubmonoidClass.coe_finsetProd, ← pow_add, ← pow_mul,
        Finset.prod_pow_eq_pow_sum, SubmonoidClass.coe_pow]
      rw [tsub_add_cancel_of_le]
      rcases d.eq_zero_or_pos with hd | hd
      · simp [hd]
      rw [← mul_le_mul_iff_of_pos_right hd, ← smul_eq_mul (a := a), ← hai, Finset.sum_mul]
      simp_rw [smul_eq_mul, mul_comm (ai _), mul_assoc]
      gcongr
      exact Nat.div_mul_le_self (ai _) d

Goal state after:
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
have ⟨p, hp, hpx⟩ := exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top x _
    (maximalIdeal.isMaximal R.toSubring).ne_top
    (top_unique <| (map_maximalIdeal_eq_top_of_isMax hR this).ge.trans le_self_add)

Goal state after:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
p : Polynomial ↥R.toSubring
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (Polynomial.aeval ⅟x) p = 0
⊢ IsIntegral (↥R.toSubring) x⁻¹
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
A : LocalSubring K
⊢ ∀ c ⊆ Set.Ici A, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub

Tactic:
intro s

Goal state after:
K : Type u_3
inst✝ : Field K
A : LocalSubring K
s : Set (LocalSubring K)
⊢ s ⊆ Set.Ici A → IsChain (fun x1 x2 ↦ x1 ≤ x2) s → ∀ y ∈ s, ∃ ub, ∀ z ∈ s, z ≤ ub
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
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]; exact SetLike.pow_mem_graded _ f_deg

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

Goal state before:
pp: Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
⊢ ∃ Y f,
    ∃ (_ : R.arrows f),
      ∃ y_1,
        (ConcreteCategory.hom ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).map f)) y_1 =
          (SpecToEquivOfField Ω S).symm ⟨(𝒰.f i) y, a⟩

Tactic:
refine ⟨𝒰.X i, 𝒰.f i, hle _ _ ⟨i⟩, ?_⟩

Goal state after:
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
⊢ ∃ y_1,
    (ConcreteCategory.hom ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).map (𝒰.f i))) y_1 =
      (SpecToEquivOfField Ω S).symm ⟨(𝒰.f i) y, a⟩
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
⊢ (Presieve.singleton f).EffectiveEpimorphic ↔ EffectiveEpi f

Tactic:
constructor
  · intro (h : Nonempty _)
    rw [Sieve.generateSingleton_eq] at h
    constructor
    apply Nonempty.map (effectiveEpiStructOfIsColimit _) h
  · rintro ⟨h⟩
    change Nonempty _
    rw [Sieve.generateSingleton_eq]
    apply Nonempty.map (isColimitOfEffectiveEpiStruct _) h

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) (m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ s.pt),
    (∀ (j : (Sieve.generateFamily X π).arrows.category),
        (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = s.ι.app j) →
      m = H.desc (fun a ↦ s.ι.app { obj := Over.mk (π a), property := ⋯ }) ⋯

Tactic:
intro S m hm; dsimp
      generalize_proofs h₁ h₂
      apply H.uniq _ h₂
      intro a
      exact hm ⟨Over.mk (π a), a, 𝟙 _, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ -x₂ ≫ r' = x₃ ≫ b'

Tactic:
neg_eq_iff_add_eq_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ x₂ ≫ r' + x₃ ≫ b' = 0