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

Goal state before:
pp: case intro
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✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
b : B
M : A[X]
a : A
ha1 : ∀ (g : G), g • (algebraMap A B) a = (algebraMap A B) a
ha2 : (algebraMap A B) a ∉ Q
hb :
  ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then (algebraMap A B) a * b₀ else 0)
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) =
      if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a * b₀)) else X
key :
  (algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) *
      f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) =
    (algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) *
      (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
⊢ (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a)) ≠ 0

Tactic:
Ne,

Goal state after:
case intro
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✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
b : B
M : A[X]
a : A
ha1 : ∀ (g : G), g • (algebraMap A B) a = (algebraMap A B) a
ha2 : (algebraMap A B) a ∉ Q
hb :
  ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then (algebraMap A B) a * b₀ else 0)
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) =
      if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a * b₀)) else X
key :
  (algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) *
      f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) =
    (algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) *
      (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
⊢ ¬(algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a)) = 0
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✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
ha : a ≠ 0
h : a • x = y * b
⊢ (algebraMap (A ⧸ P) L) a ≠ 0

Tactic:
Ne,

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✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
ha : a ≠ 0
h : a • x = y * b
⊢ ¬(algebraMap (A ⧸ P) L) a = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ a ^ 2 + b ^ 2 - x = 0

Tactic:
simpa only [f, g, eval_C, eval_X, eval_pow, eval_sub, ← add_sub_assoc] using hab

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
Fintype.card_units,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Fintype.card (ZMod p) - 1 = p - 1
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this✝ : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis ι R ↥N := smithNormalFormBotBasis b h
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (b'.repr x) i
N' : Submodule R (ι → R) := pi Set.univ fun i ↦ R ∙ a i
this : map (↑b'.equivFun) N = N'
⊢ ((ι → R) ⧸ N') ≃ₗ[R] (i : ι) → R ⧸ Ideal.span {smithNormalFormCoeffs b h i}

Tactic:
exact Submodule.quotientPi (show _ → Submodule R R from fun i => span R ({a i} : Set R))

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

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k ≃ₐ[A ⧸ P] k
f : B ⧸ Q →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective ⇑f
τ₁ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₁ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₁ x) = σ ((algebraMap (B ⧸ Q) k) x)
τ₂ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₂ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₂ x) = σ.symm ((algebraMap (B ⧸ Q) k) x)
x y : B
e : (mk Q) y = τ₂ ((mk Q) x)
⊢ (algebraMap (B ⧸ Q) k) (τ₁ (τ₂ ((mk Q) x))) = σ (σ.symm ((algebraMap (B ⧸ Q) k) ((mk Q) x)))

Tactic:
rw [← h₂, ← e, h₁]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ P ^ i
⊢ P ^ (i + 1) ≠ span {a} ⊔ P ^ (i + 1)

Tactic:
contrapose a_notMem with this

Goal state after:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ a ∈ P ^ (i + 1)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
this : (span {↑(absNorm I)}).IsPrime
⊢ span {↑(absNorm I)} ≠ ⊥

Tactic:
Ne,

Goal state after:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
this : (span {↑(absNorm I)}).IsPrime
⊢ ¬span {↑(absNorm I)} = ⊥
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case pos
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ S
inst✝² : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S ↥I
inst✝ : AddEquivClass E S ↥I
e : E
hI : I = ⊥
⊢ (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I

Tactic:
subst hI
    have : (1 : S) ≠ 0 := one_ne_zero
    have : (1 : S) = 0 := EquivLike.injective e (Subsingleton.elim _ _)
    contradiction

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
I : Ideal S
hI : I ≠ ⊥
⊢ absNorm I ≠ 0

Tactic:
Ne,

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
⊢ ¬absNorm I = 0
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
z : S
⊢ ∃ r m, z = r • ↑((toInvSubmonoid M S) m)

Tactic:
rcases IsLocalization.surj M z with ⟨⟨r, m⟩, e : z * _ = algebraMap R S r⟩
  refine ⟨r, m, ?_⟩
  rw [Algebra.smul_def, ← e, mul_assoc]
  simp

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
simp_rw [isLocallyClosed_iff_isOpen_coborder, coborder, isOpen_compl_iff,
      Set.nonempty_iff_ne_empty]
    intro H Z hZ hZ' e
    have : Z ⊆ closure Z \ Z := by
      refine subset_closure.trans ?_
      nth_rw 1 [← H isClosed_closure]
      rw [hZ'.closure_subset_iff, Set.subset_sdiff, Set.disjoint_iff, Set.inter_assoc,
        Set.inter_comm _ Z, e]
      exact ⟨Set.inter_subset_left, Set.inter_subset_right⟩
    rw [Set.subset_sdiff, disjoint_self, Set.bot_eq_empty] at this
    exact hZ this.2

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R✝
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R✝ A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R✝ B
inst✝⁶ : IsScalarTower R✝ A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
R : Type u_4
k : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsLocalRing R
inst✝² : Field k
inst✝¹ : Algebra R k
inst✝ : Module.Finite R k
⊢ Ideal.comap (algebraMap R k) ⊥ = maximalIdeal R

Tactic:
rw [← eq_maximalIdeal (Algebra.ker_algebraMap_isMaximal_of_isIntegral R k), RingHom.ker]

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
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
⊢ e ∣ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1

Tactic:
rw [← Ideal.mem_span_singleton, ← he₂]
        exact Ideal.subset_span ⟨s, rfl⟩

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✝³ : Algebra S T
inst✝² : IsScalarTower R S T
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : T
⊢ p ⊗ₜ[S] s ∈ ↑(↑S (Algebra.linearMap P.ResidueField (P.Fiber T))).range

Tactic:
obtain ⟨s, t, rfl⟩ := IsLocalization.exists_mk'_eq M s

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
⊢ p ⊗ₜ[S] IsLocalization.mk' T s t ∈ ↑(↑S (Algebra.linearMap P.ResidueField (P.Fiber T))).range
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✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
j : I
hj : j ∉ f.support.biUnion fun i ↦ (a i).support
⊢ b.repr (f.sum fun i y ↦ (a i) j • y) = 0

Tactic:
simp only [Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_exists, not_and,
      not_not] at hj

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
j : I
hj : ∀ (x : I), ¬f x = 0 → (a x) j = 0
⊢ b.repr (f.sum fun i y ↦ (a i) j • y) = 0
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✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := ⋯
sA : ↥A := ⋯
f : Localization.Away sA →+* T := ⋯
this✝⁶ : Algebra (Localization.Away sA) T := ⋯
this✝⁵ : Algebra (↥A) (Localization.Away sA) := ⋯
this✝⁴ : SMul (↥A) (Localization.Away sA) := ⋯
this✝³ : MulAction (↥A) (Localization.Away sA) := ⋯
this✝² : IsScalarTower R (↥A) (Localization.Away sA)
this✝¹ : IsScalarTower (↥A) (Localization.Away sA) T
this✝ : IsScalarTower R (Localization.Away sA) T
x : S
n : ℕ
this : IsIntegral (Localization.Away sA) ((algebraMap S T) x)
⊢ (algebraMap S T) x = (sA • Localization.Away.invSelf sA) ^ n • (algebraMap S T) x

Tactic:
simp [Algebra.smul_def, -map_pow, Localization.Away.invSelf, Localization.mk_eq_mk']

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

Goal state before:
pp: case h1
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 σ
⊢ Extension.Cotangent.map (Q.ofComp P).toExtensionHom ∘ₗ
      LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom) =
    0

Tactic:
LinearMap.liftBaseChange_comp,

Goal state after:
case h1
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 σ
⊢ LinearMap.liftBaseChange T
      (↑S (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) ∘ₗ
        Extension.Cotangent.map (Q.toComp P).toExtensionHom) =
    0
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case e'_4
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ Extension.H1Cotangent.map (W.defaultHom (Q.comp P)).toExtensionHom ∘ₗ
      LinearMap.liftBaseChange T (Extension.H1Cotangent.map g.toExtensionHom) =
    LinearMap.liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)

Tactic:
LinearMap.liftBaseChange_comp,

Goal state after:
case e'_4
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ LinearMap.liftBaseChange T
      (↑S (Extension.H1Cotangent.map (W.defaultHom (Q.comp P)).toExtensionHom) ∘ₗ
        Extension.H1Cotangent.map g.toExtensionHom) =
    LinearMap.liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : (Generators.self R T).toExtension.Hom Q :=
  { toRingHom := (MvPolynomial.aeval Q.σ).toRingHom, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
⊢ (Extension.H1Cotangent.map
        {
          toRingHom :=
            algebraMap (Generators.self R S).toExtension.Ring
              (Localization (Submonoid.comap (algebraMap (Generators.self R S).toExtension.Ring S) M)),
          toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
      x =
    (↑S (Extension.H1Cotangent.map f))
      ((Extension.H1Cotangent.map ((Generators.self R S).defaultHom (Generators.self R T)).toExtensionHom) x)

Tactic:
← LinearMap.comp_apply,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : (Generators.self R T).toExtension.Hom Q :=
  { toRingHom := (MvPolynomial.aeval Q.σ).toRingHom, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
⊢ (Extension.H1Cotangent.map
        {
          toRingHom :=
            algebraMap (Generators.self R S).toExtension.Ring
              (Localization (Submonoid.comap (algebraMap (Generators.self R S).toExtension.Ring S) M)),
          toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
      x =
    (↑S (Extension.H1Cotangent.map f) ∘ₗ
        Extension.H1Cotangent.map ((Generators.self R S).defaultHom (Generators.self R T)).toExtensionHom)
      x
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case h
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsGLB s (-Classical.choose ⋯)

Tactic:
← isLUB_neg

Goal state after:
case h
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsLUB (-s) (Classical.choose ⋯)
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0

Tactic:
have h_supp : {v : HeightOneSpectrum R | ¬((Associates.mk v.asIdeal).count
      (Associates.mk I).factors : ℤ) = 0} = {v : HeightOneSpectrum R | v.asIdeal ∣ I} := by
    ext v
    simp_rw [Int.natCast_eq_zero]
    exact Associates.count_ne_zero_iff_dvd hI v.irreducible
  rw [Filter.eventually_cofinite, h_supp]
  exact Ideal.finite_factors hI

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ
s✝ : Set ℝ
a : ℝ
s : Set ℝ
hs : ¬BddAbove s
⊢ sSup s = sSup ∅

Tactic:
simp [hs, sSup_def]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) ≠ 1}.Finite

Tactic:
Ne,

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
⊢ {x | ¬↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) = 1}.Finite
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
⊢ {x | (↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors))⁻¹ ≠ 1}.Finite

Tactic:
Ne,

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
⊢ {x | ¬(↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors))⁻¹ = 1}.Finite
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : ¬HasFiniteMulSupport fun v ↦ v.maxPowDividing I
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

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

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ x⁻¹ ≠ 0

Tactic:
Ne,

Goal state after:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ ¬x⁻¹ = 0