mathlib-initiative/mathlib-tactics huggingface dataset:
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.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
R : Presieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
H' :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows

Tactic:
exact h₁.isSheafFor_sieve_of_pullback h₂ H H'

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ {u : R}, IsUnit u → ∀ {P : Fin 3 → R}, W'.Nonsingular (u • P) → W'.Nonsingular P
h : W'.Nonsingular P
⊢ W'.Nonsingular (↑hu.unit⁻¹ • u • P)

Tactic:
by rwa [smul_smul, hu.val_inv_mul, one_smul]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝² : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).HasPairwisePullbacks
inst✝ : PreservesLimit (Discrete.functor fun x ↦ op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : (fun X ↦ X) (∏ᶜ fun b ↦ F.obj (op (X b)))),
    ∃! a,
      (ConcreteCategory.hom
            (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
              Equalizer.Presieve.Arrows.forkMap F X c.inj))
          a =
        b
⊢ ∀ (y : Equalizer.Presieve.Arrows.FirstObj F X),
    (ConcreteCategory.hom (Equalizer.Presieve.Arrows.firstMap F X c.inj)) y =
        (ConcreteCategory.hom (Equalizer.Presieve.Arrows.secondMap F X c.inj)) y →
      ∃! x, (ConcreteCategory.hom (Equalizer.Presieve.Arrows.forkMap F X c.inj)) x = y

Tactic:
intro b _

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝² : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).HasPairwisePullbacks
inst✝ : PreservesLimit (Discrete.functor fun x ↦ op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : (fun X ↦ X) (∏ᶜ fun b ↦ F.obj (op (X b)))),
    ∃! a,
      (ConcreteCategory.hom
            (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
              Equalizer.Presieve.Arrows.forkMap F X c.inj))
          a =
        b
b : Equalizer.Presieve.Arrows.FirstObj F X
a✝ :
  (ConcreteCategory.hom (Equalizer.Presieve.Arrows.firstMap F X c.inj)) b =
    (ConcreteCategory.hom (Equalizer.Presieve.Arrows.secondMap F X c.inj)) b
⊢ ∃! x, (ConcreteCategory.hom (Equalizer.Presieve.Arrows.forkMap F X c.inj)) x = b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular (⇑↑f ∘ P) ↔ (W'⁄A).Nonsingular P

Tactic:
← map_nonsingular _ hf,

Goal state after:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular (⇑↑f ∘ P) ↔ ((W'⁄A).map f.toRingHom).Nonsingular (⇑f.toRingHom ∘ P)
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case h₂
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ IsOpenImmersion.precoverage ≤ Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage

Tactic:
rw [MorphismProperty.comap_precoverage]
    exact MorphismProperty.precoverage_monotone fun X Y f hf ↦ f.isOpenEmbedding

Goal state after:
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: ⊢ grothendieckTopology.Subcanonical

Tactic:
refine .of_isSheaf_yoneda_obj _ fun X ↦ ?_
  rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small]
  intro Y 𝒰
  rw [Presieve.isSheafFor_arrows_iff]
  have heq (i y) : 𝒰.f i y = (Subtype.val : Set.range (𝒰.f i) → Y) ⟨𝒰.f i y, by simp⟩ := rfl
  refine fun x hx ↦ ⟨?_, fun i ↦ ?_, fun f hf ↦ ?_⟩
  · refine ofHom <| ContinuousMap.liftCover (fun i ↦ Set.range (𝒰.f i)) ?_ ?_ ?_
    · intro i
      exact ⟨(x i).hom ∘ (isOpenEmbedding_f_zeroHypercover 𝒰 i).toHomeomorph.symm, by fun_prop⟩
    · intro i j y
      simp only [Set.mem_range, ContinuousMap.coe_mk, Function.comp_apply, forall_exists_index]
      intro xi hi xj hj
      conv_lhs => simp only [← hi]
      conv_rhs => simp only [← hj]
      have := hx i j _ (TopCat.pullbackCone (𝒰.f i) (𝒰.f j)).fst
        (TopCat.pullbackCone (𝒰.f i) (𝒰.f j)).snd (TopCat.pullbackCone (𝒰.f i) (𝒰.f j)).condition
      dsimp at this
      simpa using! congr($(this) ⟨(xi, xj), hi ▸ hj.symm⟩)
    · intro x
      obtain ⟨i, hi⟩ := exists_mem_zeroHypercover_range 𝒰 x
      exact ⟨i, (isOpenEmbedding_f_zeroHypercover 𝒰 i).isOpen_range.mem_nhds hi⟩
  · apply ConcreteCategory.hom_ext
    intro
    simp only [yoneda_obj_map, Quiver.Hom.unop_op, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
      hom_comp, ContinuousMap.comp_apply]
    rw [heq, ContinuousMap.liftCover_coe]
    simp
  · dsimp
    ext x
    obtain ⟨i, y, rfl⟩ := exists_mem_zeroHypercover_range 𝒰 x
    have := congr($(hf i).hom y)
    dsimp at this ⊢
    rw [this, heq, ContinuousMap.liftCover_coe]
    simp

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
x : S ⊗[R] Ω[A⁄R]
⊢ 0 • x = 0

Tactic:
induction x <;> simp [*]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
A : Type u
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K L
inst✝³ : Algebra K A
inst✝² : EssFiniteType K A
inst✝¹ : FormallyEtale K A
p : Ideal A
inst✝ : p.IsPrime
⊢ Algebra.IsSeparable K (A ⧸ p)

Tactic:
have := Algebra.FormallyUnramified.finite_of_free K A
  have : IsArtinianRing A := isArtinian_of_tower K inferInstance
  have := Algebra.FormallyUnramified.isReduced_of_field K A
  let := Ideal.Quotient.field p
  rw [← Algebra.FormallyEtale.iff_isSeparable]
  have : Algebra.FormallyEtale K (Π (m : MaximalSpectrum A), (A ⧸ m.asIdeal)) :=
    .of_equiv ((IsArtinianRing.equivPi _).restrictScalars K)
  rw [Algebra.FormallyEtale.pi_iff] at this
  exact this ⟨p, inferInstance⟩

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

Goal state before:
pp: case tmul.tmul
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
h : Algebra.IsPushout R S A B
x : B
m✝ : A
⊢ x •
      (LinearMap.liftBaseChange S (↑R (map R S A B)))
        ((derivationTensorProduct R S A B) ((IsScalarTower.toAlgHom R A B).toLinearMap m✝)) =
    x • (D S B) ((IsScalarTower.toAlgHom R A B).toLinearMap m✝)

Tactic:
simp only [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom',
          derivationTensorProduct_algebraMap, LinearMap.liftBaseChange_tmul,
          LinearMap.coe_restrictScalars, map_D, one_smul]

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
inst✝ : Algebra.IsPushout R S A B
a : A
this : Algebra.IsPushout R A S B
a' : A
s : S
⊢ s • a' • (D S B) ((algebraMap A B) a) = (Algebra.IsPushout.equiv R A S B) (a' ⊗ₜ[R] s) • (D S B) ((algebraMap A B) a)

Tactic:
simp [Algebra.IsPushout.equiv_tmul, mul_smul, smul_comm]

Goal state after:
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
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : N
n : ℕ
hy : y ∈ I ^ n • ⊤
⊢ ∃ x ∈ I ^ n • ⊤, f x ≡ y [SMOD I ^ (n + 1) • ⊤]

Tactic:
by
  induction hy using smul_induction_on' with
  | smul r hr y _ =>
    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
  | add y1 hy1 y2 hy2 ih1 ih2 =>
    obtain ⟨x1, hx1, hx1'⟩ := ih1
    obtain ⟨x2, hx2, hx2'⟩ := ih2
    use x1 + x2, add_mem hx1 hx2
    simp only [map_add]
    exact SModEq.add hx1' hx2'

Goal state after:
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
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
y : N
n : ℕ
hxy : f x ≡ y [SMOD I ^ n • ⊤]
⊢ ∃ x', x ≡ x' [SMOD I ^ n • ⊤] ∧ f x' ≡ y [SMOD I ^ (n + 1) • ⊤]

Tactic:
obtain ⟨z, hz, hz'⟩ :=
    exists_smodEq_pow_add_one_smul h (y := y - f x) (SModEq.sub_mem.mp hxy.symm)

Goal state after:
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)
x : M
y : N
n : ℕ
hxy : f x ≡ y [SMOD I ^ n • ⊤]
z : M
hz : z ∈ I ^ n • ⊤
hz' : f z ≡ y - f x [SMOD I ^ (n + 1) • ⊤]
⊢ ∃ x', x ≡ x' [SMOD I ^ n • ⊤] ∧ f x' ≡ y [SMOD I ^ (n + 1) • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : R ⧸ I • ⊤
x : M ⧸ I • ⊤
⊢ (r • s) • x = r • s • x

Tactic:
by
    induction s, x using Quotient.inductionOn₂' with | _ s x
    simp only [Submodule.Quotient.mk''_eq_mk]
    rw [← Submodule.Quotient.mk_smul, Ideal.Quotient.mk_eq_mk, mk_smul_mk, smul_assoc]
    rfl

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
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
hli : LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))
hsp : Submodule.span S (Set.range fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) = ⊤
⊢ IsUnit P.jacobian

Tactic:
rw [isUnit_jacobian_iff_aevalDifferential_bijective]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
hli : LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))
hsp : Submodule.span S (Set.range fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) = ⊤
⊢ Function.Bijective ⇑P.aevalDifferential
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
inst✝¹ : FormallySmooth R A
I : Ideal S
inst✝ : IsAdicComplete I S
f : A →ₐ[R] S ⧸ I
⊢ ∃ g, (Ideal.Quotient.mkₐ R I).comp g = f

Tactic:
by
  obtain ⟨g, hg⟩ := exists_adicCompletionEvalOneₐ_comp_eq f
  refine ⟨AlgHom.comp ((AdicCompletion.ofAlgEquiv I).symm.toAlgHom.restrictScalars R) g, ?_⟩
  ext x
  simpa using congr($hg x)

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).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁ i j =
    (algebraMap Q.Ring T).mapMatrix Q.jacobiMatrix i j

Tactic:
simp only [Matrix.map_apply, RingHom.mapMatrix_apply, ← Q.jacobiMatrix_comp_inl_inl P,
    Q.algebraMap_apply]

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).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁ i j =
    (aeval Q.val) ((aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P).jacobiMatrix (Sum.inl i) (Sum.inl j)))
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
⊢ Function.Surjective ⇑(p.projectionOnto q hpq ∘ₗ f)

Tactic:
rw [← Set.surjOn_univ, LinearMap.coe_comp, Set.surjOn_comp_iff, Set.image_univ]

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
⊢ Set.SurjOn (⇑(p.projectionOnto q hpq)) (Set.range ⇑f) Set.univ
Module: Mathlib.RingTheory.Smooth.Flat

Goal state before:
pp: R : Type u_1
A : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective ⇑f
inst✝² : Module.Flat R S
inst✝¹ : IsNoetherianRing S
inst✝ : FormallySmooth R A
⊢ Module.Flat R A

Tactic:
by
  have : Module.Flat R (AdicCompletion (RingHom.ker f) S) := .trans _ S _
  obtain ⟨g, hg⟩ := exists_kerProj_comp_eq_id f hf
  exact .of_retract g.toLinearMap
    (AdicCompletion.kerProj hf).toLinearMap (LinearMap.ext fun x ↦ congr($hg x))

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra A B
D : DescentAux A B
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
⊢ (subalgebra R D).FG

Tactic:
refine Subalgebra.fg_def.mpr ⟨_, ?_, rfl⟩

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra A B
D : DescentAux A B
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
⊢ (D.P.coeffs ∪
      (((⋃ i, ↑(D.h i).coeffs) ∪ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x)) ∪ ⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs)).Finite
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
⊢ D.P.coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
    without the `rw`. It is not yet clear whether this is due to defeq abuse in Mathlib or a
    problem in the new canonicalizer; a minimization would help. The original proof was:
    `grind [subalgebra, Subalgebra.setRange_algebraMap, Algebra.subset_adjoin]` -/

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
⊢ D.P.coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

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✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ ⊤ ≤ Submodule.comap (Submodule.subtype P.ker) (Ideal.span (Set.range (Subtype.val ∘ v))) ⊔ P.ker • ⊤

Tactic:
rw [← Submodule.coe_subtype, Ideal.span, Set.range_comp, ← Submodule.map_span,
    Submodule.comap_map_eq_of_injective P.ker.subtype_injective,
    ← Extension.Cotangent.ker_mk]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ ⊤ ≤ Submodule.span P.Ring (Set.range v) ⊔ Extension.Cotangent.mk.ker
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Smooth
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f

Tactic:
algebraize [f]
  obtain ⟨s, hs, h⟩ := Algebra.Smooth.exists_span_eq_top_isStandardSmooth R S
  refine ⟨s, hs, fun t ht ↦ ?_⟩
  dsimp only
  rw [← f.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_eq, isStandardSmooth_algebraMap]
  exact h t ht

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

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝² : Field L
inst✝¹ : Field K
inst✝ : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
this✝ : FormallySmooth K ↥(adjoin K (Set.range v))
this : FormallySmooth ↥(adjoin K (Set.range v)) ↥(IntermediateField.adjoin K (Set.range v))
⊢ FormallySmooth K ↥(IntermediateField.adjoin K (Set.range v))

Tactic:
exact .comp _ (adjoin K (Set.range v)) _

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
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Subsingleton S
⊢ Ideal.span (Set.range fun x ↦ 1) = (ofSurjective (fun i ↦ 0) ⋯).ker

Tactic:
simpa using! (RingHom.ker_eq_top_of_subsingleton _).symm

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ HasOfPostcompProperty (@Etale) (@LocallyOfFiniteType ⊓ @FormallyUnramified)

Tactic:
MorphismProperty.hasOfPostcompProperty_iff_le_diagonal

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFiniteType ⊓ @FormallyUnramified ≤ diagonal @Etale
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : P'.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), P' f → P (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
h : P' f
hf : P (pullback.fst f g)
hZ : ∃ R, Z = Spec R
⊢ P g

Tactic:
obtain ⟨R, rfl⟩ := hZ

Goal state after:
P P' : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : P'.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), P' f → P (pullback.fst f g) → P g
X Y : Scheme
R : CommRingCat
f : X ⟶ Spec R
g : Y ⟶ Spec R
inst✝ : HasPullback f g
h : P' f
hf : P (pullback.fst f g)
⊢ P g
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental S x
⊢ IsStronglyTranscendental R x

Tactic:
by
  intro t p hp
  simpa [map_map, ← IsScalarTower.algebraMap_eq] using h t (p.map (algebraMap R S)) (by simpa)

Goal state after:
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
i : ℕ
hi : i < p.natDegree
⊢ v ((algebraMap A B) (p.coeff i)) * v w ^ i < v ((algebraMap A B) p.leadingCoeff) * v w ^ p.natDegree

Tactic:
by_cases h0 : (p.coeff i) = 0

Goal state after:
case pos
Γ : 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
i : ℕ
hi : i < p.natDegree
h0 : p.coeff i = 0
⊢ v ((algebraMap A B) (p.coeff i)) * v w ^ i < v ((algebraMap A B) p.leadingCoeff) * v w ^ p.natDegree

case neg
Γ : 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
i : ℕ
hi : i < p.natDegree
h0 : ¬p.coeff i = 0
⊢ v ((algebraMap A B) (p.coeff i)) * v w ^ i < v ((algebraMap A B) p.leadingCoeff) * v w ^ p.natDegree
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
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
⊢ Function.Injective ⇑f

Tactic:
refine RingHom.lift_injective_of_ker_le_ideal _ _ fun u hu => ?_
    rwa [RingHom.mem_ker, RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap,
      comap_map_eq_map_adjoin_of_coprime_conductor hx h_alg] at hu

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
⊢ ∃ p ∈ I, Ideal.span {map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I

Tactic:
obtain ⟨p, hp : _ = Ideal.span _⟩ := (inferInstance :
    (I.map (mapRingHom (algebraMap R P.ResidueField))).IsPrincipal)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
⊢ ∃ p ∈ I, Ideal.span {map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I