mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ z ∈ sphere c R, ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq : iteratedDeriv n f c = n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z
⊢ ‖n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z‖ ≤
    ↑n.factorial * (R * (C / R ^ (n + 1)))

Tactic:
rw [RCLike.norm_nsmul (K := ℂ), nsmul_eq_mul, mul_le_mul_iff_right₀ (by positivity)]

Goal state after:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ z ∈ sphere c R, ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq : iteratedDeriv n f c = n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z
⊢ ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z‖ ≤ R * (C / R ^ (n + 1))
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p * q = 0
⊢ Function.Injective ⇑(restrictProd p q)

Tactic:
have : Unique (p * q).Gal := by rw [hpq]; infer_instance
    exact fun f g _ => Eq.trans (Unique.eq_default f) (Unique.eq_default g).symm

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ esymm σ R n = ∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1)) 1

Tactic:
by
  simp_rw [monomial_sum_one, esymm, ← X_pow_eq_monomial, pow_one]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
r : F[X]
hr : Irreducible r
hr' : r.natDegree = 0
⊢ P r

Tactic:
exact Splits.of_natDegree_le_one <| natDegree_map_le.trans (hr'.trans_le zero_le_one)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ (map r s).esymm ((map r s).card - k) = (map r s).esymm (s.card - k)

Tactic:
rw [s.card_map r]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ k ≤ (map r s).card

Tactic:
rw [s.card_map r]

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ k ≤ s.card
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ nnnormHom s.prod ≤ B ^ ((map f p).natDegree - i)

Tactic:
← MonoidHom.coe_coe,

Goal state after:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ ↑nnnormHom s.prod ≤ B ^ ((map f p).natDegree - i)
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedAddMonoid M
inst✝² : One M
inst✝¹ : ZeroLEOneClass M
inst✝ : NeZero 1
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ num ≤ n * ↑den

Tactic:
by
  refine le_of_smul_le_smul_right (h.trans ?_) (by simp)
  rw [mul_comm, ← smul_smul]
  simpa using nsmul_le_nsmul_right hn den

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
⊢ a ∈ ratLt (x + y) ↔ a ∈ ratLt x + ratLt y

Tactic:
Set.mem_add

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
⊢ a ∈ ratLt (x + y) ↔ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H : ∃ y, y ≠ 1
H' : ∀ (x : K), v x ≠ 0 → v x = 1
⊢ False

Tactic:
obtain ⟨x, hx⟩ := H

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H' : ∀ (x : K), v x ≠ 0 → v x = 1
x : (ofClass v).ValueGroup₀ˣ
hx : x ≠ 1
⊢ False
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (closedBall x r ⊓ (ball x r)ᶜ)

Tactic:
exact (isOpen_closedBall x hr).inter (isClosed_ball x r).isOpen_compl

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

Goal state before:
pp: σ : 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
this : ↑(toLex u) < φ.lexOrder ∨ ↑(toLex v) < ψ.lexOrder
⊢ (coeff u) φ * (coeff v) ψ = 0

Tactic:
rcases this with (hu | hv)

Goal state after:
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

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.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y : L
⊢ v.norm (x * y) = v.norm x * v.norm y

Tactic:
simp only [Valuation.norm, ← NNReal.coe_mul, map_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (Ideal.span {X}).IsPrime

Tactic:
by
  suffices Ideal.span ({X} : Set R⟦X⟧) = RingHom.ker constantCoeff by
    rw [this]
    exact RingHom.ker_isPrime _
  apply Ideal.ext
  intro φ
  rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]

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 : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negY P = -P y

Tactic:
negY,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -P y - W'.a₁ * P x - W'.a₃ * P z = -P y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / P z + -W.a₃ * 1 - (W.toAffine.negY (P x / P z) (P y / P z) + -W.a₃ * (P z / P z)) = 0

Tactic:
negY,

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (-P y - W.a₁ * P x - W.a₃ * P z) / P z + -W.a₃ * 1 - (W.toAffine.negY (P x / P z) (P y / P z) + -W.a₃ * (P z / P z)) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - W'.negY P) * Q z + -W'.a₁ * (P x * Q z)) =
    0

Tactic:
negY,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - W'.negY P) * Q z + -W'.a₁ * (P x * Q z)) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ (eval P) W.polynomialY = (P y - W.negY P) * P z

Tactic:
negY,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ (eval P) W.polynomialY = (P y - (-P y - W.a₁ * P x - W.a₃ * P z)) * P z
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
⊢ a • 0 = 0

Tactic:
← zero_tmul _ (0 : Ω[A⁄R]),

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
⊢ a • 0 ⊗ₜ[R] 0 = 0 ⊗ₜ[R] 0
Module: Mathlib.RingTheory.Etale.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ etaleLocus R A ↔ Etale R (Localization.Away f)

Tactic:
basicOpen_subset_etaleLocus_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ FormallyEtale R (Localization.Away f) ↔ Etale R (Localization.Away f)
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case refine_1
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := mapPreimage hf b
n : ℕ
⊢ ↑(a (n + 1)) ≡ ↑(a n) [SMOD I ^ n • ⊤]

Tactic:
simp only [SModEq, mapPreimage, Submodule.Quotient.mk_sub,
      sub_eq_self, Submodule.Quotient.mk_eq_zero, SetLike.coe_mem, a]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
⊢ Submodule.Quotient.mk (if h : j = i then Eq.recOn h (↑x n) else 0) =
    ↑((component (AdicCompletion I R) ι (fun i ↦ AdicCompletion I (M i)) i)
          ((lof (AdicCompletion I R) ι (fun i ↦ AdicCompletion I (M i)) j) ((mk I (M j)) x)))
      n

Tactic:
DirectSum.component.of

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
⊢ Submodule.Quotient.mk (if h : j = i then Eq.recOn h (↑x n) else 0) =
    ↑(if h : j = i then Eq.recOn h ((mk I (M j)) x) else 0) n
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

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
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Tactic:
have hf : Function.Surjective f := by
    simp only [hfg, LinearMap.coe_comp, g]
    apply Function.Surjective.comp
    · exact AdicCompletion.map_surjective I hp
    · exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(ofTensorProduct I M)
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
⊢ Function.Bijective ⇑(ofTensorProduct I M)

Tactic:
by
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  exact ofTensorProduct_bijective_of_map_from_fin I M f hf

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

Goal state before:
pp: case e'_4
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
⊢ ⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘
      ⇑(Finsupp.lcomapDomain P.map ⋯) ∘ ⇑P.cotangentSpaceBasis.repr ∘ ⇑P.cotangentSpaceBasis ∘ P.map =
    ⇑(Pi.basisFun S σ)

Tactic:
classical
    ext i j
    simp only [Function.comp_apply, Basis.repr_self, Finsupp.linearEquivFunOnFinite_apply,
      Pi.basisFun_apply]
    simp [Finsupp.single_eq_pi_single]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : ↥D.presLeft.toExtension.ker
⊢ D.tensorCotangentHom (1 ⊗ₜ[D.T] Extension.Cotangent.mk x) = Extension.Cotangent.mk ⟨↑x, ⋯⟩

Tactic:
simp_rw +instances [tensorCotangentHom, LinearMap.liftBaseChange_tmul, one_smul, presLeft,
    Extension.Cotangent.map_mk, Extension.Hom.toAlgHom_apply, Hom.toExtensionHom_toRingHom,
    toAlgHom_fhom, AlgHom.toRingHom_eq_coe, AlgHom.id_toRingHom, toExtension_Ring,
    toExtension_commRing, toExtension_algebra₂, Presentation.naive_toGenerators, RingHom.id_apply]

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:
have : HasRingHomProperty @Smooth.{u} (Locally IsStandardSmooth) := by
    convert! (inferInstance : HasRingHomProperty (@Smooth.{u}) RingHom.Smooth)
    ext f
    rw [RingHom.smooth_iff_locally_isStandardSmooth]

Goal state after:
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ 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
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this : CompactSpace ↥X
⊢ UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))

Tactic:
← Scheme.toSpecΓ_naturality,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this : CompactSpace ↥X
⊢ UniversallyClosed (f ≫ Y.toSpecΓ)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝ :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this : ⟨x, hxU⟩ ∈ ⇑U.ι ⁻¹' closure ↑(smoothLocus f)
⊢ x ∈ closure ↑(smoothLocus f)

Tactic:
Set.mem_preimage,

Goal state after:
case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝ :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this : U.ι ⟨x, hxU⟩ ∈ closure ↑(smoothLocus f)
⊢ x ∈ closure ↑(smoothLocus f)
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
⊢ -(P y ^ 2 * Q z * W'.negY Q) - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q = P y ^ 2 * Q z * Q y

Tactic:
negY,

Goal state after:
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
⊢ -(P y ^ 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)) - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q =
    P y ^ 2 * Q z * Q y
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
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -(-(Q y ^ 2 * P z) * W'.negY P) - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q = -(Q y ^ 2 * P z) * P y

Tactic:
negY,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -(-(Q y ^ 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)) - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q =
    -(Q y ^ 2 * P z) * P y
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ P f

Tactic:
IsZariskiLocalAtSource.iff_of_openCover 𝒰 (P := P)

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addZ P Q] =
    ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addXYZ P Q y, (u * v) ^ 2 * W'.addXYZ P Q z]

Tactic:
addXYZ_Y,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addZ P Q] =
    ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addXYZ P Q z]
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
⊢ (Over.pullback f).Faithful

Tactic:
refine ⟨fun {X} Y a b hab ↦ ?_⟩

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
X Y : Over S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
⊢ a = b
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
⊢ @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat

Tactic:
rw [inf_comm]
    gcongr
    exact IsLocalIso.le_of_isZariskiLocalAtSource @Flat

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I
p : R[X]
hp : p.Monic
e : (aeval x) p = 0
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi✝ : i ≠ p.natDegree
hi : p.natDegree < i
⊢ p.coeff i ∈ I

Tactic:
· simp [coeff_eq_zero_of_natDegree_lt hi]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ eval f a (x + y) = eval f a x + eval f a y

Tactic:
unfold eval

Goal state after:
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ eval f a (x * y) = eval f a x * eval f a y

Tactic:
unfold eval

Goal state after:
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ (Ideal.span {X}).IsPrime

Tactic:
rw [Ideal.span_singleton_prime]

Goal state after:
K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ Prime X

K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ X ≠ 0
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
⊢ IsIntegral R (p.coeff i)

Tactic:
obtain rfl | hp0 := eq_or_ne p 0

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp : IsIntegral R[X] 0
⊢ IsIntegral R (coeff 0 i)

case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
⊢ IsIntegral R (p.coeff i)