mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
hσ' : σ ≠ 1
a✝ : K
⊢ (σ ^ 2) a✝ = 1 a✝

Tactic:
simpa using isConj_apply_apply hσ _

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
hσ' : σ ≠ 1
⊢ σ ^ 2 = 1

Tactic:
ext; simpa using isConj_apply_apply hσ _

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ ∀ (a : ℂ), (aeval a) p = 0 ↔ a ∈ b ∨ a ∈ c

Tactic:
hb,

Goal state after:
case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ ∀ (a : ℂ), (aeval a) p = 0 ↔ (aeval a) p = 0 ∧ a.im = 0 ∨ a ∈ c
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
z : ℂ
⊢ z ∈ b → z ∉ c

Tactic:
hb,

Goal state after:
case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
z : ℂ
⊢ (aeval z) p = 0 ∧ z.im = 0 → z ∉ c
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case e'_4
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ max ((fun x ↦ ‖x‖) x) ((fun x ↦ ‖x‖) y) = max (dist 0 x) (dist x (x + y))

Tactic:
congr <;> simp [SeminormedAddGroup.dist_eq]

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

Goal state before:
pp: case singleton
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
⊢ ∃ b ∈ {j}, ‖∏ i ∈ {j}, f i‖ ≤ ‖f b‖

Tactic:
simp only [Finset.mem_singleton, Finset.prod_singleton, exists_eq_left, le_refl]

Goal state after:
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
t : Finset ι
inst✝ : Nonempty ι
f : ι → M
ht : t.Nonempty
⊢ ∃ i, (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖

Tactic:
exact (fun ⟨i, h, h'⟩ => ⟨i, fun _ ↦ h, h'⟩) <| exists_norm_finsetProd_le_of_nonempty ht f

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
⊢ min φ.lexOrder ψ.lexOrder ≤ (φ + ψ).lexOrder

Tactic:
rw [le_lexOrder_iff]
  intro d hd
  simp only [lt_min_iff] at hd
  rw [map_add, coeff_eq_zero_of_lt_lexOrder hd.1, coeff_eq_zero_of_lt_lexOrder hd.2, add_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: K✝ : Type u_1
hK : NormedField K✝
inst✝² : IsUltrametricDist K✝
K : Type u_2
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : K
h : 1 < ‖x‖
⊢ valuation x ≠ 0 ∧ valuation x ≠ 1

Tactic:
by
    have h' : x ≠ 0 := norm_eq_zero.not.mp (h.gt.trans' (by simp)).ne'
    simp [valuation_apply, ← NNReal.coe_inj, h.ne', h']

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ ∑ p ∈ antidiagonal n, (coeff p.1) φ * (coeff p.2) (φ.invOfUnit u) = 0

Tactic:
← Finset.insert_erase this,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ ∑ p ∈ insert (0, n) ((antidiagonal n).erase (0, n)), (coeff p.1) φ * (coeff p.2) (φ.invOfUnit u) = 0
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
h : absNorm v.asIdeal ≤ 1
⊢ 0 < absNorm v.asIdeal

Tactic:
Nat.pos_iff_ne_zero,

Goal state after:
R : Type u_2
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
h : absNorm v.asIdeal ≤ 1
⊢ absNorm v.asIdeal ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
⊢ normUnit X = 1

Tactic:
simp [normUnit, ← Units.val_eq_one, Unit_of_divided_by_X_pow_order_nonzero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ (ofJ0 R).c₄ = 0

Tactic:
rw [ofJ0, c₄, b₂, b₄]
  norm_num1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ u • P ≈ v • Q ↔ P ≈ Q

Tactic:
← Quotient.eq_iff_equiv,

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ ⟦u • P⟧ = ⟦v • Q⟧ ↔ P ≈ Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ ⟦u • P⟧ = ⟦v • Q⟧ ↔ P ≈ Q

Tactic:
← Quotient.eq_iff_equiv,

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ ⟦u • P⟧ = ⟦v • Q⟧ ↔ ⟦P⟧ = ⟦Q⟧
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
W : C
f : W ⟶ Z
x✝ : (E.sieve₁ g₁ g₂).arrows f
T : E.I₁ i₁ i₂
u : W ⟶ E.Y T
h₁ : f ≫ g₁ = u ≫ E.p₁ T
h₂ : f ≫ g₂ = u ≫ E.p₂ T
⊢ (ConcreteCategory.hom (F.map (u ≫ E.p₁ T).op)) (x i₁) =
    (ConcreteCategory.hom (F.map f.op)) ((ConcreteCategory.hom (F.map g₂.op)) (x i₂))

Tactic:
conv_rhs => rw [← comp_apply, ← Functor.map_comp, ← op_comp, h₂]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
W : C
f : W ⟶ Z
x✝ : (E.sieve₁ g₁ g₂).arrows f
T : E.I₁ i₁ i₂
u : W ⟶ E.Y T
h₁ : f ≫ g₁ = u ≫ E.p₁ T
h₂ : f ≫ g₂ = u ≫ E.p₂ T
⊢ (ConcreteCategory.hom (F.map (u ≫ E.p₁ T).op)) (x i₁) = (ConcreteCategory.hom (F.map (u ≫ E.p₂ T).op)) (x i₂)
Module: Mathlib.RingTheory.Smooth.Local

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsLocalRing S
inst✝¹¹ : Algebra R S
P : Type u_3
K : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : Algebra S K
inst✝⁴ : Algebra P K
inst✝³ : IsScalarTower P S K
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
h₃ : maximalIdeal S ≤ RingHom.ker (algebraMap S K)
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
⊢ FormallySmooth R S ↔ Function.Injective ⇑(cotangentComplexBaseChange R S P K)

Tactic:
let := f.toAlgebra

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsLocalRing S
inst✝¹¹ : Algebra R S
P : Type u_3
K : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : Algebra S K
inst✝⁴ : Algebra P K
inst✝³ : IsScalarTower P S K
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
h₃ : maximalIdeal S ≤ RingHom.ker (algebraMap S K)
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this : Algebra (ResidueField S) K := f.toAlgebra
⊢ FormallySmooth R S ↔ Function.Injective ⇑(cotangentComplexBaseChange R S P K)
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra K A
⊢ Etale K A ↔ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)

Tactic:
constructor
  · intro H
    obtain ⟨I, _, Ai, _, _, e, _⟩ := (FormallyEtale.iff_exists_algEquiv_prod K A).mp inferInstance
    have := FormallyUnramified.finite_of_free K A
    exact ⟨_, ‹_›, _, _, _, e, fun i ↦ ⟨.of_surjective ((LinearMap.proj i).comp e.toLinearMap)
      ((Function.surjective_eval i).comp e.surjective), inferInstance⟩⟩
  · intro ⟨I, _, Ai, _, _, e, H⟩
    choose h₁ h₂ using H
    have := Module.Finite.of_surjective e.symm.toLinearMap e.symm.surjective
    refine ⟨?_, FinitePresentation.of_finiteType.mp inferInstance⟩
    exact (FormallyEtale.iff_exists_algEquiv_prod K A).mpr ⟨_, inferInstance, _, _, _, e, h₂⟩

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

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
inst✝ : Finite σ
P : PreSubmersivePresentation R S ι σ
x : ↥P.ker
⊢ P.cotangentComplexAux (Cotangent.mk x) = 0 ↔ ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0

Tactic:
funext_iff

Goal state after:
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 : PreSubmersivePresentation R S ι σ
x : ↥P.ker
⊢ (∀ (x_1 : σ), P.cotangentComplexAux (Cotangent.mk x) x_1 = 0 x_1) ↔
    ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addZ P P = 0

Tactic:
by
  rw [addZ]
  ring1

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

Goal state before:
pp: case inl
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
inst✝ : Nontrivial S
r : Unit
⊢ D.basis (Sum.inl r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl r), ⋯⟩

pp: case inr
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
inst✝ : Nontrivial S
r : σ
⊢ D.basis (Sum.inr r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
· rw [basis_inl, cotangentEquivProd_symm_apply]
    exact cotangentCompLocalizationAwayEquiv_symm_inr _ _ _

Goal state after:
case inr
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
inst✝ : Nontrivial S
r : σ
⊢ D.basis (Sum.inr r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
w✝² w✝¹ : Type
w✝ : _root_.Finite w✝¹
left✝ : _root_.Finite w✝²
P : Algebra.SubmersivePresentation R S w✝² w✝¹
⊢ ∃ n g, g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
let := f.toAlgebra

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
w✝² w✝¹ : Type
w✝ : _root_.Finite w✝¹
left✝ : _root_.Finite w✝²
P : Algebra.SubmersivePresentation R S w✝² w✝¹
this : Algebra R S := f.toAlgebra
⊢ ∃ n g, g.comp MvPolynomial.C = f ∧ g.Etale
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: n m : ℕ
X Y : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : Smooth f
⊢ Smooth (Scheme.Hom.resLE f V U e)

Tactic:
by
  delta Scheme.Hom.resLE; infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal ↑Γ(Y, U) := (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)

Tactic:
let q := (hV.primeIdealOf ⟨x, hx⟩).asIdeal

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal ↑Γ(Y, U) := (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
q : Ideal ↑Γ(X, V) := (hV.primeIdealOf ⟨x, hx⟩).asIdeal
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth

Tactic:
· have := hV.isLocalization_basicOpen r
    rw [← RingHom.smooth_algebraMap] at hr
    convert!
      RingHom.Smooth.propertyIsLocal.respectsIso.1 _
        (IsLocalization.algEquiv (.powers r) _ Γ(X, X.basicOpen r)).toRingEquiv hr
    ext
    dsimp
    simp only [IsScalarTower.algebraMap_apply Γ(Y, U) Γ(X, V) (Localization _),
      IsLocalization.map_eq]
    simp only [algebraMap_toAlgebra, RingHomCompTriple.comp_apply, ← ConcreteCategory.comp_apply,
      Scheme.Hom.appLE_map]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
H✝ : smoothLocus f = ⊤
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V
H : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
⊢ ∃ U V, ∃ (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), Smooth (resLE f U V e)

Tactic:
refine ⟨U, V, hxV, hVU, ?_⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
H✝ : smoothLocus f = ⊤
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V
H : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
⊢ Smooth (resLE f U V hVU)
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X Y : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : Etale f
⊢ Etale (Scheme.Hom.resLE f V U e)

Tactic:
by
  delta Scheme.Hom.resLE; infer_instance

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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addY P Q * (P z * Q z) ^ 3 = -(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2

Tactic:
by
  linear_combination (norm := (rw [addY, negY_eq, addX_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx]; ring1)) -(P z * Q z) * negAddY_of_X_eq' hP hQ hx

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P Q : Fin 3 → R
⊢ (W'.map f).negAddY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.negAddY P Q)

Tactic:
by
  simp only [negAddY]
  map_simp

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i✝ : ℕ
hi✝ : i✝ ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
hi : i < p.natDegree
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (X ^ p.natDegree).coeff i

pp: case inr.inl
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
⊢ (map (Ideal.Quotient.mk P) p).coeff p.natDegree = (X ^ p.natDegree).coeff p.natDegree

pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i✝ : ℕ
hi✝ : i✝ ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
hi : p.natDegree < i
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (X ^ p.natDegree).coeff i

Tactic:
· simpa [hi.ne, Ideal.Quotient.eq_zero_iff_mem] using hPJ (Ideal.subset_span ⟨_, hi, rfl⟩)

Goal state after:
case inr.inl
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
⊢ (map (Ideal.Quotient.mk P) p).coeff p.natDegree = (X ^ p.natDegree).coeff p.natDegree

case inr.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i✝ : ℕ
hi✝ : i✝ ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
hi : p.natDegree < i
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (X ^ p.natDegree).coeff i
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
c : K
⊢ eval f a (C c) = f c

Tactic:
simp [eval]

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
⊢ eval f a X = a

Tactic:
simp [eval]

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
⊢ eval f a 0 = 0

Tactic:
simp [eval]

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
⊢ eval f a 1 = 1

Tactic:
simp [eval]

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
algInst✝ : Algebra R[X] S := f.toAlgebra
e : Ideal.map C (Ideal.under R P) = Ideal.comap (↑f) P
this✝ : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this : Algebra (Localization.AtPrime (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
⊢ False

Tactic:
let := Localization.AtPrime.algebraOfLiesOver (P.under R) P

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
algInst✝ : Algebra R[X] S := f.toAlgebra
e : Ideal.map C (Ideal.under R P) = Ideal.comap (↑f) P
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this✝ : Algebra (Localization.AtPrime (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : LocallyQuasiFinite f
⊢ LocallyQuasiFinite (Hom.resLE f V U e)

Tactic:
by
  delta Scheme.Hom.resLE; infer_instance

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

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
P : Presieve U
⊢ U.presieveOfSections (sectionsOfPresieve P) = P

Tactic:
by
  refine funext₂ fun ⟨V, hV⟩ ⟨f, hf⟩ ↦ eq_iff_iff.mpr ⟨?_, ?_⟩
  · rintro ⟨_, H, rfl⟩
    exact H
  · intro H
    obtain rfl : _ = V := hf
    exact ⟨_, H, rfl⟩

Goal state after: