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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' :
  Polynomial.eval₂ (F.comp (universalFactorizationMap ℤ n m k hn).toRingHom) (F.toRingHom (X i ⊗ₜ[ℤ] 1)) p =
    F.toRingHom 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (X i ⊗ₜ[R] 1)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0

Tactic:
← MvPolynomial.universalFactorizationMap_comp_map

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' :
  Polynomial.eval₂ ((universalFactorizationMap R n m k hn).comp (map (algebraMap ℤ R))) (F.toRingHom (X i ⊗ₜ[ℤ] 1)) p =
    F.toRingHom 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (X i ⊗ₜ[R] 1)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' :
  Polynomial.eval₂ (F.comp (universalFactorizationMap ℤ n m k hn).toRingHom) (F.toRingHom (1 ⊗ₜ[ℤ] X i)) p =
    F.toRingHom 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (1 ⊗ₜ[R] X i)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0

Tactic:
← MvPolynomial.universalFactorizationMap_comp_map

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' :
  Polynomial.eval₂ ((universalFactorizationMap R n m k hn).comp (map (algebraMap ℤ R))) (F.toRingHom (1 ⊗ₜ[ℤ] X i)) p =
    F.toRingHom 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (1 ⊗ₜ[R] X i)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝³ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this✝² : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
this✝¹ : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
this✝ : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i✝ : Fin k
⊢ ((AlgHom.restrictScalars R
            (AlgHom.restrictScalars R
              ((AlgHom.restrictScalars (MvPolynomial (Fin n) R)
                    ((fun q ↦
                        Algebra.TensorProduct.lift (Algebra.ofId R S)
                          (let __RingHom :=
                            (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn
                                      (p.map (algebraMap R S))).symm
                                  q)).toRingHom;
                          { toRingHom := __RingHom, commutes' := ⋯ })
                          ⋯)
                      ((fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩) f))).comp
                Algebra.TensorProduct.includeRight))).comp
        Algebra.TensorProduct.includeRight)
      (MvPolynomial.X i✝) =
    ((AlgHom.restrictScalars R
            (AlgHom.restrictScalars R
              ((AlgHom.restrictScalars (MvPolynomial (Fin n) R) f).comp Algebra.TensorProduct.includeRight))).comp
        Algebra.TensorProduct.includeRight)
      (MvPolynomial.X i✝)

Tactic:
simp [MvPolynomial.universalFactorizationMapLiftEquiv, MvPolynomial.mapEquivMonic,
        UniversalFactorizationRing.factor₂, coeff_freeMonic]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝³ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this✝² : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
this✝¹ : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
this✝ : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i✝ : Fin k
⊢ f ((fromTensor m k hn p) (1 ⊗ₜ[R] MvPolynomial.X i✝)) = f (1 ⊗ₜ[MvPolynomial (Fin n) R] (1 ⊗ₜ[R] MvPolynomial.X i✝))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree

Tactic:
by_contra! H
        replace H := natDegree_mul_le.trans_lt H
        rw [add_comm, ← hf.natDegree_mul' hb0, mul_comm f] at H
        have := natDegree_add_eq_left_of_natDegree_lt H
        simp only [e, natDegree_one] at this
        lia

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ (-1) ^ (f.natDegree * (f.natDegree - 1)) * ((derivative f).sylvester f (f.natDegree - 1) f.natDegree).det =
    (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff * f.discr

Tactic:
← sylvesterDeriv_updateRow f hf,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ (-1) ^ (f.natDegree * (f.natDegree - 1)) *
      (f.sylvesterDeriv.updateRow ⟨2 * f.natDegree - 2, ⋯⟩
          (f.leadingCoeff • f.sylvesterDeriv ⟨2 * f.natDegree - 2, ⋯⟩)).det =
    (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff * f.discr
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
G : C
inst✝¹ : GrpObj G
inst✝ : BraidedCategory C
⊢ IsCommMonObj G ↔ GrpObj.commutator G = toUnit (G ⊗ G) ≫ η

Tactic:
rw [isCommMonObj_iff_isMulCommutative]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
G : C
inst✝¹ : GrpObj G
inst✝ : BraidedCategory C
⊢ (∀ (X : C), IsMulCommutative (X ⟶ G)) ↔ GrpObj.commutator G = toUnit (G ⊗ G) ≫ η
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

Tactic:
simp_rw [right_triangle]

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫ g₂ ◁ ((ρ_ g₁).hom ≫ (λ_ g₁).inv) ⊗≫ ((ρ_ g₂).hom ≫ (λ_ g₂).inv) ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
a b : B
f : a ⟶ b
g : b ⟶ a
F : B ⥤ᵖ C
adj : f ⊣ g
⊢ leftZigzag ((F.mapId a).inv ≫ F.map₂ adj.unit ≫ (F.mapComp f g).hom)
      ((F.mapComp g f).inv ≫ F.map₂ adj.counit ≫ (F.mapId b).hom) =
    (F.mapId a).inv ▷ F.map f ⊗≫
      (F.mapComp (𝟙 a) f).inv ≫
        F.map₂ (leftZigzag adj.unit adj.counit) ≫ (F.mapComp f (𝟙 b)).hom ⊗≫ F.map f ◁ (F.mapId b).hom

Tactic:
by
  simp [leftZigzag, bicategoricalComp]

Goal state after:
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✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
p : PrimeSpectrum R
⊢ Nontrivial (p.asIdeal.Fiber S) ↔ p ∈ Set.range (comap (algebraMap R S))

Tactic:
p.nontrivial_iff_mem_rangeComap

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
p : PrimeSpectrum R
⊢ p ∈ Set.range (comap (algebraMap R S)) ↔ p ∈ Set.range (comap (algebraMap R S))
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₁' : a ⟶ b
r₁' : b ⟶ a
adj₁' : l₁' ⊣ r₁'
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
φ : l₁' ⟶ l₁
⊢ (conjugateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂)) (φ ▷ l₂) = r₂ ◁ (conjugateEquiv adj₁ adj₁') φ

Tactic:
have := mateEquiv_hcomp adj₁ adj₁' adj₂ adj₂
    ((λ_ _).hom ≫ φ ≫ (ρ_ _).inv) ((λ_ _).hom ≫ (ρ_ _).inv)
  dsimp [leftAdjointSquare.hcomp, rightAdjointSquare.hcomp] at this
  simp only [comp_whiskerRight, leftUnitor_whiskerRight, Category.assoc, whiskerLeft_comp,
    whiskerLeft_rightUnitor_inv, Iso.hom_inv_id, Category.comp_id, triangle_assoc,
    inv_hom_whiskerRight_assoc, Iso.inv_hom_id_assoc, mateEquiv_leftUnitor_hom_rightUnitor_inv,
    leftUnitor_inv_whiskerRight, Iso.inv_hom_id, triangle_assoc_comp_right_assoc] at this
  simp [conjugateEquiv_apply, this]

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₂
β : r₁ ≅ r₂
⊢ (conjugateEquiv adj₁ adj₂).symm β.hom ≫ (conjugateEquiv adj₂ adj₁).symm β.inv = 𝟙 l₂

Tactic:
rw [conjugateEquiv_symm_comp, Iso.inv_hom_id, conjugateEquiv_symm_id]

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
e :
  NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl f =
    NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl g
⊢ (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑f.den) x ⋯))
      (sectionInBasicOpen 𝒜 x f) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑g.den) x ⋯))
      (sectionInBasicOpen 𝒜 x g)

Tactic:
simp only [HomogeneousLocalization.NumDenSameDeg.embedding, Localization.mk_eq_mk',
      IsLocalization.mk'_eq_iff_eq,
      IsLocalization.eq_iff_exists x.asHomogeneousIdeal.toIdeal.primeCompl] at e

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
e : ∃ c, ↑c * (↑g.den * ↑f.num) = ↑c * (↑f.den * ↑g.num)
⊢ (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑f.den) x ⋯))
      (sectionInBasicOpen 𝒜 x f) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑g.den) x ⋯))
      (sectionInBasicOpen 𝒜 x g)
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
z : A
⊢ z ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal → z ∈ Ideal.span (Set.range fun i ↦ ↑i.snd)

Tactic:
hz

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
hz : z ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal
⊢ z ∈ Ideal.span (Set.range fun i ↦ ↑i.snd)
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
⊢ X.basicOpen (f r) ≤ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r

Tactic:
· intro x hx
    let I : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀ := ⟨n, r, hn, hr⟩
    obtain ⟨x, rfl⟩ : x ∈ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I).opensRange := by
      simpa [openCoverOfMapIrrelevantEqTop] using hx
    rw [← SetLike.mem_coe] -- TODO : mem version of TopologicalSpace.Opens.map_coe
    simp only [TopologicalSpace.Opens.map_coe, Set.mem_preimage,
      ← Scheme.Hom.comp_apply, fromOfGlobalSections]
    simp

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
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✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ map f (𝒜₊)
hg : 𝒞₊ ≤ map g (ℬ₊)
⊢ 𝒞₊ ≤ map (g.comp f) (𝒜₊)

Tactic:
map_comp

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
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✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ map f (𝒜₊)
hg : 𝒞₊ ≤ map g (ℬ₊)
⊢ 𝒞₊ ≤ map g (map f (𝒜₊))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

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

Tactic:
(_ : m • n = _)

Goal state after:
case refine_2.refine_1
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 ^ n ∈ 𝒜 ?m.422

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 • n = ?m.422
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
⊢ False

Tactic:
have h_RleSₘ : R ≤ fSₘ := by
    refine ⟨hS.le.trans (LocalSubring.le_ofPrime ..), ((local_hom_TFAE _).out 2 0).mp ?_⟩
    conv_rhs => rw [← IsLocalization.AtPrime.map_eq_maximalIdeal M]
    refine .trans ?_ (Ideal.map_mono h_incl)
    rw [Ideal.map_map]; rfl

Goal state after:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
h_RleSₘ : R ≤ fSₘ
⊢ False
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ awayToSection 𝒜 f ≫ (structureSheaf 𝒜).obj.map (homOfLE ⋯).op ≫ (Proj.restrict ⋯).presheaf.Γgerm x =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫
      («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv

Tactic:
← Category.assoc _ (Iso.inv _),

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ awayToSection 𝒜 f ≫ (structureSheaf 𝒜).obj.map (homOfLE ⋯).op ≫ (Proj.restrict ⋯).presheaf.Γgerm x =
    (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv) ≫
      (Proj.restrictStalkIso ⋯ x).inv
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)
⊢ (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:
have fac₂ := fac =≫ pullback.snd _ _

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 ≫ 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)