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

Goal state before:
pp: case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
⊢ ↑f₁ = ↑f₂

Tactic:
let f := RingHom.ker (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom

Goal state after:
case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) :=
  RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom
⊢ ↑f₁ = ↑f₂
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
this : ∀ (i : I), ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i
⊢ (∑ a ∈ f.support, (b.repr (x * f a)).sum fun b' c ↦ c • b b' ⊗ₜ[R] b a) =
    ∑ a_1 ∈ f.support.biUnion fun i ↦ (a i).support,
      (b.repr (f.sum fun i y ↦ (a i) a_1 • y)).sum fun b' c ↦ c • b b' ⊗ₜ[R] b a_1

Tactic:
trans (x ⊗ₜ 1) * elem R S

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := ⋯
F : I →₀ I →₀ R := ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R := ⋯
this : ∀ (i : I), ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i
⊢ (∑ a ∈ f.support, (b.repr (x * f a)).sum fun b' c ↦ c • b b' ⊗ₜ[R] b a) = x ⊗ₜ[R] 1 * elem R S

R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := ⋯
F : I →₀ I →₀ R := ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R := ⋯
this : ∀ (i : I), ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i
⊢ x ⊗ₜ[R] 1 * elem R S =
    ∑ a_1 ∈ f.support.biUnion fun i ↦ (a i).support,
      (b.repr (f.sum fun i y ↦ (a i) a_1 • y)).sum fun b' c ↦ c • b b' ⊗ₜ[R] b a_1
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
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ [inst_1 : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R I).comp

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
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [inst_1 : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst_1 : Algebra R (S ⧸ I)],
            Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst_1 : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R J).comp

Tactic:
· intro B _ I hI _; exact FormallySmooth.comp_surjective R A I hI

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
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [inst_1 : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst_1 : Algebra R (S ⧸ I)],
            Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst_1 : Algebra R S], 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
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [inst_1 : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst_1 : Algebra R (S ⧸ I)],
            Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst_1 : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R J).comp

Tactic:
· intro B _ I J hIJ h₁ h₂ _ g
    let : ((B ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)) ≃ₐ[R] B ⧸ J :=
      { (DoubleQuot.quotQuotEquivQuotSup I J).trans
          (Ideal.quotEquivOfEq (sup_eq_right.mpr hIJ)) with
        commutes' := fun x => rfl }
    obtain ⟨g', e⟩ := h₂ (this.symm.toAlgHom.comp g)
    obtain ⟨g', rfl⟩ := h₁ g'
    replace e := congr_arg this.toAlgHom.comp e
    conv_rhs at e =>
      rw [← AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.id_comp]
    exact ⟨g', e⟩

Goal state after:
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
this : FormallyEtale S Sₘ
⊢ FormallyEtale Rₘ Sₘ

Tactic:
have : FormallyEtale R Sₘ := FormallyEtale.comp R S Sₘ

Goal state after:
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
this✝ : FormallyEtale S Sₘ
this : FormallyEtale R Sₘ
⊢ FormallyEtale Rₘ Sₘ
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
M : Submonoid R
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : IsScalarTower R Rₘ Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x✝¹ : CommRing Q
x✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ (↑(lift I ⋯ (AlgHom.restrictScalars R f))).comp ((algebraMap Rₘ Sₘ).comp (algebraMap R Rₘ)) =
    (algebraMap Rₘ Q).comp (algebraMap R Rₘ)

Tactic:
← IsScalarTower.algebraMap_eq,

Goal state after:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
M : Submonoid R
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : IsScalarTower R Rₘ Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x✝¹ : CommRing Q
x✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ (↑(lift I ⋯ (AlgHom.restrictScalars R f))).comp (algebraMap R Sₘ) = (algebraMap Rₘ Q).comp (algebraMap R Rₘ)
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
M : Submonoid R
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : IsScalarTower R Rₘ Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x✝¹ : CommRing Q
x✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ (↑(lift I ⋯ (AlgHom.restrictScalars R f))).comp (algebraMap R Sₘ) = (algebraMap Rₘ Q).comp (algebraMap R Rₘ)

Tactic:
← IsScalarTower.algebraMap_eq,

Goal state after:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
M : Submonoid R
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : IsScalarTower R Rₘ Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x✝¹ : CommRing Q
x✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ (↑(lift I ⋯ (AlgHom.restrictScalars R f))).comp (algebraMap R Sₘ) = algebraMap R Q
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case add
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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
x₁ x₂ : MvPolynomial ι S
hx₁ :
  (δAux R Q') (f.toAlgHom x₁) =
    (δAux R Q) x₁ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁))
hx₂ :
  (δAux R Q') (f.toAlgHom x₂) =
    (δAux R Q) x₂ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))
⊢ (δAux R Q) x₁ +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁)) +
      ((δAux R Q) x₂ +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))) =
    (δAux R Q) x₁ + (δAux R Q) x₂ +
      ((Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁)) +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂)))

Tactic:
add_add_add_comm

Goal state after:
case add
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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
x₁ x₂ : MvPolynomial ι S
hx₁ :
  (δAux R Q') (f.toAlgHom x₁) =
    (δAux R Q) x₁ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁))
hx₂ :
  (δAux R Q') (f.toAlgHom x₂) =
    (δAux R Q) x₂ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))
⊢ (δAux R Q) x₁ + (δAux R Q) x₂ +
      ((Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁)) +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))) =
    (δAux R Q) x₁ + (δAux R Q) x₂ +
      ((Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁)) +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂)))
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case C
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 σ
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
s : R
⊢ (δAux R Q) ((Q.ofComp P).toAlgHom (C s)) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) (C s))).2

Tactic:
simp only [algHom_C, δAux_C, derivation_C, Derivation.map_algebraMap,
      tmul_zero, map_zero, MvPolynomial.algebraMap_apply, Prod.snd_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
⊢ Nontrivial (L ⊗[K] L)

Tactic:
← not_subsingleton_iff_nontrivial,

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
⊢ ¬Subsingleton (L ⊗[K] L)
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.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h :
  map ((algebraMap S (Localization.AtPrime q)).comp (algebraMap R S)) p =
    map (algebraMap S (Localization.AtPrime q)) (q ^ p.ramificationIdx' q * I)
⊢ p.ramificationIdx' q = q.ramificationIdx R

Tactic:
← IsScalarTower.algebraMap_eq,

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.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h :
  map (algebraMap R (Localization.AtPrime q)) p =
    map (algebraMap S (Localization.AtPrime q)) (q ^ p.ramificationIdx' q * I)
⊢ p.ramificationIdx' q = q.ramificationIdx R
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
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:
ramificationIdx_of_not_isPrime q R hq,

Goal state after:
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
⊢ 0 = Multiset.count q (factors (map (algebraMap R S) p))
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, x ≤ a
ha : 0 ≤ a
⊢ sSup s ≤ a

Tactic:
by
  obtain rfl | hs' := s.eq_empty_or_nonempty
  exacts [sSup_empty.trans_le ha, csSup_le hs' hs]

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive ↑x
nonpos : ∀ (x : ℝ≥0), motive ↑x → motive (-↑x)
r : ℝ
⊢ motive r

Tactic:
by
  obtain ⟨r, (rfl | rfl)⟩ := r.nnreal_dichotomy
  all_goals simp_all

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

Goal state before:
pp: a : ℝ
h : (ENNReal.ofReal a).toReal = a
⊢ 0 ≤ a

Tactic:
by
    rw [← h]
    exact toReal_nonneg

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

Goal state before:
pp: b : ℝ≥0∞
p : ℝ≥0
right✝ h : ↑p < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Tactic:
rcases exists_between h with ⟨c, pc, cb⟩

Goal state after:
b : ℝ≥0∞
p : ℝ≥0
right✝ h : ↑p < b
c : ℝ≥0∞
pc : ↑p < c
cb : c < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ p (u * v) + q (x / u * (y / v)) ≤ p u + q (x / u) + (p v + q (y / v))

Tactic:
add_add_add_comm

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ p (u * v) + q (x / u * (y / v)) ≤ p u + p v + (q (x / u) + q (y / v))
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ [[↑x, ↑y]] ⊆ s

pp: case mpr
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[↑x, ↑y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y

Tactic:
· rw [← mem_ordConnectedComponent, ← ordConnectedComponent_ordConnectedProj, h,
      ordConnectedComponent_ordConnectedProj, self_mem_ordConnectedComponent]
    exact y.2

Goal state after:
case mpr
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[↑x, ↑y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ ↑a - ↑x✝ - (↑a - ↑b) = ↑b - ↑x✝

Tactic:
norm_cast
    rw [tsub_tsub_tsub_cancel_left]
    exact mod_cast h

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

Goal state before:
pp: case succ
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
⊢ count K v (I ^ (n + 1)) = ↑(n + 1) * count K v I

Tactic:
| succ n h =>

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

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ ∞
hb₀ : ∞ ≠ 0
⊢ 0 < 1 ∧ 1 * a < ∞

Tactic:
by simpa [lt_top_iff_ne_top]

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

Goal state before:
pp: a b c : ℝ≥0∞
hc : c < a * b
⊢ ∃ a' < a, c < a' * b

Tactic:
obtain ⟨a', hc, ha'⟩ := exists_between (ENNReal.div_lt_of_lt_mul hc)
  exact ⟨_, ha', (ENNReal.div_lt_iff (.inl <| by rintro rfl; simp at *)
    (.inr <| by rintro rfl; simp at *)).1 hc⟩

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

Goal state before:
pp: case refine_1
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) x < (fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) y

Tactic:
simpa only [Subtype.mk_lt_mk, ENNReal.inv_lt_inv, ENNReal.add_lt_add_iff_right one_ne_top]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rcases hf ε' hε'.1 with ⟨i, hi, H⟩

Goal state after:
case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case mpr
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
⊢ (∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ∞

Tactic:
rintro ⟨n, hn, h'n⟩

Goal state after:
case mpr
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x ∧ x < ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: m n : ℤ
x : ℝ≥0
hx : x ≠ 0
⊢ ↑x ^ (m + n) = ↑x ^ m * ↑x ^ n

Tactic:
simp only [← coe_zpow hx, zpow_add₀ hx, coe_mul]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.1 p.2 < ε} ⊆ s
ε' : ℝ
hε' : 0 < ε' ∧ ε' < ε
⊢ ∃ i, p i ∧ {p | dist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rcases hf ε' hε'.1 with ⟨i, hi, H⟩

Goal state after:
case mp
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.1 p.2 < ε} ⊆ s
ε' : ℝ
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ i, p i ∧ {p | dist p.1 p.2 ≤ f i} ⊆ s
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
⊢ ∃ a K, J * K = Ideal.span {a} ∧ I + K = ⊤

Tactic:
refine ⟨_, _, hK.symm, ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
⊢ I + K = ⊤
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
⊢ SeparableSpace X

Tactic:
refine ⟨Set.iUnion U, Set.countable_iUnion hUc, fun x => ?_⟩

Goal state after:
ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
⊢ x ∈ closure[inst✝²] (iUnion U)