mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2.inr.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ normalize p = q

Tactic:
← normalize_normalized_factor _ hq

Goal state after:
case neg.refine_2.inr.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ normalize p = normalize q
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ Submonoid.map (algebraMap R S) M ≤ IsUnit.submonoid S

Tactic:
rintro _ ⟨a, ha, rfl⟩
  exact IsLocalization.map_units S ⟨_, ha⟩

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
⊢ S.leftInv.leftInv ≤ S

Tactic:
rintro x ⟨⟨y, z, h₁⟩, h₂ : x * y = 1⟩
  convert! z.prop
  rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case e'_3
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∉ U j
⊢ Subtype.val ⁻¹' {↑y} = ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Goal state after:
case e'_3
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∉ U j
⊢ ∀ (x : ↥(U j)), x ∉ Subtype.val ⁻¹' {↑y}
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_2
M✝ : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M✝
inst✝¹ : Module R M✝
inst✝ : IsSemiprimaryRing R
M : Type u
x✝³ : AddCommGroup M
x✝² x✝¹ : Module R M
x✝ : IsScalarTower R R M
h : IsNoetherian R ↥(Ring.jacobson R • ⊤) ↔ IsArtinian R ↥(Ring.jacobson R • ⊤)
h' : IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)
N : Submodule R M := Ring.jacobson R • ⊤
⊢ IsArtinian R ↥(Ring.jacobson R • ⊤) ∧ IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔
    IsArtinian R ↥(Ring.jacobson R • ⊤) ∧ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)

Tactic:
h'

Goal state after:
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
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
x : X
hx : x ∈ S ∩ closedPoints X
⊢ f x ∈ closedPoints Y

Tactic:
simpa using hf₂ _ hx.2

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Inertia

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
hq : q.IsPrime
inst✝¹ : Algebra (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
⊢ q.inertiaDeg R = Module.finrank (under R q).ResidueField q.ResidueField

Tactic:
by
  convert! dif_pos hq
  simp [Algebra.algebra_ext_iff, Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq]

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Inertia

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✝² : q.LiesOver p
inst✝¹ : p.IsMaximal
inst✝ : q.IsMaximal
⊢ p.inertiaDeg' q = q.inertiaDeg R

Tactic:
by
  rw [inertiaDeg'_algebraMap, inertiaDeg_eq_of_isMaximal p q]

Goal state after:
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
⊢ length B (B ⊗[A] M) = length A M * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
by
  by_cases h : IsFiniteLength A M
  · obtain ⟨s, hs_bot, hs_top⟩ := isFiniteLength_iff_exists_compositionSeries.mp h
    rw [← length_compositionSeries s hs_bot hs_top]
    suffices ∀ k, length B ((s k).baseChange B) =
        k * length B (B ⧸ (maximalIdeal A).map (algebraMap A B)) by
      rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top, baseChange_top, length_top]
    intro k
    induction k using Fin.induction with
    | zero => rw [← RelSeries.head, hs_bot, baseChange_bot]; simp
    | succ i hi => simpa [hi, add_one_mul] using (s.step i).length_baseChange B
  · have : ¬ IsFiniteLength B (B ⊗[A] M) := by
      contrapose! h
      rw [isFiniteLength_iff_isNoetherian_isArtinian] at h ⊢
      have : FaithfullyFlat A B := FaithfullyFlat.of_flat_of_isLocalHom
      exact h.imp IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat
        IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat
    rw [← length_ne_top_iff, not_ne_iff] at h this
    have ne : length B (B ⧸ (maximalIdeal A).map (algebraMap A B)) ≠ 0 := by
      simpa [← pos_iff_ne_zero, length_pos_iff] using (map_maximalIdeal_lt_top (algebraMap A B)).ne
    rw [h, this, ENat.top_mul ne]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤

Tactic:
obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
H : IsIdempotentElem (R ∙ e)
⊢ R ∙ e = ⊥ ∨ R ∙ e = ⊤
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 Q (normalizedFactors (map (algebraMap S T) (map f p))) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))

Tactic:
heq,

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 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 Q (normalizedFactors (map (algebraMap S T) (P ^ Multiset.count P (normalizedFactors (map f p)) * I))) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))
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 I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)

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
⊢ RingHom.ker (Ideal.Quotient.mk (I ^ i)) ≤ I

pp: case neg.hf
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
⊢ Function.Surjective ⇑(Ideal.Quotient.mk (I ^ i))

Tactic:
· exact H _

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
⊢ RingHom.ker (Ideal.Quotient.mk (I ^ i)) ≤ I

case neg.hf
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
⊢ Function.Surjective ⇑(Ideal.Quotient.mk (I ^ i))
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
⊢ (∃ e, IsIdempotentElem e ∧ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = S ⊗[R] S ∙ e) →
    ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ 1 - t ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
⊢ (∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ 1 - t ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) →
    ∃ e, IsIdempotentElem e ∧ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = S ⊗[R] S ∙ e

Tactic:
· rintro ⟨e, he₁, he₂ : _ = Ideal.span _⟩
    refine ⟨1 - e, ?_, ?_⟩
    · intro s
      obtain ⟨x, hx⟩ : e ∣ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 := by
        rw [← Ideal.mem_span_singleton, ← he₂]
        exact Ideal.subset_span ⟨s, rfl⟩
      rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]
    · rw [sub_sub_cancel, he₂, Ideal.mem_span_singleton]

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
⊢ (∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ 1 - t ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) →
    ∃ e, IsIdempotentElem e ∧ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = S ⊗[R] S ∙ e
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 Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
inst✝ : QuasiFiniteAt R Q
⊢ QuasiFiniteAt R P

Tactic:
let f : Localization.AtPrime Q →ₐ[R] Localization.AtPrime P :=
    IsLocalization.liftAlgHom (M := Q.primeCompl) (f := IsScalarTower.toAlgHom _ _ _) <| by
      simp only [IsScalarTower.coe_toAlgHom', Subtype.forall, Ideal.mem_primeCompl_iff]
      exact fun a ha ↦ IsLocalization.map_units (M := P.primeCompl) _ ⟨a, fun h ↦ ha (h₁ h)⟩
  refine .of_forall_exists_mul_mem_range f fun x ↦ ?_
  obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl x
  exact ⟨algebraMap _ _ s, by simpa [f] using IsLocalization.map_units _ ⟨s, hs⟩,
    algebraMap _ _ x, by simp [f]⟩

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
P : Type u_2
C : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : CommRing C
inst✝³ : Algebra R C
inst✝² : CommRing P
inst✝¹ : Algebra R P
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
lift : P₁.Ring →ₐ[R] P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
x : P₁.infinitesimal.Ring
⊢ (algebraMap P₂.infinitesimal.Ring A) ((Ideal.Quotient.liftₐ (P₁.ker ^ 2) lift ⋯).toRingHom x) =
    (algebraMap A A) ((algebraMap P₁.infinitesimal.Ring A) x)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
      exact FormallySmooth.liftOfSurjective_apply _
            (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) _ _ x

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

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

Tactic:
by
  refine .of_comp_surjective fun C _ _ I hI f ↦ ?_
  obtain ⟨f', e⟩ := FormallySmooth.comp_surjective _ _ I hI (f.comp (IsScalarTower.toAlgHom R A B))
  let := f'.toRingHom.toAlgebra
  obtain ⟨f'', e'⟩ := comp_surjective _ _ I hI { f with commutes' := AlgHom.congr_fun e.symm }
  apply_fun AlgHom.restrictScalars R at e'
  exact ⟨f''.restrictScalars _, e'.trans (AlgHom.ext fun _ => rfl)⟩

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

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
g : A →ₐ[R] R ⧸ RingHom.ker (ofId R A).toRingHom ^ 2
hg : (ofId R A).kerSquareLift.comp g = AlgHom.id R A
⊢ (g.comp (ofId R A).kerSquareLift).comp (Ideal.Quotient.mkₐ R (RingHom.ker (algebraMap R A) ^ 2)) =
    (AlgHom.id R (R ⧸ RingHom.ker (algebraMap R A) ^ 2)).comp (Ideal.Quotient.mkₐ R (RingHom.ker (algebraMap R A) ^ 2))

Tactic:
by ext

Goal state after:
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✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this : ExpChar (L ⊗[K] L) (ringExpChar K)
⊢ (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0

Tactic:
sub_pow_expChar_pow,

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this : ExpChar (L ⊗[K] L) (ringExpChar K)
⊢ 1 ⊗ₜ[K] x ^ ringExpChar K ^ n - x ⊗ₜ[K] 1 ^ ringExpChar K ^ n = 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
y : Q.Ring ⊗[P.Ring] ↥P.ker
a : Q.Ring
b : ↥P.ker
⊢ ↑(e (a ⊗ₜ[P.Ring] b)) •
      (LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk)) y =
    0

Tactic:
| tmul a b =>

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✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : S
hx : x ∈ RingHom.ker (algebraMap S (ResidueField S))
⊢ (KaehlerDifferential.kerCotangentToTensor R S (ResidueField S))
      ((RingHom.ker (algebraMap S (ResidueField S))).toCotangent ⟨x, hx⟩) =
    0

Tactic:
simp only [KaehlerDifferential.kerCotangentToTensor_toCotangent]

Goal state after:
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✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : S
hx : x ∈ RingHom.ker (algebraMap S (ResidueField S))
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
a : T
b : P.Cotangent
⊢ (tensorCotangentInvFun f halg H) ((LinearMap.liftBaseChange T (Cotangent.map f)) (a ⊗ₜ[S] b)) = a ⊗ₜ[S] b

Tactic:
| tmul a b =>

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

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
a : Q.Ring
b : ↥P.ker
⊢ (LinearMap.liftBaseChange T (Cotangent.map f))
      ((tensorCotangentInvFun f halg H)
        (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) (a ⊗ₜ[P.Ring] b)))) =
    Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) (a ⊗ₜ[P.Ring] b))

Tactic:
| tmul a b =>

Goal state after:
Module: Mathlib.Data.Finsupp.Encodable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Countable α
inst✝¹ : Countable β
inst✝ : Zero β
⊢ Countable (α →₀ β)

Tactic:
classical exact .of_equiv _ finsuppEquivDFinsupp.symm

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
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this✝ : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
⊢ x ∈ ⨆ P, primaryComponent M P.asIdeal

Tactic:
have hPairwise : (S : Set (HeightOneSpectrum _)).Pairwise
      fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤ :=
    fun r hr s hs hrs ↦ (isCoprime_pow_of_ne _ _ hrs _ _).sup_eq

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this✝ : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
hPairwise : (↑S).Pairwise fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
⊢ x ∈ ⨆ P, primaryComponent M P.asIdeal
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
h₁ : s.Nonempty
h₂ : BddAbove s
⊢ IsLUB s (sSup s)

Tactic:
by
  simp only [sSup_def, dif_pos (And.intro h₁ h₂)]
  apply Classical.choose_spec

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

Goal state before:
pp: case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x ∈ s, x < a + ε

pp: case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε

Tactic:
· exact exists_lt_of_csInf_lt h' (H ε ε_pos)

Goal state after:
case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε
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
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) =
    ↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)

Tactic:
FractionalIdeal.coeIdeal_finprod R⁰ K (le_refl _)

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
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) =
    ∏ᶠ (a : HeightOneSpectrum R), ↑(a.maxPowDividing I)
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℝ≥0∞ → α
⊢ ⨅ x, ⨅ (_ : x ≠ ∞), f x = ⨅ x, f ↑x

Tactic:
by rw [iInf_subtype', cinfi_ne_top]

Goal state after: