mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
H : Subgroup G
inst✝¹ : H.Normal
inst✝ : Algebra.IsInvariant A B G
x : ↥(FixedPoints.subalgebra A B ↥H)
hx : ∀ (g : G ⧸ H), g • x = x
⊢ ∃ a, (algebraMap A ↥(FixedPoints.subalgebra A B ↥H)) a = x

Tactic:
obtain ⟨y, hy⟩ := Algebra.IsInvariant.isInvariant (A := A) (G := G) x.1
      (fun g ↦ congr_arg Subtype.val (hx g))

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
H : Subgroup G
inst✝¹ : H.Normal
inst✝ : Algebra.IsInvariant A B G
x : ↥(FixedPoints.subalgebra A B ↥H)
hx : ∀ (g : G ⧸ H), g • x = x
y : A
hy : (algebraMap A B) y = ↑x
⊢ ∃ a, (algebraMap A ↥(FixedPoints.subalgebra A B ↥H)) a = x
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
F : Type u_6
inst✝² : Field F
inst✝¹ : Algebra K F
inst✝ : FiniteDimensional K L
x : L
hF : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
⊢ (algebraMap ℕ K) (finrank (↥K⟮x⟯) L) • (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)) =
    finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum

Tactic:
IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots _ hF,

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
F : Type u_6
inst✝² : Field F
inst✝¹ : Algebra K F
inst✝ : FiniteDimensional K L
x : L
hF : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
⊢ (algebraMap ℕ K) (finrank (↥K⟮x⟯) L) • ((minpoly K x).aroots F).sum = finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case neg
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
hh : ¬h⁻¹ • Q = Q
⊢ a - eval b r ∈ h⁻¹ • Q

Tactic:
exact hr' h⁻¹ hh

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

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β : κ
⊢ traceMatrix A (b ᵥ* P.map ⇑(algebraMap A B)) α β = (Pᵀ * traceMatrix A b * P) α β

Tactic:
traceMatrix_apply,

Goal state after:
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β : κ
⊢ ((traceForm A B) ((b ᵥ* P.map ⇑(algebraMap A B)) α)) ((b ᵥ* P.map ⇑(algebraMap A B)) β) =
    (Pᵀ * traceMatrix A b * P) α β
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis κ A B
i j : κ
⊢ traceMatrix A (⇑b) i j = (LinearMap.BilinForm.toMatrix b) (traceForm A B) i j

Tactic:
traceMatrix_apply,

Goal state after:
κ : Type w
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis κ A B
i j : κ
⊢ ((traceForm A B) (b i)) (b j) = (LinearMap.BilinForm.toMatrix b) (traceForm A B) i j
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case refine_2
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁴ : Group G
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ F
this : IntermediateField.restrictScalars K (FixedPoints.intermediateField ↥H) = IntermediateField.restrictScalars K ⊥
⊢ x ∈ FixedPoints.intermediateField ↥H

Tactic:
restrictScalars_bot_eq_self

Goal state after:
case refine_2
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁴ : Group G
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ F
this : IntermediateField.restrictScalars K (FixedPoints.intermediateField ↥H) = F
⊢ x ∈ FixedPoints.intermediateField ↥H
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
hg : G ≠ ⊥
⊢ ∑ x, ↑↑x = 0

Tactic:
by
  rw [Subgroup.ne_bot_iff_exists_ne_one] at hg
  rcases hg with ⟨a, ha⟩
  -- The action of a on G as an embedding
  let a_mul_emb : G ↪ G := mulLeftEmbedding a
  -- ... and leaves G unchanged
  have h_unchanged : Finset.univ.map a_mul_emb = Finset.univ := by simp
  -- Therefore the sum of x over a G is the sum of a x over G
  have h_sum_map := Finset.univ.sum_map a_mul_emb fun x => ((x : Kˣ) : K)
  -- ... and the former is the sum of x over G.
  -- By algebraic manipulation, we have Σ G, x = ∑ G, a x = a ∑ G, x
  simp only [h_unchanged, mulLeftEmbedding_apply, Subgroup.coe_mul, Units.val_mul, ← mul_sum,
    a_mul_emb] at h_sum_map
  -- thus one of (a - 1) or ∑ G, x is zero
  have hzero : (((a : Kˣ) : K) - 1) = 0 ∨ ∑ x : ↥G, ((x : Kˣ) : K) = 0 := by
    rw [← mul_eq_zero, sub_mul, ← h_sum_map, one_mul, sub_self]
  apply Or.resolve_left hzero
  contrapose ha
  ext
  rwa [← sub_eq_zero]

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ (trace K L).range = ⊤

Tactic:
apply (IsSimpleOrder.eq_bot_or_eq_top (α := Ideal K) _).resolve_left

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ ¬(trace K L).range = ⊥
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * d - a * d' ∈ P ^ (i + 1)

Tactic:
simp only [← mul_sub]

Goal state after:
S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * (d - d') ∈ P ^ (i + 1)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case succ
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
⊢ cardQuot (P ^ (i + 1)) = cardQuot P ^ (i + 1)

Tactic:
suffices hquot : map (P ^ i.succ).mkQ (P ^ i) ≃ S ⧸ P by
    rw [pow_succ' (cardQuot P), ← ih, cardQuot_apply (P ^ i.succ), ←
      card_quotient_mul_card_quotient (P ^ i) (P ^ i.succ) this.le, cardQuot_apply (P ^ i),
      cardQuot_apply P, Nat.card_congr hquot]

Goal state after:
case succ
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
⊢ ↥(map (mkQ (P ^ i.succ)) (P ^ i)) ≃ S ⧸ P
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
m : ↥M
x✝ : S
⊢ m • x✝ = (algebraMap R S) ↑m * x✝

Tactic:
rw [← Algebra.smul_def]

Goal state after:
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
m : ↥M
x✝ : S
⊢ m • x✝ = ↑m • x✝
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
hI : p ∣ ↑(absNorm P)
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
⊢ span {p} ≤ under ℤ P

Tactic:
rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI

Goal state after:
case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hI : ∃ i ≤ n, Associated p (↑q ^ i)
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
⊢ span {p} ≤ under ℤ P
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro B _ _ _ _ f₁ f₂ _

Goal state after:
R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I✝ : Ideal B
x✝ : I✝ ^ 2 = ⊥
f₁ f₂ : R →ₐ[R] B
a✝ : (Ideal.Quotient.mkₐ R I✝).comp f₁ = (Ideal.Quotient.mkₐ R I✝).comp f₂
⊢ f₁ = f₂
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
inst✝¹ : IsArtinianRing R
inst✝ : QuasiFinite R S
⊢ Module.Finite R S

Tactic:
classical
  let e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
    .ofBijective (IsScalarTower.toAlgHom _ _ _)
      (PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective.mp inferInstance)
  have : Fintype (PrimeSpectrum R) := .ofFinite _
  let e' : S ≃ₐ[R] Π p : PrimeSpectrum R, Localization p.asIdeal.primeCompl ⊗[R] S :=
    (Algebra.TensorProduct.rid R R S).symm.trans <| (Algebra.TensorProduct.congr .refl e).trans <|
      (Algebra.TensorProduct.piRight _ _ _ _).trans <| AlgEquiv.piCongrRight
      fun _ ↦ Algebra.TensorProduct.comm _ _ _
  have (p : PrimeSpectrum R) : Module.Finite R (Localization p.asIdeal.primeCompl ⊗[R] S) :=
    have : Module.Finite R (Localization.AtPrime p.asIdeal) :=
      .of_surjective (Algebra.linearMap _ _)
        (IsArtinianRing.localization_surjective p.asIdeal.primeCompl _)
    have : Module.Finite (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] S) := finite_of_isArtinianRing_of_isLocalRing
    .trans (Localization.AtPrime p.asIdeal) _
  exact .of_surjective e'.symm.toLinearMap e'.symm.surjective

Goal state after:
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 σ
⊢ Function.Exact ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
    ⇑(Extension.Cotangent.map (Q.ofComp P).toExtensionHom)

Tactic:
apply LinearMap.exact_of_comp_of_mem_range
  · rw [LinearMap.liftBaseChange_comp, ← Extension.Cotangent.map_comp,
      EmbeddingLike.map_eq_zero_iff]
    ext x
    obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
    simp only [map_mk, val_mk, LinearMap.zero_apply, val_zero]
    convert! Q.ker.toCotangent.map_zero
    trans ((IsScalarTower.toAlgHom R _ _).comp (IsScalarTower.toAlgHom R P.Ring S)) x
    · congr
      refine MvPolynomial.algHom_ext fun i ↦ ?_
      change (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom (X i)) = _
      simp
    · simp [aeval_val_eq_zero hx]
  · intro x hx
    obtain ⟨⟨x : (Q.comp P).Ring, hx'⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
    replace hx : (Q.ofComp P).toAlgHom x ∈ Q.ker ^ 2 := by
      simpa only [map_mk, val_mk, val_zero, Ideal.toCotangent_eq_zero] using! congr(($hx).val)
    rw [pow_two, ← map_ofComp_ker (P := P), ← Ideal.map_mul, Ideal.mem_map_iff_of_surjective
      _ (toAlgHom_ofComp_surjective Q P)] at hx
    obtain ⟨y, hy, e⟩ := hx
    rw [eq_comm, ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, ← map_toComp_ker] at e
    rw [LinearMap.range_liftBaseChange]
    let z : (Q.comp P).ker := ⟨x - y, Ideal.sub_mem _ hx' (Ideal.mul_le_right hy)⟩
    have hz : z.1 ∈ P.ker.map (Q.toComp P).toAlgHom.toRingHom := e
    have : Extension.Cotangent.mk (P := (Q.comp P).toExtension) ⟨x, hx'⟩ =
      Extension.Cotangent.mk z := by
      ext; simpa only [val_mk, Ideal.toCotangent_eq, sub_sub_cancel, pow_two, z]
    rw [this, ← Submodule.restrictScalars_mem (Q.comp P).Ring, ← Submodule.mem_comap,
      ← Submodule.span_singleton_le_iff_mem, ← Submodule.map_le_map_iff_of_injective
      (f := Submodule.subtype _) Subtype.val_injective, Submodule.map_subtype_span_singleton,
      Submodule.span_singleton_le_iff_mem]
    refine (show Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker ≤ _ from ?_) hz
    rw [Ideal.map_le_iff_le_comap]
    rintro w hw
    simp only [AlgHom.toRingHom_eq_coe, Ideal.mem_comap, RingHom.coe_coe,
      Submodule.mem_map, Submodule.mem_comap, Submodule.restrictScalars_mem, Submodule.coe_subtype,
      Subtype.exists, exists_and_right, exists_eq_right,
      toExtension_Ring]
    refine ⟨?_, Submodule.subset_span ⟨Extension.Cotangent.mk ⟨w, hw⟩, ?_⟩⟩
    · simp only [ker_eq_ker_aeval_val, RingHom.mem_ker, Hom.algebraMap_toAlgHom]
      rw [aeval_val_eq_zero hw, map_zero]
    · rw [map_mk]
      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
⊢ IsField A

Tactic:
by
  rw [IsLocalRing.isField_iff_maximalIdeal_eq, eq_bot_iff]
  intro x hx
  obtain ⟨x, rfl⟩ := (bijective_of_isAlgClosed_of_isLocalRing K A).surjective x
  change _ = 0
  rw [← (algebraMap K A).map_zero]
  by_contra hx'
  exact hx ((isUnit_iff_ne_zero.mpr
    (fun e ↦ hx' ((algebraMap K A).congr_arg e))).map (algebraMap K A))

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

Goal state before:
pp: case refine_4
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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
f : { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
x : S
a✝ : P
⊢ (((AlgebraTensorModule.curry
              ↑((fun x ↦
                    match x with
                    | ⟨l, hl⟩ => ⟨↑e₁.symm ∘ₗ ↑P l ∘ₗ ↑e₂.symm, ⋯⟩)
                  ((fun x ↦
                      match x with
                      | ⟨l, hl⟩ => ⟨{ toAddHom := ↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂), map_smul' := ⋯ }, ⋯⟩)
                    f)))
            x).compDer
        (D R P))
      a✝ =
    (((AlgebraTensorModule.curry ↑f) x).compDer (D R P)) a✝

Tactic:
simp only [AlgebraTensorModule.curry_apply, Derivation.coe_comp, LinearMap.coe_comp,
      LinearMap.coe_restrictScalars, Derivation.coeFn_coe, Function.comp_apply, curry_apply,
      LinearEquiv.coe_coe, LinearMap.coe_mk, AddHom.coe_coe,
      LinearEquiv.apply_symm_apply, LinearEquiv.symm_apply_apply]

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
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
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
s : Finset S
hs : Submodule.span R ↑s = ⊤
⊢ Submodule.span (Localization.AtPrime p)
      ↑(Submodule.map (IsScalarTower.toAlgHom R S (Localization.AtPrime q)).toLinearMap ⊤) =
    ⊤

Tactic:
Submodule.map_top,

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
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
s : Finset S
hs : Submodule.span R ↑s = ⊤
⊢ Submodule.span (Localization.AtPrime p) ↑(IsScalarTower.toAlgHom R S (Localization.AtPrime q)).toLinearMap.range = ⊤
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.IsPrime
inst✝ : q.LiesOver p
hp : map (algebraMap R S) p ≠ ⊥
⊢ q.ramificationIdx R = multiplicity q (map (algebraMap R S) p)

Tactic:
by
  have hq : q ≠ ⊥ := ne_bot_of_le_ne_bot hp (map_le_of_le_comap (q.over_def p).le)
  rw [ramificationIdx_eq_normalizedFactors_count p q hp,
    multiplicity_eq_of_emultiplicity_eq_some (emultiplicity_eq_count_normalizedFactors
      (prime_of_isPrime hq inferInstance).irreducible hp), normalize_eq]

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
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), r * ∏ i ∈ s, b i ∣ r' → Function.Bijective ⇑(awayMap (algebraMap R S) r')

Tactic:
refine fun r' hr' ↦ ⟨hr _ (.trans ⟨_, rfl⟩ hr'), ?_⟩

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'
⊢ Function.Surjective ⇑(awayMap (algebraMap R S) r')
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.inf fun i ↦ (S i)ᶜ)) = ∑ t ∈ s.powerset, (-1) ^ #t * ↑(#(t.inf S))

Tactic:
simpa using inclusion_exclusion_sum_inf_compl (G := ℤ) s S (f := 1)

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

Goal state before:
pp: case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨅ x, 0 = 0

Tactic:
exact ciInf_const

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

Goal state before:
pp: r : ℝ
⊢ 0 < r.toNNReal ↔ 0 < r

Tactic:
by
  simp [← NNReal.coe_lt_coe]

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

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

Tactic:
have h_dvd := finprod_mem_dvd v (hasFiniteMulSupport hI)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd : v.maxPowDividing I ∣ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ ⨅ i, i.maxPowDividing I = ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I

Tactic:
finprod_def,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ ⨅ i, i.maxPowDividing I =
    if h : HasFiniteMulSupport fun v ↦ v.maxPowDividing I then ∏ i ∈ Finite.toFinset h, i.maxPowDividing I else 1
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: x y : ℝ≥0∞
⊢ x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0

Tactic:
simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff]

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 ℝ
r : R
p : AddGroupSeminorm E
x : E
⊢ r • p (-x) = r • p x

Tactic:
simp_rw [map_neg_eq_map]

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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
h0 : spanSingleton R⁰ (mk' K n d) ≠ 0
⊢ mk' K n d = ((algebraMap R K) ↑d)⁻¹ * (algebraMap R K) n

Tactic:
rw [IsFractionRing.mk'_eq_div, div_eq_mul_inv, mul_comm]

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

Goal state before:
pp: m n : ℕ
⊢ ↑↑m - ↑↑n = ↑m - ↑n

Tactic:
coe_natCast,

Goal state after:
m n : ℕ
⊢ ↑m - ↑↑n = ↑m - ↑n
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
refine le_antisymm ?_ <| iSup_le fun i ↦ by grw [← le_iSup]

Goal state after:
case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ a + ⨆ i, f i ≤ ⨆ i, a + f i
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a c : ℝ≥0∞
hca : c < a
⊢ c < ⨆ b, ⨆ (_ : b < a), b

Tactic:
obtain ⟨d, hcd, hdb⟩ := exists_between hca

Goal state after:
a c : ℝ≥0∞
hca : c < a
d : ℝ≥0∞
hcd : c < d
hdb : d < a
⊢ c < ⨆ b, ⨆ (_ : b < a), b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : x ≤ 0
⊢ x.toReal ≤ 0

Tactic:
by
  cases x
  · simp
  · exact toReal_coe _ ▸ EReal.coe_nonpos.mp hx
  · simp

Goal state after: