mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : ¬Algebra.IsAlgebraic F E
⊢ IsPurelyInseparable F E

Tactic:
← Algebra.transcendental_iff_not_isAlgebraic

Goal state after:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.Transcendental F E
⊢ IsPurelyInseparable F E
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(integralBasis K)) ↔ x ∈ (algebraMap (𝓞 K) K).range

Tactic:
by
  simp [integralBasis, Basis.localizationLocalization_span]

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 : Basis ι A B
z : B
i : ι
⊢ ∑ x, (trace A B) (b.equivFun z x • (b i * b x)) = (trace A B) (z * b i)

Tactic:
rw [← _root_.map_sum]

Goal state after:
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ (trace A B) (∑ x, b.equivFun z x • (b i * b x)) = (trace A B) (z * b i)
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
κ : Type w
E : Type z
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Module.Finite K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsAlgClosed E
b : κ → L
inst✝ : Fintype κ
e : κ ≃ (L →ₐ[K] E)
⊢ embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ =
    (embeddingsMatrix K E b).submatrix ⇑(Equiv.refl κ).symm ⇑e.symm.symm *
      (embeddingsMatrix K E b)ᵀ.submatrix ⇑e.symm.symm ⇑(Equiv.refl κ).symm

Tactic:
← submatrix_mul_transpose_submatrix,

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
κ : Type w
E : Type z
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Module.Finite K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsAlgClosed E
b : κ → L
inst✝ : Fintype κ
e : κ ≃ (L →ₐ[K] E)
⊢ (embeddingsMatrix K E b).submatrix _root_.id ⇑?e * (embeddingsMatrix K E b)ᵀ.submatrix (⇑?e) _root_.id =
    (embeddingsMatrix K E b).submatrix ⇑(Equiv.refl κ).symm ⇑e.symm.symm *
      (embeddingsMatrix K E b)ᵀ.submatrix ⇑e.symm.symm ⇑(Equiv.refl κ).symm

case e
K : Type u_4
L : Type u_5
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
κ : Type w
E : Type z
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Module.Finite K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsAlgClosed E
b : κ → L
inst✝ : Fintype κ
e : κ ≃ (L →ₐ[K] E)
⊢ κ ≃ (L →ₐ[K] E)
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)
x : L
hx : ∀ (g : ↥(MulAction.stabilizer G Q)), ((IsFractionRing.stabilizerHom G P Q K L) g) x = x
⊢ f x = x

Tactic:
by
  obtain ⟨_⟩ := nonempty_fintype G
  have : P.IsPrime := Ideal.over_def Q P ▸ Ideal.IsPrime.under A Q
  have : Algebra.IsIntegral A B := Algebra.IsInvariant.isIntegral A B G
  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (B ⧸ Q) x
  obtain ⟨b, a, ha, h⟩ := (Algebra.IsAlgebraic.isAlgebraic (R := A ⧸ P) y).exists_smul_eq_mul x hy
  replace ha : algebraMap (A ⧸ P) L a ≠ 0 := by
    rwa [Ne, algebraMap_apply (A ⧸ P) K L, algebraMap_eq_zero_iff, algebraMap_eq_zero_iff]
  replace hy : algebraMap (B ⧸ Q) L y ≠ 0 :=
    mt (algebraMap_eq_zero_iff (B ⧸ Q) L).mp (nonZeroDivisors.ne_zero hy)
  replace h : algebraMap (B ⧸ Q) L x / algebraMap (B ⧸ Q) L y =
      algebraMap (B ⧸ Q) L b / algebraMap (A ⧸ P) L a := by
    rw [mul_comm, Algebra.smul_def, mul_comm] at h
    rw [div_eq_div_iff hy ha, ← map_mul, ← h, map_mul, ← algebraMap_apply]
  simp only [h, map_div₀, algebraMap_apply (A ⧸ P) K L, AlgEquiv.commutes] at hx ⊢
  simp only [← algebraMap_apply, div_left_inj' ha] at hx ⊢
  exact fixed_of_fixed1 G P Q K L f b (fun g ↦ IsFractionRing.injective (B ⧸ Q) L
    ((IsFractionRing.fieldEquivOfAlgEquiv_algebraMap K L L
      (Ideal.Quotient.stabilizerHom Q P G g) b).symm.trans (hx g)))

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

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : (fun x ↦ g ^ x) n ^ (Nat.card F / 2) = 1
⊢ IsSquare ((fun x ↦ g ^ x) n)

Tactic:
have key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2) := by
      rw [← pow_mul] at h
      rw [hodd, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
      apply orderOf_dvd_of_pow_eq_one h

Goal state after:
case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : (fun x ↦ g ^ x) n ^ (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)
⊢ IsSquare ((fun x ↦ g ^ x) n)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mp
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) → ∃ r, a = r * r

pp: case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = r * r) → ∃ r, a = ↑r * ↑r

Tactic:
· rintro ⟨y, hy⟩; exact ⟨y, hy⟩

Goal state after:
case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = r * r) → ∃ r, a = ↑r * ↑r
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
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) = mk' S 1 x

Tactic:
rw [← (IsLocalization.map_units S x).mul_left_inj]

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
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) * (algebraMap R S) ↑x = mk' S 1 x * (algebraMap R S) ↑x
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ zeroLocus ↑I ∩ closedPoints (PrimeSpectrum R) ⊆ zeroLocus ↑I.jacobson

Tactic:
rintro x ⟨hx : I ≤ x.asIdeal, hx'⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
x : PrimeSpectrum R
hx : I ≤ x.asIdeal
hx' : x ∈ closedPoints (PrimeSpectrum R)
⊢ x ∈ zeroLocus ↑I.jacobson
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
inst✝⁴ : p.IsPrime
inst✝³ : q.IsPrime
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsIntegral A B
this✝ : Algebra.IsIntegral (A ⧸ p) (B ⧸ q)
this : Algebra (A ⧸ p) q.ResidueField :=
  ((algebraMap (B ⧸ q) q.ResidueField).comp (algebraMap (A ⧸ p) (B ⧸ q))).toAlgebra
⊢ Algebra.IsAlgebraic p.ResidueField q.ResidueField

Tactic:
have : IsScalarTower (A ⧸ p) (B ⧸ q) q.ResidueField := .of_algebraMap_eq' rfl

Goal state after:
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
inst✝⁴ : p.IsPrime
inst✝³ : q.IsPrime
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsIntegral A B
this✝¹ : Algebra.IsIntegral (A ⧸ p) (B ⧸ q)
this✝ : Algebra (A ⧸ p) q.ResidueField :=
  ((algebraMap (B ⧸ q) q.ResidueField).comp (algebraMap (A ⧸ p) (B ⧸ q))).toAlgebra
this : IsScalarTower (A ⧸ p) (B ⧸ q) q.ResidueField
⊢ Algebra.IsAlgebraic p.ResidueField q.ResidueField
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✝ : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : P.ResidueField ⊗[R] T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
a : P.ResidueField
b : T
⊢ (AlgHom.restrictScalars S f).toLinearMap (a ⊗ₜ[R] b) = a ⊗ₜ[S] b

Tactic:
by simp [f]

Goal state after:
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
f : Localization.AtPrime Q →ₐ[R] Localization.AtPrime P := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ P.primeCompl
⊢ f.toRingHom ((algebraMap S (Localization.AtPrime Q)) x) =
    IsLocalization.mk' (Localization.AtPrime P) x ⟨s, hs⟩ * f ((algebraMap S (Localization.AtPrime Q)) s)

Tactic:
by simp [f]

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 : (Q.ofComp P).toAlgHom (x - y) = 0
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
← RingHom.mem_ker,

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 ∈ RingHom.ker (Q.ofComp P).toAlgHom
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range
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.Injective ⇑(LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))

Tactic:
rw [← compEquiv_symm_inr]

Goal state after:
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.Injective
    ⇑(↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
Module: Mathlib.RingTheory.Unramified.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Ideal R
inst✝⁴ : P.IsPrime
Q : Ideal A
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
inst✝¹ : IsUnramifiedAt R Q
Q' : Ideal (P.Fiber A)
inst✝ : Q'.IsPrime
hQ' : Q = Ideal.comap TensorProduct.includeRight.toRingHom Q'
f₀ : Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q' :=
  Localization.localAlgHom Q Q' TensorProduct.includeRight hQ'
hf₀ : Function.Surjective ⇑f₀
f : P.Fiber (Localization.AtPrime Q) →ₐ[P.ResidueField] Localization.AtPrime Q' :=
  TensorProduct.lift (ofId P.ResidueField (Localization.AtPrime Q')) f₀ ⋯
x : Localization.AtPrime Q
⊢ f (1 ⊗ₜ[R] x) = f₀ x

Tactic:
by simp [f]

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
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝³ : FiniteType K A
this✝² : Module.Finite K (Localization.AtPrime Q)
this✝¹ : IsField (Localization.AtPrime Q)
this✝ : Field (Localization.AtPrime Q) := this✝¹.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : (aeval x).toRingHom (m * q) = 0
⊢ ¬q ^ 2 ∣ p

Tactic:
← RingHom.mem_ker,

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝³ : FiniteType K A
this✝² : Module.Finite K (Localization.AtPrime Q)
this✝¹ : IsField (Localization.AtPrime Q)
this✝ : Field (Localization.AtPrime Q) := this✝¹.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : m * q ∈ RingHom.ker (aeval x).toRingHom
⊢ ¬q ^ 2 ∣ p
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)
      ↑(Finset.image (⇑(IsScalarTower.toAlgHom R S (Localization.AtPrime q)).toLinearMap) s) =
    ⊤

Tactic:
rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs,
    Submodule.map_top, LinearMap.coe_range, AlgHom.coe_toLinearMap, IsScalarTower.coe_toAlgHom',
    ← top_le_iff]

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) (Set.range ⇑(algebraMap S (Localization.AtPrime q)))
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
⊢ IsLocalizedModule M (map R R S T)

Tactic:
rw [isLocalizedModule_iff_isBaseChange M T]
  change Function.Bijective ((Algebra.H1Cotangent.map R R S T).liftBaseChange T)
  rw [← tensorH1CotangentOfIsLocalization_toLinearMap R T M]
  exact (tensorH1CotangentOfIsLocalization R T M).bijective

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:

Tactic:
∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a
      = ∑ a, f a - ∑ a ∈ s.biUnion S, f a := by
      rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
    _ = ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a
          + ∑ t ∈ s.powerset.filter (·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a := by
      simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
        sub_eq_add_neg, pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a := sum_filter_not_add_sum_filter ..

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

Goal state before:
pp: case inl
h₁ : BddBelow ∅
h₂ : BddAbove ∅
⊢ sInf ∅ ≤ sSup ∅

pp: case inr
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : s.Nonempty
⊢ sInf s ≤ sSup s

Tactic:
· rw [sInf_empty, sSup_empty]

Goal state after:
case inr
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : s.Nonempty
⊢ sInf s ≤ sSup s
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)
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

Tactic:
have h_not_dvd := Ideal.finprod_not_dvd v I 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
h_not_dvd :
  ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (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.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(const abs (sSup s) - f) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 + ε / 2 ≤ sSup s - ↑f j

Tactic:
add_halves

Goal state after:
case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(const abs (sSup s) - f) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ sSup s - ↑f j
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(f - const abs (sSup s)) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 + ε / 2 ≤ ↑f j - sSup s

Tactic:
add_halves

Goal state after:
case refine_2
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(f - const abs (sSup s)) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ ↑f j - sSup s
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) = ↑I

Tactic:
conv_rhs => rw [← Ideal.finprod_heightOneSpectrum_factorization hI]
  rw [FractionalIdeal.coeIdeal_finprod R⁰ K (le_refl _)]
  simp_rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FractionalIdeal.coeIdeal_pow,
    zpow_natCast]

Goal state after:
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case refine_2
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ c ∈ sᶜ.ordConnectedComponent y

Tactic:
refine subset_ordConnectedComponent left_mem_uIcc hxy ?_

Goal state after:
case refine_2
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ c ∈ [[y, x]]
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ i, ⨆ (_ : p i), ⨆ i_1, ⨆ (_ : q i_1), f i + g i_1 ≤ a

Tactic:
exact iSup₂_le fun i hi => iSup₂_le (h i hi)

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

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

Tactic:
refine le_antisymm (iSup₂_le fun b hb ↦ hb.le) ?_
  refine le_of_forall_lt fun c hca ↦ ?_
  obtain ⟨d, hcd, hdb⟩ := exists_between hca
  exact hcd.trans_le <| le_iSup₂_of_le d hdb le_rfl

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

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ↑y = Ioo x y

Tactic:
simp_rw [← Ioi_inter_Iio]

Goal state after:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ↑y) = Ioi x ∩ Iio y
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
rw [← coe_ne_zero] at hb

Goal state after:
case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : ↑b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case hp₁
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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
⊢ count K v (I * I') = 0

Tactic:
by_cases h : I ≠ 0 ∧ I' ≠ 0
    · rw [count_mul' K v, if_pos h, hI, hI', add_zero]
    · rw [count_mul' K v, if_neg h]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | dist p.1 p.2 < f i} ⊆ s

Tactic:
rintro ⟨ε, ε₀, hε⟩
    rcases hf ε₀ with ⟨i, hi, H⟩
    exact ⟨i, hi, fun x (hx : _ < _) => hε <| lt_of_lt_of_le hx H⟩

Goal state after: