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

Goal state before:
pp: case «3».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 1 < 5
⊢ (if 1 < 2 then if 1 ≤ 3 then f.coeff (3 - 1) else 0
    else if 1 ≤ 5 ∧ 1 ≤ 1 - 2 then f.coeff (3 - (1 - 2) + 1) * (↑(3 - (1 - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨1, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

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

Goal state before:
pp: case «3».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 2 < 5
⊢ (if 2 < 2 then if 2 ≤ 3 then f.coeff (3 - 2) else 0
    else if 2 ≤ 5 ∧ 1 ≤ 2 - 2 then f.coeff (3 - (2 - 2) + 1) * (↑(3 - (2 - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨2, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

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

Goal state before:
pp: case «3».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 3 < 5
⊢ (if 3 < 2 then if 3 ≤ 3 then f.coeff (3 - 3) else 0
    else if 3 ≤ 5 ∧ 1 ≤ 3 - 2 then f.coeff (3 - (3 - 2) + 1) * (↑(3 - (3 - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨3, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

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

Goal state before:
pp: case «3».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 ≤ 3 then f.coeff (3 - 4) else 0
    else if 4 ≤ 5 ∧ 1 ≤ 4 - 2 then f.coeff (3 - (4 - 2) + 1) * (↑(3 - (4 - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨4, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

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

Goal state before:
pp: case «4».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 0 < 5
⊢ (if 0 = 1 then 1 else if 0 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨0, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

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

Goal state before:
pp: case «4».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 1 < 5
⊢ (if 1 = 1 then 1 else if 1 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨1, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

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

Goal state before:
pp: case «4».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 2 < 5
⊢ (if 2 = 1 then 1 else if 2 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨2, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

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

Goal state before:
pp: case «4».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 3 < 5
⊢ (if 3 = 1 then 1 else if 3 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨3, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

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

Goal state before:
pp: case «4».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 4 < 5
⊢ (if 4 = 1 then 1 else if 4 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨4, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝ : Algebra.IsIntegral R' (Localization.Away e₀)
hgq : ¬IsUnit (1 ⊗ₜ[R'] (algebraMap (R' ⊗[R] R'') (Localization.Away e₀)) (1 ⊗ₜ[R] g))
m : Ideal (P.Fiber (Localization.Away e₀))
left✝ : m.IsMaximal
hm : Ideal.span {1 ⊗ₜ[R'] (algebraMap (R' ⊗[R] R'') (Localization.Away e₀)) (1 ⊗ₜ[R] g)} ≤ m
this :
  Ideal.comap (TensorProduct.includeRight.comp (algebraMap (R' ⊗[R] R'') (Localization.Away e₀))) m =
    Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
⊢ (algebraMap R'' S) g ∈ q

Tactic:
← hP'q

Goal state after:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝ : Algebra.IsIntegral R' (Localization.Away e₀)
hgq : ¬IsUnit (1 ⊗ₜ[R'] (algebraMap (R' ⊗[R] R'') (Localization.Away e₀)) (1 ⊗ₜ[R] g))
m : Ideal (P.Fiber (Localization.Away e₀))
left✝ : m.IsMaximal
hm : Ideal.span {1 ⊗ₜ[R'] (algebraMap (R' ⊗[R] R'') (Localization.Away e₀)) (1 ⊗ₜ[R] g)} ≤ m
this :
  Ideal.comap (TensorProduct.includeRight.comp (algebraMap (R' ⊗[R] R'') (Localization.Away e₀))) m =
    Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
⊢ (algebraMap R'' S) g ∈ Ideal.comap TensorProduct.includeRight.toRingHom P'
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
⊢ Smooth f

Tactic:
let Ω : Type u := AlgebraicClosure K
  let g : Spec (.of Ω) ⟶ Spec (.of K) := Spec.map (CommRingCat.ofHom <| algebraMap K Ω)
  apply MorphismProperty.of_pullback_snd_of_descendsAlong
    (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (g := g)
  · exact ⟨⟨inferInstance, inferInstance⟩, inferInstance⟩
  · let : GrpObj (Over.mk (Limits.pullback.snd f g)) := Over.grpObjMkPullbackSnd
    exact smooth_of_grpObj_of_isAlgClosed _

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ (e.hom ≫ e.inv).τl = 𝟙 adj₁.l

Tactic:
e.hom_inv_id,

Goal state after:
B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ (𝟙 adj₁).τl = 𝟙 adj₁.l
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ (e.hom ≫ e.inv).τr = 𝟙 adj₁.r

Tactic:
e.hom_inv_id,

Goal state after:
B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ (𝟙 adj₁).τr = 𝟙 adj₁.r
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✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
R' : Type u
w✝⁶ : CommRing R'
w✝⁵ : Algebra R R'
w✝⁴ : Etale R R'
P : Ideal R'
w✝³ : P.IsPrime
w✝² : P.LiesOver p
n : ℕ
e : Fin (n + 1) → R' ⊗[R] ULift.{u, v} S
he : CompleteOrthogonalIdempotents e
P' : Fin n → Ideal (R' ⊗[R] ULift.{u, v} S)
w✝¹ : ∀ (i : Fin n), (P' i).IsPrime
w✝ : ∀ (i : Fin n), (P' i).LiesOver P
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
hP' : ∀ (i : Fin n), e i.castSucc ∉ P' i
H :
  ∀ (P'' : Ideal (R' ⊗[R] ULift.{u, v} S)),
    P''.IsPrime → P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
e₁ : R' ⊗[R] S ≃ₐ[R'] R' ⊗[R] ULift.{u, v} S := TensorProduct.congr AlgEquiv.refl ULift.algEquiv.{u, v, u}.symm
P'' : Ideal (R' ⊗[R] S)
x✝¹ : P''.IsPrime
x✝ : P''.LiesOver P
⊢ (⇑e₁.symm ∘ e) (Fin.last n) ∈ P'' ∧
    ∀ (i : Fin n), (⇑e₁.symm ∘ e) i.castSucc ∉ P'' → P'' = (fun i ↦ Ideal.comap (↑e₁) (P' i)) i

Tactic:
have := H (P''.comap e₁.symm.toAlgHom) inferInstance inferInstance

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
R' : Type u
w✝⁶ : CommRing R'
w✝⁵ : Algebra R R'
w✝⁴ : Etale R R'
P : Ideal R'
w✝³ : P.IsPrime
w✝² : P.LiesOver p
n : ℕ
e : Fin (n + 1) → R' ⊗[R] ULift.{u, v} S
he : CompleteOrthogonalIdempotents e
P' : Fin n → Ideal (R' ⊗[R] ULift.{u, v} S)
w✝¹ : ∀ (i : Fin n), (P' i).IsPrime
w✝ : ∀ (i : Fin n), (P' i).LiesOver P
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
hP' : ∀ (i : Fin n), e i.castSucc ∉ P' i
H :
  ∀ (P'' : Ideal (R' ⊗[R] ULift.{u, v} S)),
    P''.IsPrime → P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
e₁ : R' ⊗[R] S ≃ₐ[R'] R' ⊗[R] ULift.{u, v} S := TensorProduct.congr AlgEquiv.refl ULift.algEquiv.{u, v, u}.symm
P'' : Ideal (R' ⊗[R] S)
x✝¹ : P''.IsPrime
x✝ : P''.LiesOver P
this :
  e (Fin.last n) ∈ Ideal.comap (↑e₁.symm) P'' ∧
    ∀ (i : Fin n), e i.castSucc ∉ Ideal.comap (↑e₁.symm) P'' → Ideal.comap (↑e₁.symm) P'' = P' i
⊢ (⇑e₁.symm ∘ e) (Fin.last n) ∈ P'' ∧
    ∀ (i : Fin n), (⇑e₁.symm ∘ e) i.castSucc ∉ P'' → P'' = (fun i ↦ Ideal.comap (↑e₁) (P' i)) i
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := ⋯
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ IsAffine.finrank (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g)) z = IsAffine.finrank (pullback.snd f g) t

Tactic:
· simp_rw [← hyr]
    exact IsAffine.finrank_snd (pullback.snd f g) (u ≫ pullback.snd _ _) z

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

Goal state before:
pp: X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst✝² : IsIso f
inst✝¹ : Flat g
inst✝ : IsFinite g
z : ↥S
e : pullback (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z)) ≅
  pullback g (S.affineOpenCover.f (S.affineOpenCover.idx z)) :=
  (pullbackRightPullbackFstIso g (S.affineOpenCover.f (S.affineOpenCover.idx z)) f).symm ≪≫
    asIso (pullback.snd f (pullback.fst g (S.affineOpenCover.f (S.affineOpenCover.idx z))))
⊢ e.hom ≫ pullback.snd g (S.affineOpenCover.f (S.affineOpenCover.idx z)) =
    pullback.snd (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z))

Tactic:
simp [e]

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

Goal state before:
pp: 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
ϖ : R
hϖ : Irreducible ϖ
⊢ (ordFrac R) ((algebraMap R K) ϖ) = WithZero.exp 1

Tactic:
simp [ordFrac_eq_valuation_inv, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap,
    IsDiscreteValuationRing.intValuation_maximalIdeal,
    IsDiscreteValuationRing.addVal_uniformizer hϖ, ← WithZero.exp_eq_coe_ofAdd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
hx : coheight x = 1
f : ↑X.functionField
hf : f ≠ 0
n : ℤ
⊢ n ≤ ord f x ↔ ↑(Multiplicative.ofAdd n) ≤ (ordHom x hx) f

Tactic:
rw [ord_eq_unzero_ordHom hx hf]

Goal state after:
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
hx : coheight x = 1
f : ↑X.functionField
hf : f ≠ 0
n : ℤ
⊢ n ≤ Multiplicative.toAdd (unzero ⋯) ↔ ↑(Multiplicative.ofAdd n) ≤ (ordHom x hx) f
Module: Mathlib.RingTheory.GradedAlgebra.RingHom

Goal state before:
pp: case mk
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
inst✝¹ : SetLike ψ C
inst✝ : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
g : 𝒜 →+*ᵍ ℬ
toRingHom✝ : A →+* B
map_mem✝ : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toRingHom✝ x ∈ ℬ i
h : (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, map_mem := map_mem✝ } = (fun f ↦ (↑↑f.toRingHom).toFun) g
⊢ { toRingHom := toRingHom✝, map_mem := map_mem✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
inst✝¹ : SetLike ψ C
inst✝ : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
toRingHom✝¹ : A →+* B
map_mem✝¹ : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toRingHom✝¹ x ∈ ℬ i
toRingHom✝ : A →+* B
map_mem✝ : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toRingHom✝ x ∈ ℬ i
h :
  (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝¹, map_mem := map_mem✝¹ } =
    (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, map_mem := map_mem✝ }
⊢ { toRingHom := toRingHom✝¹, map_mem := map_mem✝¹ } = { toRingHom := toRingHom✝, map_mem := map_mem✝ }
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
⊢ x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
hxy

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
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)
⊢ (Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯)
      ({ toFun := fun f_1 ↦ mk { deg := 0, num := f_1, den := 1, den_mem := ⋯ }, map_one' := ⋯, map_mul' := ⋯,
            map_zero' := ⋯, map_add' := ⋯ }
          a).val =
    ({ toFun := fun f ↦ mk { deg := 0, num := f, den := 1, den_mem := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        a).val

Tactic:
convert! IsLocalization.lift_eq _ _

Goal state after:
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 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ awayι 𝒜 f f_deg hm ≫
      (Proj 𝒜).topIso.inv ≫
        ((Proj 𝒜).isoOfEq ⋯).inv ≫
          ((basicOpen 𝒜 1).toSpecΓ ≫ Spec.map (awayToSection 𝒜 1)) ≫
            Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))

Tactic:
awayι

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ ((basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (basicOpen 𝒜 f).ι) ≫
      (Proj 𝒜).topIso.inv ≫
        ((Proj 𝒜).isoOfEq ⋯).inv ≫
          ((basicOpen 𝒜 1).toSpecΓ ≫ Spec.map (awayToSection 𝒜 1)) ≫
            Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
U : (Spec R).Opens
f : ↑R
hle : U ≤ PrimeSpectrum.basicOpen f
x y : ↑Γ(M, U)
⊢ (fun x ↦ f • x) x = (fun x ↦ f • x) y → x = y

Tactic:
hxy

Goal state after:
R : CommRingCat
M : (Spec R).Modules
U : (Spec R).Opens
f : ↑R
hle : U ≤ PrimeSpectrum.basicOpen f
x y : ↑Γ(M, U)
hxy : (fun x ↦ f • x) x = (fun x ↦ f • x) y
⊢ x = y
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: 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
⊢ ∑ x, (ai x % d + d * (ai x / d)) * dv x - (∑ i, dv i * (ai i / d)) * d = ∑ x, ai x % d * dv x

Tactic:
add_mul,

Goal state after:
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
⊢ ∑ x, (ai x % d * dv x + d * (ai x / d) * dv x) - (∑ i, dv i * (ai i / d)) * d = ∑ x, ai x % d * dv 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
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
this : ↑x = ↑y * (↑↑t)⁻¹ * ↑↑s
⊢ IsLocalization.mk' (Localization.AtPrime P) x s = IsLocalization.mk' (Localization.AtPrime P) y t

Tactic:
IsLocalization.mk'_eq_iff_eq

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 : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
this : ↑x = ↑y * (↑↑t)⁻¹ * ↑↑s
⊢ (algebraMap (↥A) (Localization.AtPrime P)) (↑t * x) = (algebraMap (↥A) (Localization.AtPrime P)) (↑s * y)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: 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
i : ι
m : ℕ
⊢ IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i) ^ m)

Tactic:
exact (Scheme.Modules.isUnit_algebraMap_end_of_le_basicOpen (g i) le_rfl).pow m

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
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) y ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } = 0

Tactic:
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
          HomogeneousLocalization.val_zero]

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
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ Localization.mk ↑{ deg := m * n, num := ⟨(proj 𝒜 n) y ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * n, num := ⟨(proj 𝒜 n) y ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    0
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
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) x ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } = 0

Tactic:
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
          HomogeneousLocalization.val_zero]

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
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ Localization.mk ↑{ deg := m * n, num := ⟨(proj 𝒜 n) x ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * n, num := ⟨(proj 𝒜 n) x ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    0