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

Goal state before:
pp: case hfg
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := ⋯
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (a i).support, ((a i) x_1 • f i) ⊗ₜ[R] b x_1 = ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1

Tactic:
exact fun _ _ ↦ rfl

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
s : S
t : P
⊢ ↑((retractionOfSectionOfKerSqZero g hf' hg) (s ⊗ₜ[P] (D R P) t)) = g s * t - g s * g ((algebraMap P S) t)

Tactic:
let := g.toRingHom.toAlgebra
  have := isScalarTower_of_section_of_ker_sqZero g hf' hg
  simp only [retractionOfSectionOfKerSqZero, LinearMap.coe_restrictScalars,
    LinearMap.liftBaseChange_tmul, SetLike.val_smul_of_tower]
  -- The issue is a mismatch between `RingHom.ker (algebraMap P S)` and
  -- `RingHom.ker (IsScalarTower.toAlgHom R P S)`, but `rw` and `simp` can't rewrite it away...
  erw [Derivation.liftKaehlerDifferential_comp_D]
  exact mul_sub (g s) t (g (algebraMap P S t))

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
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
hf₄ : f 1 = 1
x : A
k : K
| (⇑f ∘ ⇑e) k

Tactic:
← mul_one k,

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
| (⇑f ∘ ⇑e) (k * 1)
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
⊢ x = 0

Tactic:
have : Function.Injective f := by
    have : ⇑f = (LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap).comp
        (Algebra.TensorProduct.lid K A).symm.toLinearMap := by
      ext x; simp [f]
    rw [this]
    suffices Function.Injective
        (LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap) by
      exact this.comp (Algebra.TensorProduct.lid K A).symm.injective
    apply Module.Flat.rTensor_preserves_injective_linearMap
    exact (algebraMap K _).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 : Function.Injective ⇑f
⊢ x = 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
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
⊢ ∀ (x_1 : M.IsMaximal), (algebraMap (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)) (f x) = 0

Tactic:
hM

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 : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
⊢ (algebraMap (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)) (f x) = 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
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this✝² : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this✝¹ : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝ : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
⊢ y = 0

Tactic:
have := comp (AlgebraicClosure K) (AlgebraicClosure K ⊗[K] A)
    (Localization.AtPrime M)

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✝³ : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this✝² : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝¹ : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝ : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
this : FormallyUnramified (AlgebraicClosure K) (Localization.AtPrime M)
⊢ y = 0
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring :=
  { smul := map_toInfinitesimal_bijective._aux_1_1 P, algebraMap := map_toInfinitesimal_bijective._aux_1_3 P,
    commutes' := ⋯, smul_def' := ⋯ }
this : IsScalarTower P.Ring P.infinitesimal.Ring S
x : S
a : P.Ring
⊢ x ⊗ₜ[P.infinitesimal.Ring] (D R P.infinitesimal.Ring) (P.toInfinitesimal.toRingHom a) =
    (↑P.Ring ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm) (x ⊗ₜ[P.Ring] (D R P.Ring) a)

Tactic:
exact (tensorKaehlerQuotKerSqEquiv_symm_tmul_D _ _).symm

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
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
by
  let mR := (maximalIdeal R).map (algebraMap R S)
  have hmR : mR ≤ maximalIdeal S := ((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp ‹_›
  let : Algebra (ResidueField R) (S ⧸ mR) := (inferInstanceAs <| Algebra (R ⧸ _) _)
  have : IsScalarTower R (ResidueField R) (S ⧸ mR) := (inferInstanceAs <| IsScalarTower R (R ⧸ _) _)
  have : FormallyUnramified (ResidueField R) (S ⧸ mR) := .of_restrictScalars R _ _
  have : EssFiniteType (ResidueField R) (S ⧸ mR) := .of_comp R _ _
  have : Module.Finite (ResidueField R) (S ⧸ mR) := FormallyUnramified.finite_of_free _ _
  have : IsReduced (S ⧸ mR) := FormallyUnramified.isReduced_of_field (ResidueField R) (S ⧸ mR)
  have : IsArtinianRing (S ⧸ mR) := isArtinian_of_tower (ResidueField R) inferInstance
  have : Nontrivial (S ⧸ mR) :=
    Ideal.Quotient.nontrivial_iff.mpr <| ne_top_of_le_ne_top (maximalIdeal.isMaximal S).ne_top hmR
  have : IsLocalRing (S ⧸ mR) := .of_surjective' _ Ideal.Quotient.mk_surjective
  have : maximalIdeal (S ⧸ mR) = ⊥ := by
    rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
      ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]
  rwa [← isField_iff_maximalIdeal_eq] at this

Goal state after:
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
⊢ Surjective ⇑(map P.toInfinitesimal)

Tactic:
intro x
    obtain ⟨⟨x, hx⟩, rfl⟩ := Cotangent.mk_surjective x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    rw [ker_infinitesimal, Ideal.mk_mem_cotangentIdeal] at hx
    exact ⟨.mk ⟨x, hx⟩, rfl⟩

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
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ IsUnramifiedAt R q ↔ FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)

pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q) ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Tactic:
· exact ⟨fun _ ↦ .of_restrictScalars R _ _,
      fun _ ↦ Algebra.FormallyUnramified.comp _ (Localization.AtPrime p) _⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q) ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)
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 ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x s : P.Ring
hs : s ∈ M'
⊢ (algebraMap P.Ring (Localization M')) x =
    ↑⟨s, hs⟩ • IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩

Tactic:
← Submonoid.smul_def,

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 ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x s : P.Ring
hs : s ∈ M'
⊢ (algebraMap P.Ring (Localization M')) x =
    ⟨s, hs⟩ • IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩
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 = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
H : (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))).range ≤ (awayMapₐ (Algebra.ofId R S) r').range
x : Away ((algebraMap R S) r')
⊢ ∃ a, (awayMap (algebraMap R S) r') a = x

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers (algebraMap R S r')) x

Goal state after:
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 = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
H : (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))).range ≤ (awayMapₐ (Algebra.ofId R S) r').range
x : S
n : ℕ
⊢ ∃ a,
    (awayMap (algebraMap R S) r') a =
      IsLocalization.mk' (Away ((algebraMap R S) r')) x ⟨(fun x ↦ (algebraMap R S) r' ^ x) n, ⋯⟩
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
⊢ x ∈ ⨆ i, torsionBySet A M ↑(I ^ i) → ∃ n, ∀ a ∈ I ^ n, a • x = 0

Tactic:
intro a
    rw [Submodule.mem_iSup_of_directed] at a
    · simpa using a
    · intro x y
      use max x y
      simp [torsionBySet_le_torsionBySet_pow]

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a - ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a = 0

Tactic:
calc
    Set.indicator (⋃ i ∈ s, S i) f a - ∑ t ∈ s.powerset with t.Nonempty,
      (-1) ^ (#t + 1) • Set.indicator (⋂ i ∈ t.1, S i) f a
    _ = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ #t • Set.indicator (⋂ i ∈ t, S i) f a +
        ∑ t ∈ s.powerset with ¬ t.Nonempty, (-1) ^ #t • Set.indicator (⋂ i ∈ t, S i) f a := by
      simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ, ha]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t • Set.indicator (⋂ i ∈ t, S i) f a := by
      rw [sum_filter_add_sum_filter_not]
    _ = (∏ i ∈ s, (1 - Set.indicator (S i) 1 a : ℤ)) • f a := by
      simp only [Int.reduceNeg, prod_sub, prod_const_one, mul_one, sum_smul]
      congr! 1 with t
      simp only [prod_const_one, prod_indicator_apply]
      simp [Set.indicator]
    _ = 0 := by
      have : Set.indicator (⋃ i ∈ s, S i) 1 a = (1 : ℤ) := Set.indicator_of_mem ha 1
      rw [← this, prod_indicator_biUnion_sub_indicator, zero_smul]
      simp only [Set.mem_iUnion, exists_prop] at ha
      rcases ha with ⟨i, hi, -⟩
      exact ⟨i, hi⟩

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

Goal state before:
pp: 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
I : Ideal R
hI : I ≠ 0
⊢ HasFiniteMulSupport fun v ↦ ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)

Tactic:
by
  rw [HasFiniteMulSupport, mulSupport]
  simp_rw [Ne, zpow_natCast, ← FractionalIdeal.coeIdeal_pow, FractionalIdeal.coeIdeal_eq_one]
  exact hasFiniteMulSupport hI

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

Goal state before:
pp: case refine_2
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε

Tactic:
· rcases H _ (neg_lt_zero.mpr ε_pos) with ⟨x, x_in, hx⟩
    exact sub_lt_iff_lt_add.mp (lt_csSup_of_lt h x_in hx)

Goal state after:
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✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
h0 : spanSingleton R⁰ (mk' K n d) ≠ 0
⊢ spanSingleton R⁰ (mk' K n d) = spanSingleton R⁰ ((algebraMap R K) ↑d)⁻¹ * ↑(Ideal.span {n})

Tactic:
rw [coeIdeal_span_singleton, spanSingleton_mul_spanSingleton]

Goal state after:
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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
h0 : spanSingleton R⁰ (mk' K n d) ≠ 0
⊢ spanSingleton R⁰ (mk' K n d) = spanSingleton R⁰ (((algebraMap R K) ↑d)⁻¹ * (algebraMap R K) n)
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p : ℝ
n : ℕ
hn : n ≠ 0
⊢ ENNReal.ofReal p < ↑n ↔ p < ↑n

Tactic:
by
  exact mod_cast ofReal_lt_ofReal_iff (Nat.cast_pos.2 hn.bot_lt)

Goal state after:
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✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max 1 (if y = 0 then 0 else 1)

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
x : ℝ≥0∞
hx : ⊥ < x
⊢ a - f i < x

Tactic:
by simpa [hi.le, tsub_eq_zero_of_le]

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

Goal state before:
pp: case mp
x : ℝ
⊢ x ∈ toReal '' Ioo 0 ⊤ → x ∈ Ioi 0

pp: case mpr
x : ℝ
⊢ x ∈ Ioi 0 → x ∈ toReal '' Ioo 0 ⊤

Tactic:
· rintro ⟨y, ⟨hy0, _⟩, rfl⟩
    lift y to ℝ using by aesop
    simpa using hy0

Goal state after:
case mpr
x : ℝ
⊢ x ∈ Ioi 0 → x ∈ toReal '' Ioo 0 ⊤
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case h0
a b : ℝ≥0∞
⊢ b ≠ 0 ∨ 1 ≠ 0

Tactic:
right

Goal state after:
case h0
a b : ℝ≥0∞
⊢ 1 ≠ 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ht
a b : ℝ≥0∞
⊢ b ≠ ∞ ∨ 1 ≠ ∞

Tactic:
right

Goal state after:
case ht
a b : ℝ≥0∞
⊢ 1 ≠ ∞
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: 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
exps : HeightOneSpectrum R → ℤ
⊢ count K v (∏ᶠ (w : HeightOneSpectrum R) (_ : w ≠ v), ↑w.asIdeal ^ exps w) = 0

Tactic:
by
  apply finprod_mem_induction fun I => count K v I = 0
  · exact count_one K v
  · intro I I' hI hI'
    classical
    by_cases h : I ≠ 0 ∧ I' ≠ 0
    · rw [count_mul' K v, if_pos h, hI, hI', add_zero]
    · rw [count_mul' K v, if_neg h]
  · intro w hw
    rw [count_zpow, count_maximal_coprime K v hw, mul_zero]

Goal state after: