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

Goal state before:
pp: case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
x : S
hx : x ∈ I
⊢ x = 0

Tactic:
← Algebra.norm_eq_zero_iff (R := ℤ),

Goal state after:
case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
x : S
hx : x ∈ I
⊢ (Algebra.norm ℤ) x = 0
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ absNorm I = 0 → I = ⊥

Tactic:
intro hI
    rw [← le_bot_iff]
    intro x hx
    rw [mem_bot, ← Algebra.norm_eq_zero_iff (R := ℤ), ← Int.natAbs_eq_zero,
      ← Ideal.absNorm_span_singleton, ← zero_dvd_iff, ← hI]
    apply Ideal.absNorm_dvd_absNorm_of_le
    rwa [Ideal.span_singleton_le_iff_mem]

Goal state after:
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 : Ideal S
inst✝ : P.IsMaximal
this : IsAddTorsionFree S
⊢ ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ absNorm P = p ^ n

Tactic:
have := CharZero.of_isAddTorsionFree S S

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
this✝ : IsAddTorsionFree S
this : CharZero S
⊢ ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ absNorm P = p ^ n
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)
this : IsAddTorsionFree S
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I

Tactic:
have := CharZero.of_isAddTorsionFree S S

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
this : CharZero S
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
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
inst✝ : CharZero S
n : ℕ
⊢ {I | absNorm I = n}.Finite

Tactic:
obtain hn | hn := Nat.eq_zero_or_pos n

Goal state after:
case inl
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n = 0
⊢ {I | absNorm I = n}.Finite

case inr
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
⊢ {I | absNorm I = n}.Finite
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
⊢ f ⁻¹' closedPoints Y = closedPoints X

Tactic:
apply subset_antisymm (preimage_closedPoints_subset hf.injective hf.continuous)
  intro x hx
  apply isClosed_singleton_of_isLocallyClosed_singleton
  rw [← Set.image_singleton]
  exact (hx.isLocallyClosed.image hf.isInducing hf.isOpen_range.isLocallyClosed)

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap f (comap (↑e.toRingEquiv.symm.symm) (P ^ n)) ↔ p ≤ comap (algebraMap R S₁) (P ^ n)

Tactic:
comap_comap,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap ((↑e.toRingEquiv.symm.symm).comp f) (P ^ n) ↔ p ≤ comap (algebraMap R S₁) (P ^ n)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    maximalIdeal (Localization P.primeCompl) * maximalIdeal (Localization P.primeCompl)
this : map (algebraMap S (Localization.AtPrime P)) P = ⊥
⊢ False

Tactic:
Ideal.map_eq_bot_iff_of_injective

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    maximalIdeal (Localization P.primeCompl) * maximalIdeal (Localization P.primeCompl)
this : P = ⊥
⊢ False

R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    maximalIdeal (Localization P.primeCompl) * maximalIdeal (Localization P.primeCompl)
this : map (algebraMap S (Localization.AtPrime P)) P = ⊥
⊢ Function.Injective ⇑(algebraMap S (Localization.AtPrime P))
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
⊢ ¬p.ramificationIdx' P ≠ 1 → map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)

Tactic:
ramificationIdx'_ne_one_iff hpP,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
⊢ ¬map f p ≤ P ^ 2 → map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case h₂
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e : (Ideal.Quotient.mk J) (g₁ x) = (Ideal.Quotient.mk J) (g₂ x)
⊢ (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) ((Ideal.Quotient.mk I) (g₁ x)) =
    (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) ((Ideal.Quotient.mk I) (g₂ x))

Tactic:
Ideal.Quotient.eq,

Goal state after:
case h₂
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e : (Ideal.Quotient.mk J) (g₁ x) = (Ideal.Quotient.mk J) (g₂ x)
⊢ (Ideal.Quotient.mk I) (g₁ x) - (Ideal.Quotient.mk I) (g₂ x) ∈ Ideal.map (Ideal.Quotient.mk I) J
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case neg
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
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : ¬i = 0
x : A
⊢ (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (I ^ i)) I)) ((Ideal.Quotient.mk (I ^ i)) (g₁ x)) =
    (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (I ^ i)) I)) ((Ideal.Quotient.mk (I ^ i)) (g₂ x))

Tactic:
Ideal.Quotient.eq,

Goal state after:
case neg
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
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : ¬i = 0
x : A
⊢ (Ideal.Quotient.mk (I ^ i)) (g₁ x) - (Ideal.Quotient.mk (I ^ i)) (g₂ x) ∈ Ideal.map (Ideal.Quotient.mk (I ^ i)) I
Module: Mathlib.NumberTheory.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 S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I
hntq : ¬⊤ ≤ Q
⊢ Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P)) +
      Multiset.count Q (normalizedFactors (map (algebraMap S T) I)) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))

Tactic:
exact add_eq_left.mpr <| Decidable.byContradiction fun h ↦ hntq <| hcp.trans_le <|
    sup_le hg <| le_of_dvd <| dvd_of_mem_normalizedFactors <| Multiset.count_ne_zero.mp h

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✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ (Ideal.Quotient.mkₐ R I).comp (f₁.comp (IsScalarTower.toAlgHom R A B)) =
    (Ideal.Quotient.mkₐ R I).comp (f₂.comp (IsScalarTower.toAlgHom R A B))

Tactic:
rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc]

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

Goal state before:
pp: case h2
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).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker ≤
    Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker)
      (Submodule.comap Extension.Cotangent.mk
        (Submodule.restrictScalars (Q.comp P).Ring
          (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range)))

Tactic:
rw [Ideal.map_le_iff_le_comap]

Goal state after:
case h2
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).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ P.ker ≤
    Ideal.comap (Q.toComp P).toAlgHom.toRingHom
      (Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker)
        (Submodule.comap Extension.Cotangent.mk
          (Submodule.restrictScalars (Q.comp P).Ring
            (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range))))
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✝¹ : FormallyUnramified R A
inst✝ : FormallySmooth R B
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra A C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[A] C ⧸ I
algInst✝ : Algebra R C := ((algebraMap A C).comp (algebraMap R A)).toAlgebra
scalarTowerInst✝ : IsScalarTower R A C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R C))
g : B →ₐ[R] C
hg : (Ideal.Quotient.mkₐ R I).comp g = AlgHom.restrictScalars R f
⊢ g.comp (IsScalarTower.toAlgHom R A B) = IsScalarTower.toAlgHom R A C

Tactic:
apply Algebra.FormallyUnramified.comp_injective _ hI

Goal state after:
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✝¹ : FormallyUnramified R A
inst✝ : FormallySmooth R B
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra A C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[A] C ⧸ I
algInst✝ : Algebra R C := ⋯
scalarTowerInst✝ : IsScalarTower R A C := ⋯
g : B →ₐ[R] C
hg : (Ideal.Quotient.mkₐ R I).comp g = AlgHom.restrictScalars R f
⊢ (Ideal.Quotient.mkₐ R I).comp (g.comp (IsScalarTower.toAlgHom R A B)) =
    (Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A C)
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
⊢ 1 - f 1 • 1 = 0

Tactic:
hf₁,

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 - 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 := ⋯
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A := ⋯
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := ⋯
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
⊢ IsIdempotentElem (f 1)

Tactic:
rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, hf₁]

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
inst✝ : Algebra.FormallyEtale S T
x : T ⊗[S] Ω[S⁄R]
hx : (mapBaseChange R S T) x = 0
⊢ x = 0

Tactic:
obtain ⟨x, rfl⟩ := (Algebra.H1Cotangent.exact_δ_mapBaseChange R S T x).mp hx

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : Algebra.FormallyEtale S T
x : Algebra.H1Cotangent S T
hx : (mapBaseChange R S T) ((Algebra.H1Cotangent.δ R S T) x) = 0
⊢ (Algebra.H1Cotangent.δ R S T) x = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
hs : ∃ x ∈ s, 0 ≤ x
⊢ 0 ≤ sSup s

Tactic:
by
  classical
  obtain ⟨x, hxs, hx⟩ := hs
  exact dite _ (fun h ↦ le_csSup_of_le h hxs hx) fun h ↦ (sSup_of_not_bddAbove h).ge

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

Goal state before:
pp: x : ℝ
⊢ 0 < nnabs x ↔ x ≠ 0

Tactic:
simp [← NNReal.coe_pos]

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

Goal state before:
pp: ⊢ ⋃ n, Iio ↑n = {∞}ᶜ

Tactic:
ext x
  rw [mem_iUnion]
  exact ⟨fun ⟨n, hn⟩ => ne_top_of_lt hn, ENNReal.exists_nat_gt⟩

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : ∑ i ∈ s, p i = 0
f : HeightOneSpectrum A → ℕ
hmem : ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ f i)
m : ℕ := s.sup f
hSupIndep :
  ∀ (s : Finset (HeightOneSpectrum A)) (v : HeightOneSpectrum A → M),
    (∀ i ∈ s, v i ∈ torsionBySet A M ↑(i.asIdeal ^ m)) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
⊢ ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ m)

Tactic:
exact fun P hP ↦ torsionBySet_le_torsionBySet_pow _ _ (Finset.le_sup hP) _ (hmem P hP)

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
⊢ ∃ f, ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b

Tactic:
simp only [← mem_iSup_iff_exists_dfinsupp, iSup_primaryComponent_eq_top hM₁, mem_top]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

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

Tactic:
rw [if_pos hx, hx, one_mul, zero_add]

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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : ¬Ideal.span {a} = 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬a = 0

Tactic:
Ideal.zero_eq_bot,

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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : ¬Ideal.span {a} = ⊥
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬a = 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * b = a ↔ b = 1

Tactic:
by
  simpa using ENNReal.mul_right_inj ha₀ ha (c := 1)

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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ¬Ideal.span {choose ⋯} = 0

Tactic:
Ideal.zero_eq_bot,

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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ¬Ideal.span {choose ⋯} = ⊥
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: p : EReal → Prop
⊢ (p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r) → ∃ r, p r

Tactic:
rintro (h | h | ⟨r, hr⟩)

Goal state after:
case inl
p : EReal → Prop
h : p ⊥
⊢ ∃ r, p r

case inr.inl
p : EReal → Prop
h : p ⊤
⊢ ∃ r, p r

case inr.inr
p : EReal → Prop
r : ℝ
hr : p ↑r
⊢ ∃ r, p r