mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
⊢ ∀ (x y : { ε // ε > 0 }),
    ∃ z,
      𝓟 {p | v.norm (p.1 - p.2) < ↑x} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑z} ∧
        𝓟 {p | v.norm (p.1 - p.2) < ↑y} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑z}

Tactic:
intro x y

Goal state after:
case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x y : { ε // ε > 0 }
⊢ ∃ z,
    𝓟 {p | v.norm (p.1 - p.2) < ↑x} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑z} ∧
      𝓟 {p | v.norm (p.1 - p.2) < ↑y} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑z}
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: R : Type u_1
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Invertible (constantCoeff f.divXPowOrder)

Tactic:
apply invertibleOfNonzero

Goal state after:
R : Type u_1
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ constantCoeff f.divXPowOrder ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
⊢ P ≈ Q

Tactic:
use Units.mk0 _ hPz / Units.mk0 _ hQz

Goal state after:
case h
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
⊢ (fun m ↦ m • Q) (Units.mk0 (P z) hPz / Units.mk0 (Q z) hQz) = P
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this✝ : (E.sigmaOfIsColimit hc).HasPullbacks
this : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
⊢ PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F

Tactic:
dsimp [E]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this✝ : (E.sigmaOfIsColimit hc).HasPullbacks
this : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
⊢ PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: ⊢ zariskiTopology.Subcanonical

Tactic:
by
  apply GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
  intro X
  rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange]
  rintro Y S hS x hx
  obtain ⟨(𝓤 : OpenCover Y), rfl⟩ := exists_cover_of_mem_pretopology hS
  let e : Y ⟶ X := 𝓤.glueMorphisms (fun j => x (𝓤.f _) (.mk _)) <| by
    intro i j
    apply hx
    exact Limits.pullback.condition
  refine ⟨e, ?_, ?_⟩
  · rintro Z e ⟨j⟩
    dsimp [e]
    rw [𝓤.ι_glueMorphisms]
  · intro e' h
    apply 𝓤.hom_ext
    intro j
    rw [𝓤.ι_glueMorphisms]
    exact h (𝓤.f j) (.mk j)

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
this :
  toAffine W
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1] =
    toAffine W P + toAffine W Q
hx : P x * Q z = Q x * P z
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
rwa [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            toAffine_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx]

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

Goal state before:
pp: case g.map_mul
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ ∀ (x y : A i),
    ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
        (x * y) =
      ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
          x *
        ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
          y

Tactic:
intro x y

Goal state after:
case g.map_mul
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
x y : A i
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
      (x * y) =
    ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i) x *
      ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i) y
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g✝ : (i : I) → f i
x : I
g : (i : I) → f i
⊢ f₁ g - f₂ g ∈ J

Tactic:
← Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g✝ : (i : I) → f i
x : I
g : (i : I) → f i
⊢ (Ideal.Quotient.mk J) (f₁ g - f₂ g) = 0
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: case map_mul
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} := ⋯
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := ⋯
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i := ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
⊢ ∀ (x y : A i),
    (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) (x * y) =
      (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) x *
        (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) y

Tactic:
intro x y

Goal state after:
case map_mul
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
x y : A i
⊢ (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) (x * y) =
    (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) x * (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) y
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝¹ : FormallyUnramified K L
this✝ : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := ⋯
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
this : IsUnit ((Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen))))
u : B
hu : (Ideal.Quotient.mk I) u = -↑this.unit⁻¹
⊢ (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I

Tactic:
← Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝¹ : FormallyUnramified K L
this✝ : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
this : IsUnit ((Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen))))
u : B
hu : (Ideal.Quotient.mk I) u = -↑this.unit⁻¹
⊢ (Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen)) * u + 1) = 0
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := ⋯
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ u * (aeval x) (minpoly K pb.gen) ∈ I

Tactic:
← Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (Ideal.Quotient.mk I) (u * (aeval x) (minpoly K pb.gen)) = 0
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h✝ : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
x y : L
h : x ∈ K⟮y⟯
⊢ (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)

Tactic:
have e : K⟮x⟯ ≤ K⟮y⟯ := by
      rw [IntermediateField.adjoin_le_iff]
      rintro _ rfl
      exact h

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h✝ : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
⊢ (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
⊢ ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Tactic:
intro x y

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
⊢ ∀ (x y : L),
    { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯ }.toFun (x * y) =
      { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯ }.toFun x *
        { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯ }.toFun y

Tactic:
intro x y

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
x y : L
⊢ { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯ }.toFun (x * y) =
    { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯ }.toFun x *
      { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯ }.toFun y
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case refine_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
⊢ ∀ (x y : L),
    (↑{ toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯ }).toFun (x + y) =
      (↑{ toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯ }).toFun x +
        (↑{ toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯ }).toFun y

Tactic:
intro x y

Goal state after:
case refine_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
x y : L
⊢ (↑{ toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯ }).toFun (x + y) =
    (↑{ toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯ }).toFun x +
      (↑{ toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯ }).toFun 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
inst✝ : Algebra.IsPushout R S A B
⊢ ∀ (x : S) (y : Ω[A⁄R]),
    (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
        (x ⊗ₜ[R] y) =
      (↑R LinearMap.id) (x ⊗ₜ[R] y)

Tactic:
intro x y

Goal state after:
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
x : S
y : Ω[A⁄R]
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] y) =
    (↑R LinearMap.id) (x ⊗ₜ[R] y)
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
b : AdicCauchySequence I N
⊢ ∃ a, (map I f) a = (mk I N) b

Tactic:
let a := mapPreimage hf 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 : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := mapPreimage hf b
⊢ ∃ a, (map I f) a = (mk I N) b
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 : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
j : σ
⊢ (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) j = 0 j

Tactic:
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply]

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 : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
j : σ
⊢ ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map j)) (P.relation x)) = 0