mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
⊢ Function.Bijective ⇑↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
⊢ Function.Bijective ⇑↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.Ring
x_in : x ∈ P.toExtension.ker
property✝ : Extension.Cotangent.mk ⟨x, x_in⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ (↑((Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom)
          ((Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)
            ⟨Extension.Cotangent.mk ⟨x, x_in⟩, property✝⟩))).val =
    (↑0).val

Tactic:
;

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.Ring
x_in : x ∈ P.toExtension.ker
property✝ : Extension.Cotangent.mk ⟨x, x_in⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ (↑((Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom)
          ((Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)
            ⟨Extension.Cotangent.mk ⟨x, x_in⟩, property✝⟩))).val =
    (↑0).val
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: case mem
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x✝ : S
x : R
hx : x ∈ ↑(maximalIdeal R)
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) ((algebraMap R S) x) = 0

Tactic:
;

Goal state after:
case mem
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x✝ : S
x : R
hx : x ∈ ↑(maximalIdeal R)
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) ((algebraMap R S) x) = 0
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : S
hx : x ∈ Ideal.map (algebraMap R S) (maximalIdeal R)
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0

Tactic:
induction hx using Submodule.span_induction with

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
⊢ (tensorCotangentInvFun f halg H) (x • Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) =
    (tensorCotangentInvFun f halg H) (x • Cotangent.mk ((f.mapKer halg) y))

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
⊢ (tensorCotangentInvFun f halg H) (x • Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) =
    (tensorCotangentInvFun f halg H) (x • Cotangent.mk ((f.mapKer halg) y))
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Ideal.map (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) p

Tactic:
rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq,
    ← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map, Localization.localRingHom,
    IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
hq : p.primesOver S = {q}
inst✝³ : Module.Finite R S
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
s : Finset S
hs : Submodule.span R ↑s = ⊤
⊢ Submodule.span (Localization.AtPrime p)
      ↑(Submodule.span R (⇑(IsScalarTower.toAlgHom R S (Localization.AtPrime q)).toLinearMap '' ↑s)) =
    ⊤

Tactic:
← Submodule.map_span,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
hq : p.primesOver S = {q}
inst✝³ : Module.Finite R S
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
s : Finset S
hs : Submodule.span R ↑s = ⊤
⊢ Submodule.span (Localization.AtPrime p)
      ↑(Submodule.map (IsScalarTower.toAlgHom R S (Localization.AtPrime q)).toLinearMap (Submodule.span R ↑s)) =
    ⊤
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x : T ⊗[S] P.toExtension.H1Cotangent
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) x =
    ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x),
      x_in⟩

Tactic:
;

Goal state after:
case h
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x : T ⊗[S] P.toExtension.H1Cotangent
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) x =
    ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x),
      x_in⟩
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h.zero
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) 0) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (↑((liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) 0)).val =
    (↑⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) 0),
          x_in⟩).val

Tactic:
;

Goal state after:
case h.zero
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) 0) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (↑((liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) 0)).val =
    (↑⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) 0),
          x_in⟩).val
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h.tmul
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x : T
y : P.toExtension.H1Cotangent
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((lTensor T Extension.h1Cotangentι) (x ⊗ₜ[S] y)) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (↑((liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) (x ⊗ₜ[S] y))).val =
    (↑⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
            ((lTensor T Extension.h1Cotangentι) (x ⊗ₜ[S] y)),
          x_in⟩).val

Tactic:
;

Goal state after:
case h.tmul
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x : T
y : P.toExtension.H1Cotangent
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((lTensor T Extension.h1Cotangentι) (x ⊗ₜ[S] y)) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (↑((liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) (x ⊗ₜ[S] y))).val =
    (↑⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
            ((lTensor T Extension.h1Cotangentι) (x ⊗ₜ[S] y)),
          x_in⟩).val
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x✝ : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
x : P.Cotangent
⊢ ((AlgebraTensorModule.curry
          (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex))
        1)
      x =
    ((AlgebraTensorModule.curry (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f))) 1) x

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x✝ : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
x : P.Cotangent
⊢ ((AlgebraTensorModule.curry
          (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex))
        1)
      x =
    ((AlgebraTensorModule.curry (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f))) 1) x
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x✝ : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
x : ↥P.ker
⊢ ((AlgebraTensorModule.curry
          (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex))
        1)
      (Cotangent.mk x) =
    ((AlgebraTensorModule.curry (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f))) 1)
      (Cotangent.mk x)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x✝ : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
x : ↥P.ker
⊢ ((AlgebraTensorModule.curry
          (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex))
        1)
      (Cotangent.mk x) =
    ((AlgebraTensorModule.curry (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f))) 1)
      (Cotangent.mk x)
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
a : T ⊗[S] P.H1Cotangent
ha : (LinearMap.baseChange T h1Cotangentι) a = (tensorCotangent f halg H₂).symm ↑x
x✝ : P.H1Cotangent
⊢ (((AlgebraTensorModule.curry (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f))) 1) x✝).val =
    (((AlgebraTensorModule.curry (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι))
          1)
        x✝).val

Tactic:
;

Goal state after:
case right
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
a : T ⊗[S] P.H1Cotangent
ha : (LinearMap.baseChange T h1Cotangentι) a = (tensorCotangent f halg H₂).symm ↑x
x✝ : P.H1Cotangent
⊢ (((AlgebraTensorModule.curry (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f))) 1) x✝).val =
    (((AlgebraTensorModule.curry (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι))
          1)
        x✝).val
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hp0 : map (algebraMap R S) p ≠ ⊥
hq : q.IsPrime
⊢ q.ramificationIdx R = Multiset.count q (factors (map (algebraMap R S) p))

pp: case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hp0 : map (algebraMap R S) p ≠ ⊥
hq : ¬q.IsPrime
⊢ q.ramificationIdx R = Multiset.count q (factors (map (algebraMap R S) p))

Tactic:
;

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hp0 : map (algebraMap R S) p ≠ ⊥
hq : q.IsPrime
⊢ q.ramificationIdx R = Multiset.count q (factors (map (algebraMap R S) p))

case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hp0 : map (algebraMap R S) p ≠ ⊥
hq : ¬q.IsPrime
⊢ q.ramificationIdx R = Multiset.count q (factors (map (algebraMap R S) p))
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

pp: case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
;

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := ⋯
M' : Submonoid P.Ring := ⋯
fQ : Localization M' →ₐ[R] T := ⋯
Q : Extension R T := ⋯
f : P.Hom Q := ⋯
this✝⁹ : FormallySmooth R P.Ring
this✝⁸ : FormallySmooth P.Ring (Localization M')
this✝⁷ : FormallySmooth R Q.Ring
this✝⁶ : Module.Flat S T
this✝⁵ : Algebra P.Ring Q.Ring := ⋯
this✝⁴ : Algebra P.Ring T := ⋯
this✝³ : Algebra (Localization M') T := ⋯
this✝² : IsScalarTower P.Ring S T
this✝¹ : IsScalarTower P.Ring (Localization M') T
this✝ : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := ⋯
this :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (Algebra.linearMap P.Ring S).ker =
    RingHom.ker fQ
x✝ : ↥P.ker
⊢ ↑(F x✝) =
    ↑((↑(LinearEquiv.restrictScalars P.Ring
              (LinearEquiv.ofEq
                (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                  (Algebra.linearMap P.Ring S).ker)
                (RingHom.ker fQ) this)) ∘ₗ
          Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker)
        x✝)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := ⋯
M' : Submonoid P.Ring := ⋯
fQ : Localization M' →ₐ[R] T := ⋯
Q : Extension R T := ⋯
f : P.Hom Q := ⋯
this✝⁹ : FormallySmooth R P.Ring
this✝⁸ : FormallySmooth P.Ring (Localization M')
this✝⁷ : FormallySmooth R Q.Ring
this✝⁶ : Module.Flat S T
this✝⁵ : Algebra P.Ring Q.Ring := ⋯
this✝⁴ : Algebra P.Ring T := ⋯
this✝³ : Algebra (Localization M') T := ⋯
this✝² : IsScalarTower P.Ring S T
this✝¹ : IsScalarTower P.Ring (Localization M') T
this✝ : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := ⋯
this :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (Algebra.linearMap P.Ring S).ker =
    RingHom.ker fQ
x✝ : ↥P.ker
⊢ ↑(F x✝) =
    ↑((↑(LinearEquiv.restrictScalars P.Ring
              (LinearEquiv.ofEq
                (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                  (Algebra.linearMap P.Ring S).ker)
                (RingHom.ker fQ) this)) ∘ₗ
          Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker)
        x✝)
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a

pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a

Tactic:
;

Goal state after:
case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a

case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a