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

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✝¹ : QuasiFinite R S
inst✝ : QuasiFinite S T
P : Ideal R
hP : P.IsPrime
this✝ : Module.Finite (P.Fiber S) (P.Fiber S ⊗[S] T)
this : Module.Finite P.ResidueField (P.Fiber S ⊗[S] T)
e : P.Fiber S ≃ₐ[S] S ⊗[R] P.ResidueField :=
  let __spread.0 := TensorProduct.comm R P.ResidueField S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Module.Finite P.ResidueField (P.Fiber T)

Tactic:
let e' : (P.Fiber S) ⊗[S] T ≃ₐ[R] P.Fiber T :=
    ((Algebra.TensorProduct.congr e .refl).restrictScalars R).trans <|
    ((Algebra.TensorProduct.comm _ _ _).restrictScalars R).trans <|
    ((Algebra.TensorProduct.cancelBaseChange _ _ T _ _).restrictScalars R).trans
    (Algebra.TensorProduct.comm _ _ _)

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
inst✝¹ : QuasiFinite R S
inst✝ : QuasiFinite S T
P : Ideal R
hP : P.IsPrime
this✝ : Module.Finite (P.Fiber S) (P.Fiber S ⊗[S] T)
this : Module.Finite P.ResidueField (P.Fiber S ⊗[S] T)
e : P.Fiber S ≃ₐ[S] S ⊗[R] P.ResidueField :=
  let __spread.0 := TensorProduct.comm R P.ResidueField S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : P.Fiber S ⊗[S] T ≃ₐ[R] P.Fiber T :=
  (AlgEquiv.restrictScalars R (TensorProduct.congr e AlgEquiv.refl)).trans
    ((AlgEquiv.restrictScalars R (TensorProduct.comm S (S ⊗[R] P.ResidueField) T)).trans
      ((AlgEquiv.restrictScalars R (TensorProduct.cancelBaseChange R S T T P.ResidueField)).trans
        (TensorProduct.comm R T P.ResidueField)))
⊢ Module.Finite P.ResidueField (P.Fiber T)
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : QuasiFinite R S
P Q : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
⊢ { asIdeal := P, isPrime := inst✝¹ } ⤳ { asIdeal := Q, isPrime := inst✝ }

Tactic:
simpa [← PrimeSpectrum.le_iff_specializes]

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

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.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
sA : ↥A := ⟨s, ⋯⟩
f : Localization.Away sA →+* T := IsLocalization.Away.lift sA ⋯
this : Algebra (Localization.Away sA) T := f.toAlgebra
⊢ QuasiFinite R T

Tactic:
let : Algebra A (Localization.Away sA) := OreLocalization.instAlgebra

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
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
sA : ↥A := ⟨s, ⋯⟩
f : Localization.Away sA →+* T := IsLocalization.Away.lift sA ⋯
this✝ : Algebra (Localization.Away sA) T := f.toAlgebra
this : Algebra (↥A) (Localization.Away sA) := OreLocalization.instAlgebra
⊢ QuasiFinite R T
Module: Mathlib.RingTheory.QuasiFinite.Basic

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.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := ⋯
sA : ↥A := ⋯
f : Localization.Away sA →+* T := ⋯
this✝⁶ : Algebra (Localization.Away sA) T := ⋯
this✝⁵ : Algebra (↥A) (Localization.Away sA) := ⋯
this✝⁴ : SMul (↥A) (Localization.Away sA) := ⋯
this✝³ : MulAction (↥A) (Localization.Away sA) := ⋯
this✝² : IsScalarTower R (↥A) (Localization.Away sA)
this✝¹ : IsScalarTower (↥A) (Localization.Away sA) T
this✝ : IsScalarTower R (Localization.Away sA) T
x : S
n : ℕ
this : IsIntegral (Localization.Away sA) ((algebraMap S T) x)
⊢ (sA • Localization.Away.invSelf sA) ^ n • (algebraMap S T) x =
    Localization.Away.invSelf sA ^ n • ((algebraMap S T) x * (algebraMap S T) s ^ n)

Tactic:
· simp only [Algebra.smul_def, map_pow, map_mul, mul_pow,
        ← IsScalarTower.algebraMap_apply, Subalgebra.algebraMap_def, sA]
      ring

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H : IsOpen {p}
⊢ QuasiFiniteAt R p.asIdeal

Tactic:
by
  have : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing R S
  have : IsJacobsonRing S := isJacobsonRing_of_finiteType (A := R)
  rw [(PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing p).out
    0 1 rfl rfl] at H
  obtain ⟨e, he, H⟩ := PrimeSpectrum.isClopen_iff.mp H
  have hep : e ∉ p.asIdeal := H.le rfl
  let f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal :=
    IsLocalization.Away.liftAlgHom e (f := Algebra.ofId _ _)
      (IsLocalization.map_units (M := p.asIdeal.primeCompl) _ ⟨e, hep⟩)
  have h₁ := (PrimeSpectrum.localization_away_comap_range (Localization.Away e) e).trans H.symm
  have : Subsingleton (PrimeSpectrum (Localization.Away e)) :=
    Function.Injective.subsingleton
    (f := Set.codRestrict (PrimeSpectrum.comap (algebraMap S (Localization.Away e))) {p} fun x ↦
      h₁.le ⟨x, rfl⟩)
    ((Set.injective_codRestrict ..).mpr (PrimeSpectrum.localization_comap_injective _ (.powers e)))
  have hf : Function.Surjective f := by
    intro x
    obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.asIdeal.primeCompl x
    suffices IsUnit (algebraMap _ (Localization.Away e) s.1) by
      refine ⟨algebraMap _ _ x * this.unit⁻¹, (this.map f).mul_right_cancel ?_⟩
      simp only [← map_mul, mul_assoc, IsUnit.val_inv_mul]
      simp
    by_contra H
    obtain ⟨M, hM, H⟩ :=
      Ideal.exists_le_maximal (.span {algebraMap _ (Localization.Away e) s.1}) (by simpa)
    have := Subsingleton.elim ((IsLocalRing.closedPoint _).comap f.toRingHom) ⟨M, inferInstance⟩
    have := congr(($this).1).ge (H (Ideal.mem_span_singleton_self _))
    simp [IsLocalRing.closedPoint, IsLocalization.AtPrime.isUnit_to_map_iff _ p.asIdeal] at this
  have : Algebra.FiniteType R (Localization.AtPrime p.asIdeal) :=
    .of_surjective (f.restrictScalars R) hf
  have := (PrimeSpectrum.comap_injective_of_surjective f.toRingHom hf).subsingleton
  exact QuasiFinite.iff_finite_comap_preimage_singleton.mpr fun _ ↦
    Set.subsingleton_of_subsingleton.finite

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
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) ⋯ ⋯
this : ∀ r ∈ P₁.ker, lift r ∈ P₂.infinitesimal.ker
r : P₁.Ring
hr : r ∈ P₁.ker
⊢ ∀ s ∈ P₁.ker, r * s ∈ RingHom.ker lift

Tactic:
s

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) ⋯ ⋯
this : ∀ r ∈ P₁.ker, lift r ∈ P₂.infinitesimal.ker
r : P₁.Ring
hr : r ∈ P₁.ker
s : P₁.Ring
⊢ s ∈ P₁.ker → r * s ∈ RingHom.ker lift
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
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
⊢ TensorProduct.AlgebraTensorModule.lift (↑R (lsmul S S M).toLinearMap.flip).flip ∘ₗ sec R S M = LinearMap.id

Tactic:
ext x
  simp only [sec, LinearMap.coe_comp, LinearMap.coe_mk, LinearMap.coe_toAddHom,
    Function.comp_apply, LinearMap.flip_apply, TensorProduct.AlgebraTensorModule.mapBilinear_apply,
    TensorProduct.AlgebraTensorModule.lift_apply, LinearMap.id_coe, id_eq]
  trans (TensorProduct.lmul' R (elem R S)) • x
  · induction elem R S using TensorProduct.induction_on with
    | zero => simp
    | tmul r s => simp [mul_smul, smul_comm r s]
    | add y z hy hz => simp [hy, hz, add_smul]
  · rw [lmul_elem, one_smul]

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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
⊢ ∀ (y : S) (z : ↥(RingHom.ker (algebraMap P S))), (p • y) • z = p • y • z

Tactic:
s

Goal state after:
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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
⊢ ∀ (z : ↥(RingHom.ker (algebraMap P S))), (p • s) • z = p • s • z
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
⊢ Function.Bijective ⇑(algebraMap K A)

Tactic:
have := finite_of_free (R := K) (S := A)

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this : Module.Finite K A
⊢ Function.Bijective ⇑(algebraMap K A)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case e_f
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
r : A
⊢ ∀ (y : A ⧸ IsLocalRing.maximalIdeal A),
    (↑K ((ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap)) (r ⊗ₜ[K] y) =
      (↑K
          (TensorProduct.AlgebraTensorModule.lift
            (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip))
        (r ⊗ₜ[K] y)

Tactic:
s

Goal state after:
case e_f
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
r : A
s : A ⧸ IsLocalRing.maximalIdeal A
⊢ (↑K ((ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap)) (r ⊗ₜ[K] s) =
    (↑K
        (TensorProduct.AlgebraTensorModule.lift
          (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip))
      (r ⊗ₜ[K] s)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : ⇑f = ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap)
⊢ Function.Injective
    ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap)

Tactic:
suffices Function.Injective
        (LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap) by
      exact this.comp (Algebra.TensorProduct.lid K A).symm.injective

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : ⇑f = ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap)
⊢ Function.Injective ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case pos
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 ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L := h.extend ⋯
a : ↑S := ⟨1, ⋯⟩
ha : (Basis.extend h) a = 1
⊢ x ∈ (algebraMap K L).range

Tactic:
let b : S := ⟨x, h.subset_extend _ (by simp)⟩

Goal state after:
case pos
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 ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L := h.extend ⋯
a : ↑S := ⟨1, ⋯⟩
ha : (Basis.extend h) a = 1
b : ↑S := ⟨x, ⋯⟩
⊢ x ∈ (algebraMap K L).range
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
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
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
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
ha : a ∈ Q.ker
b : ↥Q.ker
x : Q.Ring ⊗[P.Ring] ↥P.ker
hx : e x = ⟨a, ha⟩
⊢ a • b ∈ (↑f').ker

Tactic:
obtain rfl : (e x).1 = a := congr_arg Subtype.val hx

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
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
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
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
b : ↥Q.ker
x : Q.Ring ⊗[P.Ring] ↥P.ker
ha : ↑(e x) ∈ Q.ker
hx : e x = ⟨↑(e x), ha⟩
⊢ ↑(e x) • b ∈ (↑f').ker
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case e'_4
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ ↑(equiv W (Q.comp P)) ∘ₗ LinearMap.liftBaseChange T (Extension.H1Cotangent.map g.toExtensionHom) =
    LinearMap.liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)

Tactic:
change Extension.H1Cotangent.map (W.defaultHom (Q.comp P)).toExtensionHom ∘ₗ _ = _
    rw [LinearMap.liftBaseChange_comp, ← Extension.H1Cotangent.map_comp,
      Extension.H1Cotangent.map_eq]

Goal state after:
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
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
have : IsScalarTower R Sq Sq' := IsScalarTower.of_algHom f.toAlgHom

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
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
⊢ (g • q).ramificationIdx R = q.ramificationIdx R
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
⊢ ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε

Tactic:
intro j ij k ik

Goal state after:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
k : ℕ
ik : k ≥ ⌈ε⁻¹⌉₊
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
⊢ a ≤ y

Tactic:
have hx : x ≠ 0 := ha.ne_zero

Goal state after:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ a ≤ y
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a b : ℝ≥0∞
h : a = ∞ → b = ∞
h_nnreal : a ≠ ∞ → b ≠ ∞ → a.toNNReal ≤ b.toNNReal
⊢ a ≤ b

Tactic:
by_contra! hlt

Goal state after:
a b : ℝ≥0∞
h : a = ∞ → b = ∞
h_nnreal : a ≠ ∞ → b ≠ ∞ → a.toNNReal ≤ b.toNNReal
hlt : b < a
⊢ False
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✝ : Group E
p q f g : GroupNorm E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _, _, _⟩, _⟩ := f

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : Group E
p q g : GroupNorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
eq_one_of_map_eq_zero'✝ :
  ∀ (x : E), { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }.toFun x = 0 → x = 1
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ } =
    g
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x : α
hx₁ : x ∈ s.ordT5Nhd t
hx₂ : x ∈ t.ordT5Nhd s
⊢ x ∈ ⊥

Tactic:
rcases mem_iUnion₂.1 hx₁ with ⟨a, has, ha⟩

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x : α
hx₁ : x ∈ s.ordT5Nhd t
hx₂ : x ∈ t.ordT5Nhd s
a : α
has : a ∈ s
ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a
⊢ x ∈ ⊥
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
κ : Sort u_2
q₁ : ι → Sort u_3
q₂ : κ → Sort u_4
f : (i : ι) → q₁ i → ℝ≥0∞
g : (k : κ) → q₂ k → ℝ≥0∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk

Tactic:
iInf₂_add,

Goal state after:
ι : Sort u_1
a : ℝ≥0∞
κ : Sort u_2
q₁ : ι → Sort u_3
q₂ : κ → Sort u_4
f : (i : ι) → q₁ i → ℝ≥0∞
g : (k : κ) → q₂ k → ℝ≥0∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ ⨅ i, ⨅ j, f i j + ⨅ k, ⨅ qk, g k qk
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ ↑x = 0 ↔ x = 0

Tactic:
by
  rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_zero]

Goal state after: