mathlib-initiative/mathlib-tactics huggingface dataset:
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
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R p
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
⊢ QuasiFiniteAt A q

Tactic:
let f : A ⊗[R] Localization.AtPrime p →ₐ[A] Localization.AtPrime q :=
    Algebra.TensorProduct.lift (Algebra.ofId _ _) ⟨Localization.localRingHom _ _ _ hq, by
      simp [IsScalarTower.algebraMap_apply R S (Localization.AtPrime p),
        IsScalarTower.algebraMap_apply R (A ⊗[R] S) (Localization.AtPrime q)]⟩ fun _ _ ↦ .all _ _
  let g : A ⊗[R] S →ₐ[A] A ⊗[R] Localization.AtPrime p :=
    Algebra.TensorProduct.map (.id _ _) (IsScalarTower.toAlgHom _ _ _)
  have : f.comp g = IsScalarTower.toAlgHom _ _ _ := by ext; simp [f, g]
  replace this (x : _) : f (g x) = algebraMap _ _ x := DFunLike.congr_fun this x
  refine .of_forall_exists_mul_mem_range f fun x ↦ ?_
  obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
  refine ⟨g s, this s ▸ IsLocalization.map_units _ ⟨s, hs⟩, ?_⟩
  rw [this, IsLocalization.mk'_spec_mk]
  exact ⟨g x, this x⟩

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 σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).ker
hx : (Q.ofComp P).toAlgHom x ∈ Q.toExtension.ker
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨(Q.ofComp P).toAlgHom x, hx⟩

Tactic:
exact ⟨.mk ⟨x, hx'⟩, Extension.Cotangent.map_mk _ _⟩

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 : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ Module.Projective A Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A) ↔ ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id

Tactic:
and_comm,

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ Subsingleton (H1Cotangent R A) ∧ Module.Projective A Ω[A⁄R] ↔ ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u_4
inst✝⁸ : CommRing R
A : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallySmooth R A
inst✝ : FormallySmooth A B
⊢ FormallySmooth R B

Tactic:
refine .of_comp_surjective fun C _ _ I hI f ↦ ?_
  obtain ⟨f', e⟩ := FormallySmooth.comp_surjective _ _ I hI (f.comp (IsScalarTower.toAlgHom R A B))
  let := f'.toRingHom.toAlgebra
  obtain ⟨f'', e'⟩ := comp_surjective _ _ I hI { f with commutes' := AlgHom.congr_fun e.symm }
  apply_fun AlgHom.restrictScalars R at e'
  exact ⟨f''.restrictScalars _, e'.trans (AlgHom.ext fun _ => 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 σ
i : σ
⊢ (↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
      ((Basis.baseChange T P.cotangentSpaceBasis) i) =
    (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
      ((Basis.baseChange T P.cotangentSpaceBasis) i)

Tactic:
apply (Q.comp P).cotangentSpaceBasis.repr.injective

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 σ
i : σ
⊢ (Q.comp P).cotangentSpaceBasis.repr
      ((↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
        ((Basis.baseChange T P.cotangentSpaceBasis) i)) =
    (Q.comp P).cotangentSpaceBasis.repr
      ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        ((Basis.baseChange T P.cotangentSpaceBasis) i))
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
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
⊢ { toFun := fun x ↦ ⟨x - g (f x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } 1 = 0

Tactic:
by simp only [LinearMap.coe_mk, AddHom.coe_mk, map_one, sub_self,
    Submodule.mk_eq_zero]

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

Goal state before:
pp: case mul_X
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
p : MvPolynomial ι S
n : ι
IH :
  (δAux R Q') (f.toAlgHom p) =
    (δAux R Q) p +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p))
⊢ (δAux R Q') (f.toAlgHom (p * X n)) =
    (δAux R Q) (p * X n) +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
        (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) (p * X n)))

Tactic:
simp only [map_mul, Hom.toAlgHom_X, δAux_mul, algebraMap_apply, Hom.algebraMap_toAlgHom,
      ← @IsScalarTower.algebraMap_smul Q'.Ring T, algebraMap_self, δAux_X,
      RingHom.id_apply, coe_eval₂Hom, IH, Hom.aeval_val, smul_add, map_aeval, tmul_add, tmul_smul,
      ← @IsScalarTower.algebraMap_smul Q.Ring T, smul_zero, aeval_X, zero_add, Derivation.leibniz,
      Basis.repr_self, map_add, one_smul, map_smul, Finsupp.linearCombination_single,
      RingHomCompTriple.comp_eq, Function.comp_apply, ← cotangentSpaceBasis_apply]

Goal state after:
case mul_X
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
p : MvPolynomial ι S
n : ι
IH :
  (δAux R Q') (f.toAlgHom p) =
    (δAux R Q) p +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p))
⊢ eval₂ (algebraMap S T) (fun i ↦ Q.val i) p • (δAux R Q') (f.val n) +
      (Q.val n • (δAux R Q) p +
        Q.val n •
          (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
            (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p))) =
    Q.val n • (δAux R Q) p +
      ((aeval Q.val) p • (δAux R Q') (f.val n) +
        Q.val n •
          (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
            (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p)))
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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
l : { l // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
⊢ ↑((((AlgebraTensorModule.curry
                ↑((fun g ↦ ⟨retractionOfSectionOfKerSqZero (↑g) hf' ⋯, ⋯⟩)
                    ((fun l ↦ ⟨sectionOfRetractionKerToTensor ↑l ⋯ hf' hf, ⋯⟩) l)))
              ((algebraMap P S) s)).compDer
          (D R P))
        p) =
    ↑((((AlgebraTensorModule.curry ↑l) ((algebraMap P S) s)).compDer (D R P)) p)

Tactic:
have (x y : _) : (l.1 x).1 * (l.1 y).1 = 0 := by
      rw [← Ideal.mem_bot, ← hf', pow_two]; exact Ideal.mul_mem_mul (l.1 x).2 (l.1 y).2

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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
l : { l // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
this : ∀ (x y : S ⊗[P] Ω[P⁄R]), ↑(↑l x) * ↑(↑l y) = 0
⊢ ↑((((AlgebraTensorModule.curry
                ↑((fun g ↦ ⟨retractionOfSectionOfKerSqZero (↑g) hf' ⋯, ⋯⟩)
                    ((fun l ↦ ⟨sectionOfRetractionKerToTensor ↑l ⋯ hf' hf, ⋯⟩) l)))
              ((algebraMap P S) s)).compDer
          (D R P))
        p) =
    ↑((((AlgebraTensorModule.curry ↑l) ((algebraMap P S) s)).compDer (D R P)) p)
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_1
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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
x✝ : { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
l : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent
hl : l ∘ₗ kerCotangentToTensor R P S = LinearMap.id
y : S ⊗[P'] Ω[P'⁄R]
x : P
⊢ (↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂)).toFun ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) x • y) =
    (RingHom.id P') ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) x) • (↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂)).toFun y

Tactic:
simp only [P', ← Ideal.Quotient.algebraMap_eq, IsScalarTower.algebraMap_smul]

Goal state after:
case refine_1
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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
x✝ : { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
l : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent
hl : l ∘ₗ kerCotangentToTensor R P S = LinearMap.id
y : S ⊗[P'] Ω[P'⁄R]
x : P
⊢ (↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂)).toFun (x • y) =
    (RingHom.id (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((algebraMap P (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) x) •
      (↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂)).toFun y
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case neg
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, ⋯⟩
hb : (Basis.extend h) b = x
e : ¬a = b
⊢ x ∈ (algebraMap K L).range

Tactic:
have := DFunLike.congr_fun
      (DFunLike.congr_arg ((Basis.extend h).tensorProduct (Basis.extend h)).repr H) (a, b)

Goal state after:
case neg
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, ⋯⟩
hb : (Basis.extend h) b = x
e : ¬a = b
this :
  (((Basis.extend h).tensorProduct (Basis.extend h)).repr (1 ⊗ₜ[K] x)) (a, b) =
    (((Basis.extend h).tensorProduct (Basis.extend h)).repr (x ⊗ₜ[K] 1)) (a, b)
⊢ 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
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

Tactic:
obtain ⟨y, rfl⟩ := e.surjective b

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
x : Q.Ring ⊗[P.Ring] ↥P.ker
ha : ↑(e x) ∈ Q.ker
hx : e x = ⟨↑(e x), ha⟩
y : Q.Ring ⊗[P.Ring] ↥P.ker
⊢ ↑(e x) • e y ∈ (↑f').ker
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
hx : (Ideal.Quotient.mk (P.ker ^ 2)) x ∈ P.infinitesimal.ker
⊢ ∃ a, (map P.toInfinitesimal) a = mk ⟨(Ideal.Quotient.mk (P.ker ^ 2)) x, hx⟩

Tactic:
ker_infinitesimal,

Goal state after:
case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
hx✝ : (Ideal.Quotient.mk (P.ker ^ 2)) x ∈ P.infinitesimal.ker
hx : (Ideal.Quotient.mk (P.ker ^ 2)) x ∈ P.ker.cotangentIdeal
⊢ ∃ a, (map P.toInfinitesimal) a = mk ⟨(Ideal.Quotient.mk (P.ker ^ 2)) x, hx✝⟩
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 := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
⊢ Function.Surjective ⇑fQ

Tactic:
intro x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x
    obtain ⟨x, rfl⟩ := P.algebraMap_surjective x
    obtain ⟨s, rfl⟩ := P.algebraMap_surjective s
    refine ⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩
    simp only [fQ, IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe]
    rw [IsLocalization.lift_mk'_spec]
    simp

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)
a✝ : q ∈ Finset.univ
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
⊢ (length (Localization.AtPrime r) (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) p)).toNat *
      r.inertiaDeg R =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)

Tactic:
inertiaDeg_eq p r

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
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
⊢ (length (Localization.AtPrime r) (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) p)).toNat *
      finrank p.ResidueField r.ResidueField =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
⊢ ?m.101 =
    map (algebraMap (Localization.AtPrime q) (Localization.AtPrime r))
      (map (algebraMap R (Localization.AtPrime q)) (under R r))

Tactic:
rw [map_map, ← 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
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
x : S
a b : R
hbp : b ∉ p
c : S
hcq : c ∉ q
hc : c * (algebraMap R S) a = c * (x * (algebraMap R S) b)
d : R
hd : d ∉ p
e : S
he : (algebraMap R S) d = c * e
⊢ ∃ a, ∃ b ∉ p, (algebraMap R S) a = x * (algebraMap R S) b

Tactic:
exact ⟨d * a, d * b, ‹p.IsPrime›.mul_notMem hd hbp, by grind⟩

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
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
⊢ Function.Surjective ⇑fQ

Tactic:
intro x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x
    obtain ⟨x, rfl⟩ := P.algebraMap_surjective x
    obtain ⟨s, rfl⟩ := P.algebraMap_surjective s
    refine ⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩
    simp only [fQ, IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe]
    rw [IsLocalization.lift_mk'_spec]
    simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : Finset ι
inst✝ : DecidableEq α
hs : s.Nonempty
S : ι → Finset α
a : α
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Tactic:
convert! prod_indicator_biUnion_sub_indicator hs (fun i ↦ S i) a

Goal state after:
case a
ι : Type u_1
α : Type u_2
s : Finset ι
inst✝ : DecidableEq α
hs : s.Nonempty
S : ι → Finset α
a : α
x✝ : ι
a✝ : x✝ ∈ s
⊢ ↑(s.biUnion S) = ⋃ i ∈ s, ↑(S i)
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
⊢ sSup (s / t) = sSup s / sInf t

Tactic:
by simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v : { x // x.asIdeal ∣ I }
⊢ ∀ ⦃a₂ : { x // x.asIdeal ∣ I }⦄, (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) v = (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) a₂ → v = a₂

Tactic:
w

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
⊢ (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) v = (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) w → v = w
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
hs : ∀ x ∈ ∅, 0 ≤ x
⊢ 0 ≤ sSup ∅

pp: case inr
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
x : ℝ
hx : x ∈ s
⊢ 0 ≤ sSup s

Tactic:
· exact sSup_empty.ge

Goal state after:
case inr
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
x : ℝ
hx : x ∈ s
⊢ 0 ≤ sSup s
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 ∈ Finite.toFinset h✝, v.maxPowDividing I ≠ 0

Tactic:
rw [Finset.prod_ne_zero_iff]

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
⊢ ∀ a ∈ Finite.toFinset h✝, a.maxPowDividing I ≠ 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
p : ℝ≥0
ha : 0 ≤ r
⊢ r.toNNReal < p ↔ r < ↑p

Tactic:
← NNReal.coe_lt_coe,

Goal state after:
r : ℝ
p : ℝ≥0
ha : 0 ≤ r
⊢ ↑r.toNNReal < ↑p ↔ r < ↑p
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
rwa [Ne, inv_eq_zero]

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

Goal state before:
pp: a b : ℝ≥0
h : a < b
⊢ a / b < 1

Tactic:
by
  rwa [div_lt_iff₀ h.bot_lt, one_mul]

Goal state after: