mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
⊢ Ideal.under R (Ideal.under S (IsLocalRing.maximalIdeal (Localization.AtPrime Q))) = Ideal.under R Q

Tactic:
Localization.AtPrime.under_maximalIdeal

Goal state after:
case e'_3
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
⊢ Ideal.under R Q = Ideal.under R Q
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ (g : A →ₐ[R] B ⧸ I), ∃ f, (Ideal.Quotient.mkₐ R I).comp f = g

Tactic:
change Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ Function.Surjective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case h₁
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
B✝ : Type u_1
inst✝¹ : CommRing B✝
inst✝ : FormallySmooth R A
I : Ideal B✝
hI : IsNilpotent I
B : Type u_1
⊢ ∀ [inst : CommRing B] (I : Ideal B),
    I ^ 2 = ⊥ → ∀ [inst_1 : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
case h₁
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type u_1
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I : Ideal B✝
hI : IsNilpotent I
B : Type u_1
inst✝ : CommRing B
⊢ ∀ (I : Ideal B), I ^ 2 = ⊥ → ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case h₁
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type u_1
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type u_1
inst✝ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
⊢ ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
case h₁
R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type u_1
inst✝³ : CommRing B✝
inst✝² : FormallySmooth R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type u_1
inst✝¹ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝ : Algebra R B
⊢ Function.Surjective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case h₂
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
B✝ : Type u_1
inst✝¹ : CommRing B✝
inst✝ : FormallySmooth R A
I : Ideal B✝
hI : IsNilpotent I
B : Type u_1
⊢ ∀ [inst : CommRing B] (I J : Ideal B),
    I ≤ J →
      (∀ [inst_1 : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst_1 : Algebra R (B ⧸ I)],
            Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst_1 : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R J).comp

Tactic:
_

Goal state after:
case h₂
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type u_1
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I : Ideal B✝
hI : IsNilpotent I
B : Type u_1
inst✝ : CommRing B
⊢ ∀ (I J : Ideal B),
    I ≤ J →
      (∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst : Algebra R (B ⧸ I)],
            Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R J).comp
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case h₂
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type u_1
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u_1
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
⊢ ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R J).comp

Tactic:
_

Goal state after:
case h₂
R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type u_1
inst✝³ : CommRing B✝
inst✝² : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u_1
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
⊢ Function.Surjective (Ideal.Quotient.mkₐ R J).comp
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_1
P : Type u_2
C : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : CommRing C
inst✝³ : Algebra R C
inst✝² : CommRing P
inst✝¹ : Algebra R P
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
lift : P₁.Ring →ₐ[R] P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
⊢ P₁.ker * P₁.ker ≤ RingHom.ker lift

Tactic:
Ideal.mul_le

Goal state after:
R : Type u
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_1
P : Type u_2
C : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : CommRing C
inst✝³ : Algebra R C
inst✝² : CommRing P
inst✝¹ : Algebra R P
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
lift : P₁.Ring →ₐ[R] P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
⊢ ∀ r ∈ P₁.ker, ∀ s ∈ P₁.ker, r * s ∈ RingHom.ker lift
Module: Mathlib.RingTheory.Etale.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyEtale R S
⊢ FormallyEtale Rₘ Sₘ

Tactic:
have : FormallyEtale S Sₘ := FormallyEtale.of_isLocalization (M.map (algebraMap R S))
  have : FormallyEtale R Sₘ := FormallyEtale.comp R S Sₘ
  exact FormallyEtale.localization_base M

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Etale R A ↔ FormallyUnramified R A ∧ Smooth R A

Tactic:
by
  rw [etale_iff, FormallyEtale.iff_formallyUnramified_and_formallySmooth, smooth_iff]
  tauto

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
P₁ : Extension R A
P₂ : Extension R A
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
⊢ ↑(equivOfFormallySmooth P₁ P₂) = map f

Tactic:
by
  ext1 x
  refine (LinearEquiv.symm_apply_eq _).mpr ?_
  change ((map (P₁.homInfinitesimal P₂)).restrictScalars A ∘ₗ map P₁.toInfinitesimal) x =
    ((map P₂.toInfinitesimal).restrictScalars A ∘ₗ map f) x
  rw [← map_comp, ← map_comp, map_eq]

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

Goal state before:
pp: case h2
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 : (Q.comp P).toExtension.Cotangent),
    (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x = 0 →
      x ∈ (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
· intro x hx
    obtain ⟨⟨x : (Q.comp P).Ring, hx'⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
    replace hx : (Q.ofComp P).toAlgHom x ∈ Q.ker ^ 2 := by
      simpa only [map_mk, val_mk, val_zero, Ideal.toCotangent_eq_zero] using! congr(($hx).val)
    rw [pow_two, ← map_ofComp_ker (P := P), ← Ideal.map_mul, Ideal.mem_map_iff_of_surjective
      _ (toAlgHom_ofComp_surjective Q P)] at hx
    obtain ⟨y, hy, e⟩ := hx
    rw [eq_comm, ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, ← map_toComp_ker] at e
    rw [LinearMap.range_liftBaseChange]
    let z : (Q.comp P).ker := ⟨x - y, Ideal.sub_mem _ hx' (Ideal.mul_le_right hy)⟩
    have hz : z.1 ∈ P.ker.map (Q.toComp P).toAlgHom.toRingHom := e
    have : Extension.Cotangent.mk (P := (Q.comp P).toExtension) ⟨x, hx'⟩ =
      Extension.Cotangent.mk z := by
      ext; simpa only [val_mk, Ideal.toCotangent_eq, sub_sub_cancel, pow_two, z]
    rw [this, ← Submodule.restrictScalars_mem (Q.comp P).Ring, ← Submodule.mem_comap,
      ← Submodule.span_singleton_le_iff_mem, ← Submodule.map_le_map_iff_of_injective
      (f := Submodule.subtype _) Subtype.val_injective, Submodule.map_subtype_span_singleton,
      Submodule.span_singleton_le_iff_mem]
    refine (show Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker ≤ _ from ?_) hz
    rw [Ideal.map_le_iff_le_comap]
    rintro w hw
    simp only [AlgHom.toRingHom_eq_coe, Ideal.mem_comap, RingHom.coe_coe,
      Submodule.mem_map, Submodule.mem_comap, Submodule.restrictScalars_mem, Submodule.coe_subtype,
      Subtype.exists, exists_and_right, exists_eq_right,
      toExtension_Ring]
    refine ⟨?_, Submodule.subset_span ⟨Extension.Cotangent.mk ⟨w, hw⟩, ?_⟩⟩
    · simp only [ker_eq_ker_aeval_val, RingHom.mem_ker, Hom.algebraMap_toAlgHom]
      rw [aeval_val_eq_zero hw, map_zero]
    · rw [map_mk]
      rfl

Goal state after:
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 σ
| ⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))

Tactic:
rw [← LinearEquiv.symm_symm (compEquiv Q P)]

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 σ
| ⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P).symm.symm)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type u_3
⊢ ∀ [inst : CommRing B] [inst_1 : Algebra K B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ K I).comp

Tactic:
_

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
B : Type u_3
inst✝ : CommRing B
⊢ ∀ [inst : Algebra K B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ K I).comp
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
B : Type u_3
inst✝ : CommRing B
⊢ ∀ [inst : Algebra K B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ K I).comp

Tactic:
_

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
⊢ ∀ (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ K I).comp
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
⊢ (algebraMap P S) (σ 1) = (algebraMap P S) 1

Tactic:
simp [hσ]

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
this : ∀ (x y : S ⊗[P] Ω[P⁄R]), ↑(l x) * ↑(l y) = 0
⊢ (algebraMap P S) (σ (a * b)) = (algebraMap P S) (σ a * σ b)

Tactic:
simp [hσ]

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
⊢ (algebraMap P S) (σ 0) = (algebraMap P S) 0

Tactic:
simp [hσ]

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
⊢ (algebraMap P S) (σ (a + b)) = (algebraMap P S) (σ a + σ b)

Tactic:
simp [hσ]

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
x : P
⊢ (algebraMap P S) (σ ((algebraMap P S) x)) = (algebraMap P S) x

Tactic:
simp [hσ]

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
inst✝¹ : IsScalarTower R S T
inst✝ : Algebra.FormallyEtale S T
x : Algebra.H1Cotangent S T
hx : (mapBaseChange R S T) ((Algebra.H1Cotangent.δ R S T) x) = 0
⊢ (Algebra.H1Cotangent.δ R S T) x = 0

Tactic:
rw [Subsingleton.elim x 0, map_zero]

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

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this : Nontrivial (L ⊗[K] L)
x : L
⊢ x ∈ ⊤ → x ∈ (algebraMap K L).range

Tactic:
_

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
⊢ x ∈ (algebraMap K L).range
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case 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 σ
x : T
y : P.toExtension.H1Cotangent
⊢ (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((LinearMap.lTensor T Extension.h1Cotangentι) (x ⊗ₜ[S] y)) ∈
    (Q.comp P).toExtension.cotangentComplex.ker

Tactic:
| tmul x y =>

Goal state after:
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) =
    ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
        ((lTensor T Extension.h1Cotangentι) (x ⊗ₜ[S] y)),
      x_in⟩

Tactic:
| tmul x y =>

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
⊢ q ∈ Finset.univ →
    (↑((primesOverOrderIsoFiber R S p).symm.toEquiv q)).ramificationIdx R *
        (↑((primesOverOrderIsoFiber R S p).symm.toEquiv q)).inertiaDeg R =
      finrank p.ResidueField (Localization.AtPrime q.asIdeal)

Tactic:
_

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
⊢ (↑((primesOverOrderIsoFiber R S p).symm.toEquiv q)).ramificationIdx R *
      (↑((primesOverOrderIsoFiber R S p).symm.toEquiv q)).inertiaDeg R =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
hp : map (algebraMap R S) p ≠ ⊥
⊢ q.ramificationIdx R = multiplicity q (map (algebraMap R S) p)

Tactic:
have hq : q ≠ ⊥ := ne_bot_of_le_ne_bot hp (map_le_of_le_comap (q.over_def p).le)

Goal state after:
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.IsPrime
inst✝ : q.LiesOver p
hp : map (algebraMap R S) p ≠ ⊥
hq : q ≠ ⊥
⊢ q.ramificationIdx R = multiplicity q (map (algebraMap R S) p)
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(span {a})
ha0 : span {a} ≠ ⊥
⊢ x ∈ ⨆ P, primaryComponent M P.asIdeal

Tactic:
← iInf_maxPowDividing_eq ha0

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
⊢ x ∈ ⨆ P, primaryComponent M P.asIdeal
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ι : Sort u_1
⊢ ⨆ x, 0 = 0

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨆ x, 0 = 0

case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨆ x, 0 = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ι : Sort u_1
⊢ ⨅ x, 0 = 0

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨅ x, 0 = 0

case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨅ x, 0 = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
⊢ sInf s ≤ sSup s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)
  · rw [sInf_empty, sSup_empty]
  · exact csInf_le_csSup hne h₁ h₂

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
v : HeightOneSpectrum R
⊢ v ∈ Finite.toFinset h✝ → v.maxPowDividing I ≠ 0

Tactic:
_

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
v : HeightOneSpectrum R
a✝ : v ∈ Finite.toFinset h✝
⊢ v.maxPowDividing I ≠ 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : IsEmpty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

case inr
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : Nonempty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y

Tactic:
· have : Nonempty s := hs.to_subtype
            refine ciSup_le fun p ↦ (map_mul_le_add p.1 x y).trans ?_
            gcongr
            all_goals
              apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p
              simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : IsEmpty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

case inr
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : Nonempty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
by
  simp only [ne_eq, toReal_eq_zero_iff, not_or]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ≥0∞
⊢ ↑(x + y) = ↑x + ↑y

Tactic:
cases x <;> cases y <;> rfl

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹⁻¹ = 1⁻¹ ↔ a = 1

Tactic:
inv_inv,

Goal state after:
a : ℝ≥0∞
⊢ a = 1⁻¹ ↔ a = 1