mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
⊢ closedBall x r = closedBall y r ∨ Disjoint (closedBall x r) (closedBall y r)

Tactic:
by
  refine Set.disjoint_or_nonempty_inter (closedBall x r) (closedBall y r) |>.symm.imp
    (fun h ↦ ?_) id
  have h₁ := closedBall_eq_of_mem <| Set.inter_subset_left h.some_mem
  have h₂ := closedBall_eq_of_mem <| Set.inter_subset_right h.some_mem
  exact h₁.trans h₂.symm

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
t : Finset ι
inst✝ : Nonempty ι
f : ι → M
⊢ ∃ i, (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Goal state after:
case inl
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
inst✝ : Nonempty ι
f : ι → M
⊢ ∃ i, (∅.Nonempty → i ∈ ∅) ∧ ‖∏ j ∈ ∅, f j‖ ≤ ‖f i‖

case inr
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
t : Finset ι
inst✝ : Nonempty ι
f : ι → M
ht : t.Nonempty
⊢ ∃ i, (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
by_cases h : Multipliable f

Goal state after:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hu : ↑(toLex u) < φ.lexOrder
⊢ (coeff u) φ * (coeff v) ψ = 0

pp: case inr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hv : ↑(toLex v) < ψ.lexOrder
⊢ (coeff u) φ * (coeff v) ψ = 0

Tactic:
· rw [coeff_eq_zero_of_lt_lexOrder hu, zero_mul]

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hv : ↑(toLex v) < ψ.lexOrder
⊢ (coeff u) φ * (coeff v) ψ = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
⊢ (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R) ↔ r ∈ nonZeroDivisorsRight R

Tactic:
by
  constructor
  · intro H s hrs
    have := H (C s) (by rw [← monomial_zero_eq_C, monomial_mul_monomial]; ext; simp [hrs])
    simpa using congr(coeff 0 $(this))
  · intro H p hrp
    ext i
    have := congr(coeff (i + n) $hrp)
    rw [coeff_mul_monomial, if_pos le_add_self, add_tsub_cancel_right] at this
    simpa using H _ this

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0 ∨ (weightedHomogeneousComponent w q) g = 0
⊢ False

Tactic:
rcases H with H | H

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ False

case inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = constantCoeff φ
⊢ IsUnit φ ∨ IsUnit (1 - φ)

Tactic:
left

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = constantCoeff φ
⊢ IsUnit φ
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ ¬(Set.range ⇑Valued.v).Subsingleton

Tactic:
simpa using Valued.v.range_nontrivial

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
hr : Presieve.Arrows.Compatible F E.f s
s' : Presieve.FamilyOfElements F (Presieve.ofArrows E.X E.f)
hs' : ∀ (i : E.I₀), s' (E.f i) ⋯ = s i
t' : F.obj (op X)
ht' : ∀ (i : E.I₀), (ConcreteCategory.hom (F.map (E.f i).op)) t' = s i
hunique :
  ∀ (y : (fun X ↦ X) (F.obj (op X))),
    (fun t ↦ ∀ (i : E.I₀), (ConcreteCategory.hom (F.map (E.f i).op)) t = s i) y → y = t'
y : F.obj (op X)
hy : (fun t_1 ↦ t.IsAmalgamation t_1) y
i : E.I₀
Z : C
g : Z ⟶ E.X i
hg : (Sieve.pullback (E.f i) S).arrows g
⊢ (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (F.map (E.f i).op)) y) =
    Presieve.FamilyOfElements.pullback (E.f i) t g hg

Tactic:
simp [Presieve.FamilyOfElements.pullback, ← hy _ hg]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Projective R
W : Projective F
x✝¹ x✝ : W.Point
⊢ x✝¹ + x✝ = x✝ + x✝¹

Tactic:
by
    classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_comm]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
s : A
a : S
x : S ⊗[R] Ω[A⁄R]
⊢ s • a • x = a • s • x

Tactic:
rw [← smul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Pointwise

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : x - y ∈ U
c : R
hc : c ∈ I
⊢ c • x - c • y ∈ I • U

Tactic:
← smul_sub

Goal state after:
R : Type u_1
inst✝² : Ring R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : x - y ∈ U
c : R
hc : c ∈ I
⊢ c • (x - y) ∈ I • U
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ map I LinearMap.id = LinearMap.id

Tactic:
ext a n

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : AdicCauchySequence I M
n : ℕ
⊢ ↑((map I LinearMap.id) ((mk I M) a)) n = ↑(LinearMap.id ((mk I M) a)) n
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: case smul
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y✝ : N
n : ℕ
r : R
hr : r ∈ I ^ n
y : N
hn✝ : y ∈ ⊤
⊢ ∃ x ∈ I ^ n • ⊤, f x ≡ r • y [SMOD I ^ (n + 1) • ⊤]

Tactic:
obtain ⟨x, hx⟩ := h (mkQ _ y)
    use r • x, smul_mem_smul hr mem_top
    simp only [coe_comp, Function.comp_apply, mkQ_apply, ← SModEq.def, map_smul] at ⊢ hx
    rw [pow_succ, ← smul_smul]
    exact SModEq.smul' hx hr

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = I ^ m • ⊤
⊢ (Ideal.Quotient.mk (I ^ m)) (↑r n) = (Ideal.Quotient.mk (I ^ m)) (↑r m)

Tactic:
rw [← Ideal.Quotient.mk_eq_mk, ← Ideal.Quotient.mk_eq_mk, h]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = I ^ m • ⊤
⊢ Submodule.Quotient.mk (↑r n) = Submodule.Quotient.mk (↑r m)
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case convert_6.refine_2
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
n : ℕ
d : N
hdmem : d ∈ I ^ (k + n + 1) • ⊤
y yₙ : M
hd : f y = ↑x (k + n + 1) - d
hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤
⊢ d ∈ I ^ (k + n) • ⊤

Tactic:
· exact (Submodule.smul_mono_left (Ideal.pow_le_pow_right (by lia))) hdmem

Goal state after:
Module: Mathlib.RingTheory.Smooth.AdicCompletion

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m n : ℕ
hn : m ≤ n
⊢ (Ideal.Quotient.factorₐ R ⋯).comp (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m

Tactic:
by
  induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hmn ih =>
    rw [← Ideal.Quotient.factorₐ_comp _
      (Ideal.pow_le_pow_right n.le_succ) (Ideal.pow_le_pow_right hmn), AlgHom.comp_assoc]
    simpa

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : Fintype σ'
i j : σ
⊢ (aeval (Q.comp P).val) ((Q.comp P).jacobiMatrix (Sum.inr i) (Sum.inr j)) =
    eval₂ ((algebraMap S T).comp (algebraMap R S)) (fun i ↦ (algebraMap S T) (P.val i)) (P.jacobiMatrix i j)

Tactic:
rw [jacobiMatrix_comp_inr_inr, ← IsScalarTower.algebraMap_eq]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : Fintype σ'
i j : σ
⊢ (aeval (Q.comp P).val) ((rename Sum.inr) (P.jacobiMatrix i j)) =
    eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) (P.jacobiMatrix i j)
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : P.HasCoeffs R₀
inst✝¹ : Finite ι
inst✝ : Finite σ
⊢ FinitePresentation R₀ (ModelOfHasCoeffs R₀)

Tactic:
cases nonempty_fintype σ
  exact .quotient ⟨Finset.image (P.relationOfHasCoeffs R₀) .univ, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addX P Q = P y ^ 2 * Q z * Q x

Tactic:
by
  rw [addX, hPz, X_eq_zero_of_Z_eq_zero hP hPz]
  ring1

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
n : ℕ
hf : IsStandardSmoothOfRelativeDimension n f
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
g : MvPolynomial (Fin n) R →ₐ[R] S
hg : g.Etale
⊢ ∃ g, g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
exact ⟨_, g.comp_algebraMap, hg⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ Smooth f ↔
    ∀ (x : ↥X),
      ∃ U,
        ∃ (_ : IsAffineOpen U),
          ∃ V,
            ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

Tactic:
by
  have : HasRingHomProperty @Smooth.{u} (Locally IsStandardSmooth) := by
    convert! (inferInstance : HasRingHomProperty (@Smooth.{u}) RingHom.Smooth)
    ext f
    rw [RingHom.smooth_iff_locally_isStandardSmooth]
  rw [HasRingHomProperty.iff_exists_appLE_locally (P := @Smooth)]
  · congr!
    simp [Subtype.exists]
    grind [Scheme.affineOpens]
  · exact isStandardSmooth_stableUnderCompositionWithLocalizationAway.left
  · exact isStandardSmooth_respectsIso

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
x : ↥X
⊢ Algebra.IsSeparable ↑(Y.residueField (f x)) ↑(X.residueField x)

Tactic:
algebraize [(f.stalkMap x).hom]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
x : ↥X
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
⊢ Algebra.IsSeparable ↑(Y.residueField (f x)) ↑(X.residueField x)
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝³ : HasPullbacks C
P Q : MorphismProperty C
inst✝² : P.DescendsAlong Q
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
⊢ ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g], Q f → P.diagonal (pullback.fst f g) → P.diagonal g

Tactic:
introv hf hfst

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
⊢ P.diagonal g
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : FaithfulSMul S L
x y : S
hy : y ∈ conductor R x
z : S
⊢ ∃ x_1 ∈ R[x], (algebraMap S L) x_1 = (algebraMap S L) y * (algebraMap S L) z

Tactic:
exact ⟨_, hy z, map_mul _ _ _⟩

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

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f✝)
algInst✝ : Algebra R S := f✝.toAlgebra
P : Ideal R
x✝ : P.IsPrime
this✝¹ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this✝ : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
a : P.Fiber S
ha : f a = 0
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : ↑(P.primesOver S) := (PrimeSpectrum.primesOverOrderIsoFiber R S P).symm { asIdeal := J, isPrime := ⋯ }
this : ¬↑s ⊆ ↑↑I
r : S
hrs : r ∈ ↑s
hrI : r ∉ ↑↑I
⊢ Submonoid.powers r ≤ Submonoid.comap Algebra.TensorProduct.includeRight.toRingHom J.primeCompl

Tactic:
by
      simpa [Submonoid.powers_le] using! hrI

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : q ∈ minimalPrimes S
u : S
p : R[X]
e : (aeval x) p * u ∈ q
⊢ map (algebraMap R (S ⧸ q)) p * C ((Ideal.Quotient.mk q) u) = 0

Tactic:
have := hq.1.1

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : q ∈ minimalPrimes S
u : S
p : R[X]
e : (aeval x) p * u ∈ q
this : q.IsPrime
⊢ map (algebraMap R (S ⧸ q)) p * C ((Ideal.Quotient.mk q) u) = 0
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : q ∈ minimalPrimes S
u : S
p : R[X]
e : (aeval x) p * u ∈ q
this✝¹ : q.IsPrime
this✝ : Ring.KrullDimLE 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := ⋯.toField
⊢ (algebraMap S (Localization.AtPrime q)) ((aeval x) p * u) ∈ Ideal.map (algebraMap S (Localization.AtPrime q)) q

Tactic:
exact Ideal.mem_map_of_mem _ e

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z✝ : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z✝
lem :
  ∀ {a : R},
    a ∈ I →
      l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
z : ↥R[x]
hz : z ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I)
y : ↥R[x]
hy : y ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I)
⊢ (algebraMap (↥R[x]) S) z + (algebraMap (↥R[x]) S) y ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
rw [← map_add]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z✝ : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z✝
lem :
  ∀ {a : R},
    a ∈ I →
      l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
z : ↥R[x]
hz : z ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I)
y : ↥R[x]
hy : y ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I)
⊢ (algebraMap (↥R[x]) S) (z + y) ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
Module: Mathlib.FieldTheory.RatFunc.Defs

Goal state before:
pp: K : Type u
inst✝ : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ { toFractionRing := Localization.mk n d }.liftOn f H = f n ↑d

Tactic:
RatFunc.liftOn

Goal state after:
K : Type u
inst✝ : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ Localization.liftOn { toFractionRing := Localization.mk n d }.toFractionRing (fun p q ↦ f p ↑q) ⋯ = f n ↑d
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommSemiring A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : 1 < v w
p : A[X]
hp : p ≠ 0
⊢ v ((aeval w) p) = v ((aeval w) ((monomial p.natDegree) p.leadingCoeff))

Tactic:
nth_rw 1 [as_sum_range p, map_sum]

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommSemiring A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : 1 < v w
p : A[X]
hp : p ≠ 0
⊢ v (∑ x ∈ Finset.range (p.natDegree + 1), (aeval w) ((monomial x) (p.coeff x))) =
    v ((aeval w) ((monomial p.natDegree) p.leadingCoeff))
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f g : K[X]
hg : g ≠ 0
⊢ (valuation K⟮X⟯ (idealX K)) (RatFunc.mk f g) = (idealX K).intValuation f / (idealX K).intValuation g

Tactic:
by
  simp only [RatFunc.mk_eq_mk' _ hg, valuation_of_mk']

Goal state after: