mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ w ≤ φ.lexOrder → ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff d) φ = 0

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ (∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff d) φ = 0) → w ≤ φ.lexOrder

Tactic:
· intro h d hd
    apply coeff_eq_zero_of_lt_lexOrder
    exact lt_of_lt_of_le hd h

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ (∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff d) φ = 0) → w ≤ φ.lexOrder
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
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : u = p ∧ v = q
⊢ (u, v) = (p, q)

Tactic:
simp [h''.1, h''.2]

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 σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (coeff p) φ * (coeff q) ψ ≠ 0

Tactic:
mul_ne_zero_iff

Goal state after:
σ : 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)
⊢ (coeff p) φ ≠ 0 ∧ (coeff q) ψ ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsLeft R
p : MvPowerSeries σ R
hrp : (monomial n) r * p = 0
i : σ →₀ ℕ
⊢ (coeff i) p = (coeff i) 0

Tactic:
have := congr(coeff (i + n) $hrp)

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsLeft R
p : MvPowerSeries σ R
hrp : (monomial n) r * p = 0
i : σ →₀ ℕ
this : (coeff (i + n)) ((monomial n) r * p) = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsRight R
p : MvPowerSeries σ R
hrp : p * (monomial n) r = 0
i : σ →₀ ℕ
⊢ (coeff i) p = (coeff i) 0

Tactic:
have := congr(coeff (i + n) $hrp)

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsRight R
p : MvPowerSeries σ R
hrp : p * (monomial n) r = 0
i : σ →₀ ℕ
this : (coeff (i + n)) (p * (monomial n) r) = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

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

Tactic:
ofJ0,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.c₄ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ (ofJ0 R).Δ = -27

Tactic:
ofJ0,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.Δ = -27
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: 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
⊢ 2 * 2 = 1

Tactic:
by linear_combination h3

Goal state after:
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)
      rw [h0, ofJ_0_of_three_ne_zero h3]
      infer_instance

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

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
⊢ 2 * 2 = 1

Tactic:
by linear_combination h3

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

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

Tactic:
rw [addZ, neg_X, neg_Y, neg_Z, negY]
  ring1

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ Type u_2
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  (ConcreteCategory.hom (F.map (pullback.fst (E.f i) (E.f j)).op)) (s.val i) =
    (ConcreteCategory.hom (F.map (pullback.snd (E.f i) (E.f j)).op)) (s.val j)
⊢ (ConcreteCategory.hom (F.map gi.op)) (s.val i) = (ConcreteCategory.hom (F.map gj.op)) (s.val j)

Tactic:
← pullback.lift_fst _ _ hgij

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ Type u_2
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  (ConcreteCategory.hom (F.map (pullback.fst (E.f i) (E.f j)).op)) (s.val i) =
    (ConcreteCategory.hom (F.map (pullback.snd (E.f i) (E.f j)).op)) (s.val j)
⊢ (ConcreteCategory.hom (F.map (pullback.lift gi gj hgij ≫ pullback.fst (E.f i) (E.f j)).op)) (s.val i) =
    (ConcreteCategory.hom (F.map gj.op)) (s.val j)
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
b : Equalizer.Presieve.Arrows.FirstObj F X
⊢ (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

Tactic:
_

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.Point

Goal state before:
pp: R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field F
inst✝⁷ : Field K
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
⊢ (W'⁄K).add (⇑↑f ∘ P) (⇑↑f ∘ Q) = ⇑↑f ∘ (W'⁄F).add P Q

Tactic:
← WeierstrassCurve.Projective.map_add _ hP hQ,

Goal state after:
R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field F
inst✝⁷ : Field K
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
⊢ (W'⁄K).add (⇑↑f ∘ P) (⇑↑f ∘ Q) = ((W'⁄F).map ↑f).add (⇑↑f ∘ P) (⇑↑f ∘ Q)
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: ⊢ precoverage ≤ Precoverage.comap uliftFunctor precoverage

Tactic:
refine Precoverage.le_of_zeroHypercover fun X E ↦ ?_

Goal state after:
X : TopCat
E : precoverage.ZeroHypercover X
⊢ E.presieve₀ ∈ (Precoverage.comap uliftFunctor precoverage).coverings X
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified

Tactic:
_

Goal state after:
R S : Type u_3
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified

Tactic:
_

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (e : R ≃+* S), e.toRingHom.FormallyUnramified
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (algebraMap R S)

Tactic:
_

Goal state after:
R S : Type u_3
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] [inst_1 : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (algebraMap R S)
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] [inst_1 : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (algebraMap R S)

Tactic:
_

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ [inst : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (algebraMap R S)
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ [inst : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (algebraMap R S)

Tactic:
_

Goal state after:
R S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ∀ (M : Submonoid R) [IsLocalization M S], (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (algebraMap R S)
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
M : Submonoid R
⊢ ∀ [IsLocalization M S], (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (algebraMap R S)

Tactic:
_

Goal state after:
R S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ (algebraMap R S).FormallyUnramified
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: ⊢ HoldsForLocalization fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
intro R S _ _ _ M _

Goal state after:
R S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ (algebraMap R S).FormallyUnramified
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    (∀ (J : Ideal S) (x : J.IsPrime),
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)) →
      (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f

Tactic:
_

Goal state after:
R S : Type u_3
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (f : R →+* S),
    (∀ (J : Ideal S) (x : J.IsPrime),
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)) →
      (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (f : R →+* S),
    (∀ (J : Ideal S) (x : J.IsPrime),
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)) →
      (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f

Tactic:
_

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (f : R →+* S),
    (∀ (J : Ideal S) (x : J.IsPrime),
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)) →
      (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f

Tactic:
_

Goal state after:
R S : Type u_3
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f

Tactic:
_

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr
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_1 : Algebra R B] (I_1 : Ideal B),
    I_1 ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I_1).comp

Tactic:
_

Goal state after:
case intro.mpr
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] (I_1 : Ideal B), I_1 ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I_1).comp
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr
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] (I_1 : Ideal B), I_1 ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I_1).comp

Tactic:
_

Goal state after:
case intro.mpr
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
⊢ ∀ (I_1 : Ideal B), I_1 ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I_1).comp
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 x : L
⊢ x ∈ {x✝, y} → IsIntegral K x

Tactic:
_

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 x : L
a✝ : x ∈ {x✝, y}
⊢ IsIntegral K x
Module: Mathlib.LinearAlgebra.SModEq.Pointwise

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : x - y ∈ U
c : R
hc : c ∈ I
⊢ c • x - c • y ∈ I • U

Tactic:
rw [← smul_sub]

Goal state after:
R : Type u_1
inst✝² : Ring R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : x - y ∈ U
c : R
hc : c ∈ I
⊢ c • (x - y) ∈ I • U
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case 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 y : B
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B)))
      ((derivationTensorProduct R S A B).liftKaehlerDifferential ((D S B).tensorProductTo (x ⊗ₜ[S] y))) =
    (D S B).tensorProductTo (x ⊗ₜ[S] y)

Tactic:
| tmul x y =>

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
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
  AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm) (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
      TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
x : B
y : Ω[A⁄R]
⊢ e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • x ⊗ₜ[A] y) =
    (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ (x ⊗ₜ[A] y)

Tactic:
| tmul x y =>

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

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Flat R S
inst✝¹⁰ : CommRing P
inst✝⁹ : Algebra R P
inst✝⁸ : Algebra P S
inst✝⁷ : IsScalarTower R P S
inst✝⁶ : IsLocalRing R
inst✝⁵ : IsLocalRing S
inst✝⁴ : IsLocalHom (algebraMap R S)
inst✝³ : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
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
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst✝³ : Algebra Pp Sp := φ.toAlgebra
algInst✝² : Algebra P Sp := (φ.comp (algebraMap P Pp)).toAlgebra
algInst✝¹ : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst✝ : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst✝¹ : IsScalarTower P Pp Sp := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P Sp))
scalarTowerInst✝ : IsScalarTower Pp Sp 𝓀[S] := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Pp 𝓀[S]))
this✝⁷ : IsScalarTower 𝓀[R] Pp Sp
this✝⁶ : IsScalarTower R Sp 𝓀[S]
this✝⁵ : IsScalarTower P S Sp
this✝⁴ : IsScalarTower S Sp 𝓀[S]
this✝³ : IsScalarTower P Sp 𝓀[S]
this✝² : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp).symm
this✝¹ : Module.Free Pp Ω[Pp⁄𝓀[R]]
this✝ : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (algebraMap P S)) := kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective ⇑φ
h₂' : (RingHom.ker φ).FG
h₃ : 𝓂[Sp] ≤ RingHom.ker ψ
this : Function.Injective ⇑(KaehlerDifferential.cotangentComplexBaseChange 𝓀[R] Sp Pp 𝓀[S])
eᵣ : 𝓀[S] ⊗[Pp] Ω[Pp⁄𝓀[R]] ≃ₗ[S] 𝓀[S] ⊗[P] Ω[P⁄R] :=
  LinearEquiv.restrictScalars S (AlgebraTensorModule.congr (LinearEquiv.refl 𝓀[S] 𝓀[S]) e₀) ≪≫ₗ
    LinearEquiv.restrictScalars S (AlgebraTensorModule.cancelBaseChange P Pp Sp 𝓀[S] Ω[P⁄R])
eₗ : 𝓀[S] ⊗[Pp] ↥(RingHom.ker φ) ≃ₗ[S] 𝓀[S] ⊗[P] ↥(RingHom.ker (algebraMap P S)) :=
  LinearEquiv.restrictScalars S (AlgebraTensorModule.congr (LinearEquiv.refl 𝓀[S] 𝓀[S]) e₁) ≪≫ₗ
    LinearEquiv.restrictScalars S (AlgebraTensorModule.cancelBaseChange P Pp Sp 𝓀[S] ↥(RingHom.ker (algebraMap P S)))
x : 𝓀[S]
y : ↥(RingHom.ker (algebraMap P S))
⊢ (KaehlerDifferential.cotangentComplexBaseChange R S P 𝓀[S]) (x ⊗ₜ[P] y) =
    eᵣ ((KaehlerDifferential.cotangentComplexBaseChange 𝓀[R] Sp Pp 𝓀[S]) (eₗ.symm (x ⊗ₜ[P] y)))

Tactic:
| tmul x y =>

Goal state after:
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 : AdicCompletion I R
x : AdicCompletion I M
n : ℕ
⊢ ↑((r • s) • x) n = ↑(r • s • x) n

Tactic:
rw [smul_eval, val_smul_apply, val_smul_apply, smul_eval, smul_assoc]

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

Goal state before:
pp: S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n • ⊤)) ((ofAlgEquiv I).symm x) = (eval I S n) x

Tactic:
nth_rw 2 [← of_ofAlgEquiv_symm I x]
  simp [-of_ofAlgEquiv_symm, eval]

Goal state after: