mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
I : Ideal S
hI : p ∣ ↑(absNorm I)
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I

Tactic:
have : IsAddTorsionFree S := .of_isTorsionFree ℤ _

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
I : Ideal S
hI : p ∣ ↑(absNorm I)
this : IsAddTorsionFree S
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
hJ : J ∈ {I | absNorm I = n}
h : f I = f J
⊢ comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) I) =
    comap (Quotient.mk (span {↑(absNorm J)})) (map (Quotient.mk (span {↑(absNorm J)})) J)

Tactic:
← hJ.symm

Goal state after:
case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
hJ : J ∈ {I | absNorm I = n}
h : f I = f J
⊢ comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) I) =
    comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) J)
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst✝] Z
H' : ((closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ¬(closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ (Z ∩ closedPoints X) = ∅
⊢ False

Tactic:
← Set.disjoint_iff_inter_eq_empty,

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst✝] Z
H' : ((closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ¬Disjoint (closure[inst✝] (Z ∩ closedPoints X))ᶜ (Z ∩ closedPoints X)
⊢ False
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this :
  ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B (B ⊗[A] M) = length B ↥⊤

Tactic:
length_top

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this :
  ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B (B ⊗[A] M) = length B (B ⊗[A] M)
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
g₁ g₂ : A →ₐ[R] B
h : (Ideal.Quotient.mkₐ R I).comp g₁ = (Ideal.Quotient.mkₐ R I).comp g₂
⊢ g₁ = g₂

Tactic:
by
  revert g₁ g₂
  change Function.Injective (Ideal.Quotient.mkₐ R I).comp
  revert ‹Algebra R B›
  apply Ideal.IsNilpotent.induction_on (S := B) I hI
  · intro B _ I hI _; exact FormallyUnramified.comp_injective I hI
  · intro B _ I J hIJ h₁ h₂ _ g₁ g₂ e
    apply h₁
    apply h₂
    ext x
    replace e := AlgHom.congr_fun e x
    dsimp only [AlgHom.comp_apply, Ideal.Quotient.mkₐ_eq_mk] at e ⊢
    rwa [Ideal.Quotient.eq, ← map_sub, Ideal.mem_quotient_iff_mem hIJ, ← Ideal.Quotient.eq]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
t : S ⊗[R] S
⊢ (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S

Tactic:
simp only [KaehlerDifferential.ideal, RingHom.mem_ker, map_sub, map_one,
      sub_eq_zero, @eq_comm S 1]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ f₁ (f x) = f₂ (f x)

Tactic:
rw [← AlgHom.comp_apply, ← AlgHom.comp_apply]

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ (f₁.comp f) x = (f₂.comp f) x
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
⊢ FormallyUnramified R B

Tactic:
rw [iff_comp_injective]
  intro Q _ _ I hI f₁ f₂ e
  ext x
  obtain ⟨x, rfl⟩ := H x
  rw [← AlgHom.comp_apply, ← AlgHom.comp_apply]
  congr 1
  apply FormallyUnramified.comp_injective I hI
  ext x; exact DFunLike.congr_fun e (f x)

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
⊢ FormallyUnramified B (B ⊗[R] A)

Tactic:
by
  rw [iff_comp_injective]
  intro C _ _ I hI f₁ f₂ e
  let := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
  have : IsScalarTower R B C := IsScalarTower.of_algebraMap_eq' rfl
  ext : 1
  exact FormallyUnramified.ext I ⟨2, hI⟩ fun x => AlgHom.congr_fun e (1 ⊗ₜ x)

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✝ : QuasiFinite R S
f : S →ₐ[R] T
H : ∀ (x : T), ∃ s, IsUnit (f s) ∧ x * f s ∈ f.range
⊢ ∀ (y : ↥(Submonoid.comap f (IsUnit.submonoid T))), IsUnit (f ↑y)

Tactic:
simp [IsUnit.mem_submonoid_iff]

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
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
| (Ideal.quotientKerAlgEquivOfSurjective hg).symm (f x)

Tactic:
← AlgEquiv.coe_toAlgHom,

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_1
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
| ↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm (f x)
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 : σ
j : ι ⊕ σ
⊢ ((Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)).repr (0, 1 ⊗ₜ[S] P.cotangentSpaceBasis i))
      j =
    (aeval (Q.comp P).val) (Pi.single j 1 (Sum.inr i))

Tactic:
obtain (j | j) := j

Goal state after:
case inl
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 : σ
j : ι
⊢ ((Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)).repr (0, 1 ⊗ₜ[S] P.cotangentSpaceBasis i))
      (Sum.inl j) =
    (aeval (Q.comp P).val) (Pi.single (Sum.inl j) 1 (Sum.inr i))

case 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 σ
i j : σ
⊢ ((Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)).repr (0, 1 ⊗ₜ[S] P.cotangentSpaceBasis i))
      (Sum.inr j) =
    (aeval (Q.comp P).val) (Pi.single (Sum.inr j) 1 (Sum.inr i))
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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
x : Q.Ring
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
⊢ (δAux R Q') (f.toAlgHom x) =
    (δAux R Q) x +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x))

Tactic:
induction x using MvPolynomial.induction_on with
  | C s => simp [MvPolynomial.algebraMap_eq, δAux_C]
  | add x₁ x₂ hx₁ hx₂ =>
    simp only [map_add, hx₁, hx₂, tmul_add]
    rw [add_add_add_comm]
  | mul_X p n IH =>
    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]
    rw [add_left_comm]
    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
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)
n : ℕ
hn : IsLocalRing.maximalIdeal A ^ n = 0
⊢ f 1 = 1

Tactic:
have : (1 - f 1) ^ n = 0 := by
      rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hn]
      exact Ideal.pow_mem_pow hf₂ n

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
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)
n : ℕ
hn : IsLocalRing.maximalIdeal A ^ n = 0
this : (1 - f 1) ^ n = 0
⊢ f 1 = 1
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁶ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
inst✝³ : q.IsPrime
inst✝² : Algebra.EssFiniteType R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : PerfectField (under R q).ResidueField
h : (map (algebraMap R (Localization.AtPrime q)) (under R q)).IsMaximal
⊢ Algebra.IsUnramifiedAt R q

Tactic:
IsLocalRing.isMaximal_iff

Goal state after:
S : Type u_1
inst✝⁶ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
inst✝³ : q.IsPrime
inst✝² : Algebra.EssFiniteType R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : PerfectField (under R q).ResidueField
h : map (algebraMap R (Localization.AtPrime q)) (under R q) = IsLocalRing.maximalIdeal (Localization.AtPrime q)
⊢ Algebra.IsUnramifiedAt R q
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case right
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
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
a : T ⊗[S] P.H1Cotangent
ha : (LinearMap.baseChange T h1Cotangentι) a = (tensorCotangent f halg H₂).symm ↑x
⊢ ∃ a, (LinearMap.liftBaseChange T (H1Cotangent.map f)) a = x

Tactic:
refine ⟨a, Subtype.ext (.trans ?_ ((LinearEquiv.eq_symm_apply _).mp ha))⟩

Goal state after:
case right
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
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
a : T ⊗[S] P.H1Cotangent
ha : (LinearMap.baseChange T h1Cotangentι) a = (tensorCotangent f halg H₂).symm ↑x
⊢ ↑((LinearMap.liftBaseChange T (H1Cotangent.map f)) a) =
    (tensorCotangent f halg H₂) ((LinearMap.baseChange T h1Cotangentι) a)
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h : map (algebraMap R (Localization.AtPrime q)) p = map (algebraMap S (Localization.AtPrime q)) q ^ p.ramificationIdx' q
⊢ p.ramificationIdx' q = q.ramificationIdx R

Tactic:
AtPrime.map_eq_maximalIdeal

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h :
  map (algebraMap R (Localization.AtPrime q)) p =
    IsLocalRing.maximalIdeal (Localization q.primeCompl) ^ p.ramificationIdx' q
⊢ p.ramificationIdx' q = 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
⊢ ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)

Tactic:
intro n n0 y yS

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
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
⊢ y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
⊢ ↑(sInf ∅) = sInf (toReal '' ∅)

Tactic:
simp only [Set.image_empty, Real.sInf_empty, coe_eq_zero]
    exact @subset_sInf_emptyset ℝ (Set.Ici (0 : ℝ)) _ _ (_)

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

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

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

Tactic:
· exact sInf_empty.le

Goal state after:
case inr
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
x : ℝ
hx : x ∈ s
⊢ sInf s ≤ 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ r.toNNReal ≤ 1 ↔ r ≤ 1

Tactic:
by
  simpa using toNNReal_le_toNNReal_iff zero_le_one

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

Goal state before:
pp: Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ
hr : 0 < r
⊢ ∃ d, ↑(f ↑d) < r

Tactic:
set s : NNReal := ⟨r, le_of_lt hr⟩

Goal state after:
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ
hr : 0 < r
s : ℝ≥0 := ⟨r, ⋯⟩
⊢ ∃ d, ↑(f ↑d) < r
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: ⊢ ENNReal.ofReal 0 = 0

Tactic:
by simp [ENNReal.ofReal]

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

Goal state before:
pp: ⊢ ENNReal.ofReal 1 = 1

Tactic:
by simp [ENNReal.ofReal]

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

Goal state before:
pp: n : ℕ
⊢ ENNReal.ofReal ↑n = ↑n

Tactic:
by simp [ENNReal.ofReal]

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✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
⊢ max (p 1) (q 1) = p 1

Tactic:
sup_eq_left,

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
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
⊢ q 1 ≤ p 1
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p : ℝ
⊢ 0 < ENNReal.ofReal p ↔ 0 < p

Tactic:
by simp [ENNReal.ofReal]

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

Goal state before:
pp: p : ℝ
⊢ ENNReal.ofReal p = 0 ↔ p ≤ 0

Tactic:
by simp [ENNReal.ofReal]

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
p✝ q✝ p q : NonarchAddGroupSeminorm E
⊢ max (p 0) (q 0) = p 0

Tactic:
sup_eq_left,

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p✝ q✝ p q : NonarchAddGroupSeminorm E
⊢ q 0 ≤ p 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a - ⨅ i, f i = ⨆ i, a - f i

Tactic:
refine eq_of_forall_ge_iff fun c => ?_
  rw [tsub_le_iff_right, add_comm, iInf_add]
  simp [tsub_le_iff_right, add_comm]

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

Goal state before:
pp: ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
cases isEmpty_or_nonempty ι
  · simp
  · refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))
    refine iSup_add_iSup_le fun i j => ?_
    rcases h i j with ⟨k, hk⟩
    exact le_iSup_of_le k hk

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

Goal state before:
pp: x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ {⊥, ⊤}ᶜ

Tactic:
induction x <;> simp

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

Goal state before:
pp: x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ Ioo ⊥ ⊤

Tactic:
induction x <;> simp

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

Goal state before:
pp: case mp
y : ℝ
hy0 : 0 < ↑y
right✝ : ↑y < ⊤
⊢ (↑y).toReal ∈ Ioi 0

Tactic:
simpa using hy0

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

Goal state before:
pp: case mp
y : ℝ
left✝ : ⊥ < ↑y
hy0 : ↑y < 0
⊢ (↑y).toReal ∈ Iio 0

Tactic:
simpa using hy0

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

Goal state before:
pp: x y : ℝ
⊢ WithBot.some '' Ico ↑x ↑y = Ico ↑x ↑y

Tactic:
WithBot.image_coe_Ico

Goal state after:
x y : ℝ
⊢ Ico ↑↑x ↑↑y = Ico ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ WithBot.some '' Ico ↑x ⊤ = Ico ↑x ⊤

Tactic:
WithBot.image_coe_Ico

Goal state after:
x : ℝ
⊢ Ico ↑↑x ↑⊤ = Ico ↑x ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Iio x = Ioo ⊥ ↑x

Tactic:
by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Iio, WithBot.image_coe_Iio]
  rfl

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

Goal state before:
pp: r p : ℝ≥0
⊢ ↑(p / r) ≤ ↑p / ↑r

Tactic:
simpa only [div_eq_mul_inv, coe_mul] using _root_.mul_le_mul_right coe_inv_le _

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

Goal state before:
pp: a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
⊢ a * (a⁻¹ * b) = b

Tactic:
by
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp_all
  obtain rfl | ha := eq_or_ne a ⊤
  · simp_all
  · simp [← mul_assoc, ENNReal.mul_inv_cancel, *]

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

Goal state before:
pp: case pos
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
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : n = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

pp: case neg
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
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : ¬n = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
· rw [hn, neg_zero, zpow_zero, count_one, neg_zero]

Goal state after:
case neg
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
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : ¬n = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)