mathlib-initiative/mathlib-tactics huggingface dataset:
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' : ∀ (x : K), v x ≠ 0 → v x = 1
x : (ofClass v).ValueGroup₀ˣ
hx : x ≠ 1
k : K
hk : (restrict₀ (ofClass v)) k = ↑x
⊢ False

Tactic:
have h0 : v k ≠ 0 := by
      apply_fun embedding at hk
      simp only [embedding_restrict₀, MonoidWithZeroHom.coe_ofClass] at hk
      simp [hk]

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
k : K
hk : (restrict₀ (ofClass v)) k = ↑x
h0 : v k ≠ 0
⊢ False
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) (x + y) ≤ max ((fun x ↦ ‖x‖) x) ((fun x ↦ ‖x‖) y)

Tactic:
convert! dist_triangle_max 0 x (x + y) using 1

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

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))
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
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
h✝ : Nonempty ι
⊢ ‖∏' (i : ι), f i‖ ≤ C

Tactic:
· exact norm_tprod_le_of_forall_le h

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
⊢ φ.lexOrder ≤ ↑(toLex u) → ¬ψ.lexOrder ≤ ↑(toLex v)

Tactic:
intro hu hv

Goal state after:
σ : 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 : φ.lexOrder ≤ ↑(toLex u)
hv : ψ.lexOrder ≤ ↑(toLex v)
⊢ False
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 : ¬φ.lexOrder + ψ.lexOrder ≤ ↑(toLex d)
u v : σ →₀ ℕ
h : u + v = d
hu : φ.lexOrder ≤ ↑(toLex u)
hv : ψ.lexOrder ≤ ↑(toLex v)
⊢ False

Tactic:
apply hd

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ¬φ.lexOrder + ψ.lexOrder ≤ ↑(toLex d)
u v : σ →₀ ℕ
h : u + v = d
hu : φ.lexOrder ≤ ↑(toLex u)
hv : ψ.lexOrder ≤ ↑(toLex v)
⊢ φ.lexOrder + ψ.lexOrder ≤ ↑(toLex d)
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case inr.inr
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
rcases exists_finsupp_eq_lexOrder_of_ne_zero hψ with ⟨q, hq⟩

Goal state after:
case inr.inr
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).IsElliptic

Tactic:
have := Fact.mk (Ne.isUnit h3)

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ j).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
⊢ (ofJ j).j = j

Tactic:
have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩
      simp_rw [h0, ofJ_0_of_three_eq_zero h3, ofJ1728_j]
      linear_combination 576 * h3

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

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).j = j

Tactic:
have := Fact.mk (Ne.isUnit h3)

Goal state after:
case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ j).j = j
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 (f ≫ g₂).op)) (x i₂)

Tactic:
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₂)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) W'.polynomialX = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2)

Tactic:
rw [polynomialX_eq]
  simp

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : Q z = 0
⊢ W.Nonsingular (W.add P Q)

pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
⊢ W.Nonsingular (W.add P Q)

Tactic:
· simpa only [add_of_Z_eq_zero_right hQ.left hPz hQz,
        nonsingular_smul _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg]

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
⊢ W.Nonsingular (W.add P Q)
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
f : R →+* S
hf : Function.Injective ⇑f
P : Fin 3 → R
⊢ (W'.map f).Equation (⇑f ∘ P) ↔ W'.Equation P

Tactic:
simp only [Equation, map_polynomial, eval_map, ← eval₂_comp, map_eq_zero_iff f hf]

Goal state after:
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
f : R →+* S
⊢ (W'.map f).polynomialX = (MvPolynomial.map f) W'.polynomialX

Tactic:
simp only [polynomialX, map_polynomial, pderiv_map]

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

Goal state before:
pp: case refine_2
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ ⨅ j,
      TopologicalSpace.induced (⇑(ConcreteCategory.hom ((uliftFunctor.mapCone c).π.app j)))
        ((K ⋙ uliftFunctor).obj j).str ≤
    TopologicalSpace.induced ULift.down c.pt.str

Tactic:
rw [← generateFrom_iUnion_isOpen, induced_of_isLimit _ hc, induced_iInf, le_iInf_iff]

Goal state after:
case refine_2
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ ∀ (i : J✝),
    TopologicalSpace.generateFrom (⋃ i, {s | IsOpen s}) ≤
      TopologicalSpace.induced ULift.down (TopologicalSpace.induced (⇑(ConcreteCategory.hom (c.π.app i))) (K.obj i).str)
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_3
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
f : (fun X ↦ X) ((yoneda.obj X).obj (Opposite.op Y))
hf : (fun t ↦ ∀ (i : 𝒰.I₀), (ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op)) t = x i) f
i : 𝒰.I₀
y : ↑(𝒰.X i)
⊢ (ConcreteCategory.hom f) ((ConcreteCategory.hom (𝒰.f i)) y) =
    (ConcreteCategory.hom
        (ofHom
          (ContinuousMap.liftCover (fun i ↦ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
            (fun i ↦ { toFun := ⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ }) ⋯ ⋯)))
      ((ConcreteCategory.hom (𝒰.f i)) y)

Tactic:
have := congr($(hf i).hom y)

Goal state after:
case refine_3
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
f : (fun X ↦ X) ((yoneda.obj X).obj (Opposite.op Y))
hf : (fun t ↦ ∀ (i : 𝒰.I₀), (ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op)) t = x i) f
i : 𝒰.I₀
y : ↑(𝒰.X i)
this : (Hom.hom ((ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op)) f)) y = (Hom.hom (x i)) y
⊢ (ConcreteCategory.hom f) ((ConcreteCategory.hom (𝒰.f i)) y) =
    (ConcreteCategory.hom
        (ofHom
          (ContinuousMap.liftCover (fun i ↦ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
            (fun i ↦ { toFun := ⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ }) ⋯ ⋯)))
      ((ConcreteCategory.hom (𝒰.f i)) y)
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_1
X : TopCat
E : precoverage.ZeroHypercover X
i : E.I₀
y : ↑(E.X i)
⊢ ∃ i_1 y_1, (ConcreteCategory.hom (uliftFunctor.map (E.f i_1))) y_1 = { down := (ConcreteCategory.hom (E.f i)) y }

Tactic:
use i, ⟨y⟩

Goal state after:
case h
X : TopCat
E : precoverage.ZeroHypercover X
i : E.I₀
y : ↑(E.X i)
⊢ (ConcreteCategory.hom (uliftFunctor.map (E.f i))) { down := y } = { down := (ConcreteCategory.hom (E.f i)) y }
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
h : Algebra.IsPushout R S A B
b : B
x : S ⊗[R] Ω[A⁄R]
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) (b • x) = b • (LinearMap.liftBaseChange S (↑R (map R S A B))) x

Tactic:
by
  induction b using h.1.inductionOn with
  | zero => simp only [zero_smul, map_zero]
  | smul s b e => rw [smul_assoc, map_smul, e, smul_assoc]
  | add b₁ b₂ e₁ e₂ => simp only [map_add, e₁, e₂, add_smul]
  | tmul a =>
    induction x
    · simp only [smul_zero, map_zero]
    · simp [smul_comm]
    · simp only [map_add, smul_add, *]

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

Goal state before:
pp: 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
⊢ ∃ a, (map I f) a = y

Tactic:
apply AdicCompletion.induction_on I N y (fun b ↦ ?_)

Goal state after:
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, (map I f) a = (mk I N) b
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n : ℕ
x : R
⊢ (evalₐ I n) ((liftRingHom I f ⋯) x) = (f n) x

Tactic:
by
  rw [← factor_eval_eq_evalₐ I _ (le_of_eq (Ideal.mul_top _))]
  simp [liftRingHom, eval]

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

Goal state before:
pp: case 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
y : AdicCompletion I N
⊢ y ∈ (map I g).ker → y ∈ (map I f).range

Tactic:
apply AdicCompletion.induction_on I N y (fun b ↦ ?_)

Goal state after:
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
y : AdicCompletion I N
b : AdicCauchySequence I N
⊢ (mk I N) b ∈ (map I g).ker → (mk I N) b ∈ (map I f).range
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
inst✝¹ : Finite σ
r : R
inst✝ : IsLocalization.Away r S
⊢ IsUnit (PreSubmersivePresentation.localizationAway S r).jacobian

Tactic:
rw [localizationAway_jacobian]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Finite σ
r : R
inst✝ : IsLocalization.Away r S
⊢ IsUnit ((algebraMap R S) r)
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: case hab
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)
⊢ Codisjoint (Set.range f) (Set.range P.map)

Tactic:
· exact hcompl.2

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Tactic:
algebraize [((Generators.localizationAway T g).toComp P).toAlgHom.toRingHom]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
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
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.Smooth R S
s : Set S
hs : Ideal.span s = ⊤
h : ∀ x ∈ s, Algebra.IsStandardSmooth R (Localization.Away x)
t : S
ht : t ∈ s
⊢ (algebraMap R (Localization.Away t)).IsStandardSmooth

Tactic:
isStandardSmooth_algebraMap

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Smooth
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.Smooth R S
s : Set S
hs : Ideal.span s = ⊤
h : ∀ x ∈ s, Algebra.IsStandardSmooth R (Localization.Away x)
t : S
ht : t ∈ s
⊢ Algebra.IsStandardSmooth R (Localization.Away t)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case refine_1
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 : (Scheme.Opens.toSpecΓ V ≫ IsAffineOpen.fromSpec hV) ⟨x, hxV⟩ ∈ X.basicOpen r
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ x ∈ X.basicOpen r

Tactic:
IsAffineOpen.toSpecΓ_fromSpec

Goal state after:
case refine_1
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 : (Scheme.Opens.ι V) ⟨x, hxV⟩ ∈ X.basicOpen r
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ x ∈ X.basicOpen r
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι✝ : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι✝ → K
F : MvPolynomial ι✝ k
HF : ∀ (F' : MvPolynomial ι✝ k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι✝), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι✝ →₀ ℕ) → ι✝ →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
ι : Type u_3
x✝ : Fintype ι
v : ι → K
hv : LinearIndependent k v
⊢ LinearIndepOn k id ↑(Finset.image v Finset.univ)

Tactic:
by simpa using! hv.linearIndepOn_id

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

Goal state before:
pp: P : MorphismProperty Scheme
X Y : Scheme
inst✝ : P.RespectsIso
f : X ⟶ Y
⊢ sourceLocalClosure IsOpenImmersion P f ↔ ∀ (x : ↥X), ∃ U, x ∈ U ∧ P (U.ι ≫ f)

Tactic:
by
  refine ⟨fun ⟨𝒰, hf⟩ x ↦ ?_, fun H ↦ ?_⟩
  · refine ⟨(𝒰.f (𝒰.idx x)).opensRange, 𝒰.covers x, ?_⟩
    rw [← Scheme.Hom.isoOpensRange_inv_comp, Category.assoc, P.cancel_left_of_respectsIso]
    apply hf
  · choose U hx hf using H
    exact ⟨.mkOfCovers X (fun x ↦ U x) (fun _ ↦ (U _).ι) (fun x ↦ ⟨x, ⟨x, hx x⟩, rfl⟩)
      fun _ ↦ inferInstance, hf⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified

Tactic:
algebraize [φ.hom]

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

Goal state before:
pp: case refine_1
W P Q : MorphismProperty Scheme
X Y : Scheme
inst✝³ : W.IsStableUnderBaseChange
inst✝² : Scheme.IsJointlySurjectivePreserving W
inst✝¹ : P.RespectsIso
inst✝ : P.RespectsLeft IsOpenImmersion
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X✝
x✝ : sourceLocalClosure IsOpenImmersion P f
𝒱 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X✝
h : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ f)
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f i) 𝒱).I₀
⊢ P ((Precoverage.ZeroHypercover.pullback₁ (𝒰.f i) 𝒱).f j ≫ 𝒰.f i ≫ f)

Tactic:
simpa [pullback.condition_assoc] using
      RespectsLeft.precomp (Q := @IsOpenImmersion) _ inferInstance _ (h j)

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

Goal state before:
pp: case refine_1
⊢ ∀ (i : MorphismProperty Scheme), i.ContainsIdentities → IsZariskiLocalAtSource i → @IsLocalIso ≤ i

Tactic:
apply le_of_isZariskiLocalAtSource

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
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this : IsLocalHom (algebraMap ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x))
⊢ Algebra.IsSeparable (IsLocalRing.ResidueField ↑(Y.presheaf.stalk (f x)))
    (IsLocalRing.ResidueField ↑(X.presheaf.stalk x))

Tactic:
have : Algebra.EssFiniteType (Y.presheaf.stalk (f x)) (X.presheaf.stalk x) := by
    rw [← RingHom.essFiniteType_algebraMap, RingHom.algebraMap_toAlgebra]
    exact LocallyOfFiniteType.stalkMap f x

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
this✝ : IsLocalHom (algebraMap ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x))
this : Algebra.EssFiniteType ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x)
⊢ Algebra.IsSeparable (IsLocalRing.ResidueField ↑(Y.presheaf.stalk (f x)))
    (IsLocalRing.ResidueField ↑(X.presheaf.stalk x))
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
inst✝¹ : ExpChar k p
inst✝ : Algebra.EssFiniteType k K
⊢ ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(adjoin k ↑s)) K

Tactic:
have ⟨s, hs, Hs⟩ := exists_finset_maximalFor_isTranscendenceBasis_separableClosure k K
  refine ⟨s, hs, ⟨fun n ↦ of_not_not fun hn ↦ ?_⟩⟩
  have hns : n ∉ s := fun h ↦ hn (le_restrictScalars_separableClosure _ (subset_adjoin _ _ h))
  have ⟨i, hi₁, hi₂⟩ := exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow'
    p hp (a := id) H s n hs hns
  rw [Set.image_id] at hi₂
  refine not_lt_iff_le_imp_ge.mpr (Hs hi₁) (SetLike.lt_iff_le_and_exists.mpr ⟨?_, n, ?_, hn⟩)
  · rw [separableClosure_le_separableClosure_iff, adjoin_le_iff]
    intro x hx
    obtain rfl | ne := eq_or_ne x i
    exacts [hi₂, le_restrictScalars_separableClosure _ (subset_adjoin _ _ ⟨.inr hx, ne⟩)]
  · obtain rfl | ne := eq_or_ne n i
    exacts [hi₂, le_restrictScalars_separableClosure _ (subset_adjoin _ _ ⟨.inl rfl, ne⟩)]

Goal state after: