mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : P = ⊥
⊢ p.ramificationIdx' 0 = 0

Tactic:
exact Ideal.ramificationIdx'_of_not_le (mt le_bot_iff.mp hp)

Goal state after:
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:
ext1

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₁ = ↑f₂
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
⊢ Module.Finite P.ResidueField (P.Fiber T)

Tactic:
have : Module.Finite (P.Fiber S) ((P.Fiber S) ⊗[S] T) :=
    iff_of_isArtinianRing.mp inferInstance

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)
⊢ 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
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
this✝⁵ : IsLocalizedModule p.primeCompl LinearMap.id
this✝⁴ : Module.Finite R (Localization.AtPrime p)
this✝³ : Module.Finite S (Localization.AtPrime p)
this✝² : IsArtinianRing (Localization.AtPrime p)
this✝¹ : IsNoetherianRing S
this✝ : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
hrq :
  PrimeSpectrum.comap (algebraMap S (Localization.Away r))
      ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    ↑(PrimeSpectrum.basicOpen r)
⊢ PrimeSpectrum.comap (algebraMap S (Localization.Away r))
      ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    {{ asIdeal := p, isPrime := inst✝³ }}

Tactic:
ext1

Goal state after:
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✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
this✝⁵ : IsLocalizedModule p.primeCompl LinearMap.id
this✝⁴ : Module.Finite R (Localization.AtPrime p)
this✝³ : Module.Finite S (Localization.AtPrime p)
this✝² : IsArtinianRing (Localization.AtPrime p)
this✝¹ : IsNoetherianRing S
this✝ : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p := ⋯
hrq :
  PrimeSpectrum.comap (algebraMap S (Localization.Away r))
      ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    ↑(PrimeSpectrum.basicOpen r)
⊢ (PrimeSpectrum.comap (algebraMap S (Localization.Away r))
        ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p)))).asIdeal =
    { asIdeal := p, isPrime := inst✝³ }.asIdeal
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
inst✝ : FormallySmooth R P.Ring
r : P.Ring
m : P.ker.Cotangent
⊢ (AddEquiv.refl P.ker.Cotangent).toFun (r • m) = (RingHom.id P.Ring) r • (AddEquiv.refl P.ker.Cotangent).toFun m

Tactic:
ext1

Goal state after:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
r : P.Ring
m : P.ker.Cotangent
⊢ Cotangent.val ((AddEquiv.refl P.ker.Cotangent).toFun (r • m)) =
    ((RingHom.id P.Ring) r • (AddEquiv.refl P.ker.Cotangent).toFun m).val
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
f : P →ₐ[R] A
hf : Function.Surjective ⇑f
this : Algebra P A := f.toAlgebra
⊢ FormallySmooth R A ↔ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
iff_split_injection hf,

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
f : P →ₐ[R] A
hf : Function.Surjective ⇑f
this : Algebra P A := f.toAlgebra
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A
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
⊢ FormallyUnramified K L

Tactic:
rw [iff_comp_injective]
  intro B _ _ I hI f₁ f₂ e
  ext x
  have : f₁ x - f₂ x ∈ I := by
    simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun e x
  have := Polynomial.eval_add_of_sq_eq_zero ((minpoly K x).map (algebraMap K B)) (f₂ x)
    (f₁ x - f₂ x) (show (f₁ x - f₂ x) ^ 2 ∈ ⊥ from hI ▸ Ideal.pow_mem_pow this 2)
  simp only [add_sub_cancel, eval_map_algebraMap, aeval_algHom_apply, minpoly.aeval, map_zero,
    derivative_map, zero_add] at this
  rwa [eq_comm, ((isUnit_iff_ne_zero.mpr
    ((Algebra.IsSeparable.isSeparable K x).aeval_derivative_ne_zero
      (minpoly.aeval K x))).map f₂).mul_right_eq_zero, sub_eq_zero] at this

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

Goal state before:
pp: case mul_X.inr
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
p : MvPolynomial (ι ⊕ σ) R
IH :
  (δAux R Q) ((Q.ofComp P).toAlgHom p) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2
n : σ
⊢ eval₂ (algebraMap R T) (fun i ↦ Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) i) p •
        (δAux R Q) (Sum.elim X (⇑C ∘ P.val) (Sum.inr n)) +
      (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) (Sum.inr n)) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2 =
    (aeval (Q.comp P).val) p •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) ((Q.comp P).cotangentSpaceBasis (Sum.inr n))).2 +
      Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) (Sum.inr n) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2

Tactic:
simp only [Sum.elim_inr, Function.comp_apply, algHom_C, δAux_C,
        CotangentSpace.compEquiv, LinearEquiv.trans_apply, Basis.repr_symm_apply,
        algebraMap_smul, Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply,
        LinearMap.coe_inr, Basis.baseChange_apply, one_smul, LinearMap.baseChange_tmul,
        toKaehler_cotangentSpaceBasis, add_left_inj, LinearMap.coe_inl]
      rfl

Goal state after:
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
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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
⊢ (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) 1 - (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) (f 1) = 0

Tactic:
map_one,

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
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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
⊢ 1 - (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) (f 1) = 0
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
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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
hf₄ : f 1 = 1
x : A
k : K
| k • f (e 1)

Tactic:
map_one,

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
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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
hf₄ : f 1 = 1
x : A
k : K
| k • f 1
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
s : S
⊢ (tensorKaehlerEquivOfFormallyEtale R S T).symm ((D R T) ((algebraMap S T) s)) = 1 ⊗ₜ[S] (D R S) s

Tactic:
by
  rw [LinearEquiv.symm_apply_eq, tensorKaehlerEquivOfFormallyEtale_apply, mapBaseChange_tmul,
    one_smul, map_D]

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
P : Extension R S
Q : Extension R T
f : P.Hom Q
H : f.toRingHom.FormallyEtale
this✝⁴ : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this✝³ : IsScalarTower R P.Ring Q.Ring
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
this : FormallyEtale P.Ring Q.Ring
⊢ Ω[Q.Ring⁄R] →ₗ[Q.Ring] T ⊗[S] P.CotangentSpace

Tactic:
by
      refine LinearMap.liftBaseChange _ ?_ ∘ₗ
        (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm.toLinearMap
      exact (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring ∘ₗ
        (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring

Goal state after:
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
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝³ : FiniteType K A
this✝² : Module.Finite K (Localization.AtPrime Q)
this✝¹ : IsField (Localization.AtPrime Q)
this✝ : Field (Localization.AtPrime Q) := this✝¹.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
⊢ ¬q ^ 2 ∣ p

Tactic:
obtain ⟨⟨m, hm⟩, hm'⟩ := (IsLocalization.map_eq_zero_iff Q.primeCompl _ _).mp this

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝³ : FiniteType K A
this✝² : Module.Finite K (Localization.AtPrime Q)
this✝¹ : IsField (Localization.AtPrime Q)
this✝ : Field (Localization.AtPrime Q) := this✝¹.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : A
hm : m ∈ Q.primeCompl
hm' : ↑⟨m, hm⟩ * (aeval x) q = 0
⊢ ¬q ^ 2 ∣ p
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case left
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x y : P.H1Cotangent
e : (map P.toInfinitesimal) x = (map P.toInfinitesimal) y
⊢ x = y

Tactic:
ext1

Goal state after:
case left
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x y : P.H1Cotangent
e : (map P.toInfinitesimal) x = (map P.toInfinitesimal) y
⊢ ↑x = ↑y
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 ⋯
x : T
⊢ ∃ a, fQ a = x

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ M
⊢ ∃ a, fQ a = IsLocalization.mk' T x ⟨s, hs⟩
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 ⋯
x : T
⊢ ∃ a, fQ a = x

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
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 ⋯
x s : S
hs : s ∈ M
⊢ ∃ a, fQ a = IsLocalization.mk' T x ⟨s, hs⟩
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a = ∑ a, f a - ∑ a ∈ s.biUnion S, f a

Tactic:
by
      rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]

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

Goal state before:
pp: n : ℕ
⊢ ↑(↑n).toNNReal = ↑↑n

Tactic:
by simp [Real.coe_toNNReal]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ ⨆ i, f i = 0

Tactic:
dsimp [iSup]
  convert! Real.sSup_empty
  rw [Set.range_eq_empty_iff]
  infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
⊢ ¬v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
      v.maxPowDividing I * ∏ i ∈ (Finite.toFinset hf).erase v, i.maxPowDividing I

Tactic:
intro h_contr

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ (Finite.toFinset hf).erase v, i.maxPowDividing I
⊢ False
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
⊢ ∀ a ∈ Finite.toFinset h✝, a.maxPowDividing I ≠ 0

Tactic:
intro v _

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.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors ∣
    ∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors
h_not_dvd :
  ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors

Tactic:
rw [← Associates.mk_dvd_mk] at h_dvd h_not_dvd

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  Associates.mk (v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ∣
    Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)
h_not_dvd :
  ¬Associates.mk (v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1)) ∣
      Associates.mk
        (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal

Tactic:
div_eq_inv_mul,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ (y⁻¹ * x).toNNReal = x.toNNReal / y.toNNReal
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ (y⁻¹ * x).toNNReal = x.toNNReal / y.toNNReal

Tactic:
div_eq_inv_mul,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ (y⁻¹ * x).toNNReal = y.toNNReal⁻¹ * x.toNNReal
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ x ∈ ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I → x ∈ ⨅ i, i.maxPowDividing I

Tactic:
· simp only [Finite.mem_toFinset, mem_mulSupport, one_eq_top, ne_eq, Submodule.mem_iInf]
      intro h i
      by_cases i.maxPowDividing I = ⊤ <;> simp_all

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

Goal state before:
pp: case neg
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
⊢ f ↑g⁻¹ < 1

Tactic:
· have hfg0 : f g ≠ 0 :=
        fun h0 ↦ (Units.ne_zero g) ((map_eq_zero f).mp h0)
      have hg1' : 1 < g := lt_of_le_of_ne (not_lt.mp hu1) hg1.symm
      rw [Units.val_inv_eq_inv_val, map_inv₀, inv_lt_one_iff hfg0, ← map_one f]
      exact hf hg1'

Goal state after: