mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this : ∀ (k : Fin (s.length + 1)), length A ↥(s.toFun k) = ↑↑k * length (ResidueField A) (ResidueField B)
⊢ length A M = ↑↑(Fin.last s.length) * length (ResidueField A) (ResidueField B)

Tactic:
← this,

Goal state after:
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✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this : ∀ (k : Fin (s.length + 1)), length A ↥(s.toFun k) = ↑↑k * length (ResidueField A) (ResidueField B)
⊢ length A M = length A ↥(s.toFun (Fin.last s.length))
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
p q : Submodule A M
h : p ⋖ q
⊢ length B ↥(Submodule.baseChange B q) =
    length B (B ⊗[A] ↥p) + length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
← (toBaseChange.toLinearEquiv B q).length_eq

Goal state after:
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
p q : Submodule A M
h : p ⋖ q
⊢ length B (B ⊗[A] ↥q) = length B (B ⊗[A] ↥p) + length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
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
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this :
  ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B (B ⊗[A] M) = ↑↑(Fin.last s.length) * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
← this,

Goal state after:
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
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this :
  ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B (B ⊗[A] M) = length B ↥(Submodule.baseChange B (s.toFun (Fin.last s.length)))
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ p.ramificationIdx' P ≠ 1 ↔ map f p ≤ P ^ 2

Tactic:
rw [Ideal.ramificationIdx'_eq_find H]

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ Nat.find H ≠ 1 ↔ map f p ≤ P ^ 2
Module: Mathlib.RingTheory.Unramified.Basic

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

Tactic:
hIJ

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

Goal state before:
pp: case mp.refine_2
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}
⊢ 1 - (1 - e) ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
sub_sub_cancel,

Goal state after:
case mp.refine_2
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}
⊢ e ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
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
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l✝ : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l✝ ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
H : ∀ (x : P.Ring), (Ideal.Quotient.mk I) ((aeval (σ ∘ ⇑f)) x) = f ((algebraMap P.Ring A) x)
l : P.Ring ⧸ RingHom.ker (algebraMap P.Ring A) ^ 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ (RingHom.ker (algebraMap P.Ring A) ^ 2) (aeval (σ ∘ ⇑f)) ⋯
this : f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift = (Ideal.Quotient.mkₐ R I).comp l
⊢ ((Ideal.Quotient.mkₐ R I).comp l).comp g = f

Tactic:
← this,

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l✝ : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l✝ ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
H : ∀ (x : P.Ring), (Ideal.Quotient.mk I) ((aeval (σ ∘ ⇑f)) x) = f ((algebraMap P.Ring A) x)
l : P.Ring ⧸ RingHom.ker (algebraMap P.Ring A) ^ 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ (RingHom.ker (algebraMap P.Ring A) ^ 2) (aeval (σ ∘ ⇑f)) ⋯
this : f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift = (Ideal.Quotient.mkₐ R I).comp l
⊢ (f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift).comp g = 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
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
this✝⁵ : IsLocalizedModule p.primeCompl LinearMap.id
this✝⁴ : Module.Finite R (Localization.AtPrime p)
this✝³ : Module.Finite S (Localization.AtPrime p)
this✝² : IsArtinianRing (Localization.AtPrime p)
this✝¹ : IsNoetherianRing S
this✝ : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
q : PrimeSpectrum (Localization.AtPrime p)
hrq :
  PrimeSpectrum.comap (algebraMap S (Localization.Away r)) ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm q) ∈
    ↑(PrimeSpectrum.basicOpen r)
⊢ PrimeSpectrum.comap (algebraMap S (Localization.Away r)) ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm q) ∈
    {{ asIdeal := p, isPrime := inst✝³ }}

Tactic:
obtain rfl : q = IsLocalRing.closedPoint _ := Subsingleton.elim _ _

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
this✝⁵ : IsLocalizedModule p.primeCompl LinearMap.id
this✝⁴ : Module.Finite R (Localization.AtPrime p)
this✝³ : Module.Finite S (Localization.AtPrime p)
this✝² : IsArtinianRing (Localization.AtPrime p)
this✝¹ : IsNoetherianRing S
this✝ : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
hrq :
  PrimeSpectrum.comap (algebraMap S (Localization.Away r))
      ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    ↑(PrimeSpectrum.basicOpen r)
⊢ PrimeSpectrum.comap (algebraMap S (Localization.Away r))
      ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    {{ asIdeal := p, isPrime := inst✝³ }}
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case h₂
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type u_1
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u_1
inst✝ : CommRing B
I J : Ideal B
⊢ I ≤ J →
    (∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
      (∀ [inst : Algebra R (B ⧸ I)],
          Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
        ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R J).comp

Tactic:
hIJ

Goal state after:
case h₂
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type u_1
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u_1
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
⊢ (∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
    (∀ [inst : Algebra R (B ⧸ I)],
        Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
      ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R J).comp
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
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : FormallySmooth R P
f : P →ₐ[R] A
g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2
h : f.kerSquareLift.comp g = AlgHom.id R A
x : A
y : P
hy : (Ideal.Quotient.mk (RingHom.ker f.toRingHom ^ 2)) y = g x
⊢ ∃ a, f a = x

Tactic:
exact ⟨y, congr(f.kerSquareLift $hy).trans congr($h x)⟩

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

Goal state before:
pp: case refine_2
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
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✝ : FormallySmooth R A
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
this : IsScalarTower R B C
b : B
a : A
⊢ f ((b • 1) ⊗ₜ[R] a) = f (b ⊗ₜ[R] a)

Tactic:
smul_eq_mul,

Goal state after:
case refine_2
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
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✝ : FormallySmooth R A
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
this : IsScalarTower R B C
b : B
a : A
⊢ f ((b * 1) ⊗ₜ[R] a) = f (b ⊗ₜ[R] a)
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
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ unramifiedLocus R A ↔ FormallyUnramified R (Localization.Away f)

Tactic:
rw [unramifiedLocus_eq_compl_support, Set.subset_compl_comm,
    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
    ← LocalizedModule.subsingleton_iff_support_subset, Algebra.formallyUnramified_iff]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Subsingleton (LocalizedModule.Away f Ω[A⁄R]) ↔ Subsingleton Ω[Localization.Away f⁄R]
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case hF
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 σ
i : σ
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (P.cotangentSpaceBasis i))

Tactic:
cotangentSpaceBasis_apply

Goal state after:
case hF
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 σ
i : σ
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul.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
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
⊢ ↑(e (a ⊗ₜ[P.Ring] b)) •
      (LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk))
        (c ⊗ₜ[P.Ring] d) =
    0

Tactic:
simp only [LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, SetLike.val_smul,
          LinearMap.coe_restrictScalars, Function.comp_apply, mk_apply, smul_eq_mul, e,
          LinearMap.liftBaseChange_tmul, LinearEquiv.ofBijective_apply]
        have h₂ : b.1 • Cotangent.mk d = 0 := by ext; simp [Cotangent.smul_eq_zero_of_mem _ b.2]
        rw [TensorProduct.smul_tmul', mul_smul, f.mapKer_apply_coe, ← halg,
          algebraMap_smul, ← TensorProduct.tmul_smul, h₂, tmul_zero, smul_zero]

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) (Set.range ⇑(IsScalarTower.toAlgHom R S (Localization.AtPrime q))) = ⊤

Tactic:
IsScalarTower.coe_toAlgHom',

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
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 : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁷ : FormallySmooth R P.Ring
this✝⁶ : FormallySmooth P.Ring (Localization M')
this✝⁵ : FormallySmooth R Q.Ring
this✝⁴ : Module.Flat S T
this✝³ : Algebra P.Ring Q.Ring := inferInstance
this✝² : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : Algebra (Localization M') T := fQ.toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring (Localization M') T
⊢ IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap

Tactic:
by
    rw [isLocalizedModule_iff_isLocalization]
    convert! ‹IsLocalization M T› using 1
    exact Submonoid.map_comap_eq_of_surjective P.algebraMap_surjective _

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
this : (⋃ i ∈ s, S i).indicator 1 a = 1
⊢ (∏ i ∈ s, (1 - (S i).indicator 1 a)) • f a = 0

Tactic:
← this,

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
this : (⋃ i ∈ s, S i).indicator 1 a = 1
⊢ (∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a)) • f a = 0
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 | v.maxPowDividing I ≠ 1} ⊆ {v | ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0}

Tactic:
intro v hv h_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
⊢ False
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ f ↑↑⟨y, hxy⟩ ≤ f ↑q

Tactic:
refine hf_mono (le_trans ?_ hyq.le)

Goal state after:
case refine_2.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ ↑↑⟨y, hxy⟩ ≤ ↑y
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: s : Set ℝ
h : s.OrdConnected
⊢ (toNNReal '' s).OrdConnected

Tactic:
refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩
  rcases le_total y 0 with hy₀ | hy₀
  · rw [mem_Icc, Real.toNNReal_of_nonpos hy₀, nonpos_iff_eq_zero] at hz
    exact ⟨y, hy, (toNNReal_of_nonpos hy₀).trans hz.2.symm⟩
  · lift y to ℝ≥0 using hy₀
    rw [toNNReal_coe] at hz
    exact ⟨z, h.out hx hy ⟨toNNReal_le_iff_le_coe.1 hz.1, hz.2⟩, toNNReal_coe⟩

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

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

Tactic:
coe_sub,

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
⊢ a + b - a = b

Tactic:
simp [ha]

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

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

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

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

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal '' Icc x y = Icc ↑x ↑y

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Icc, WithBot.image_coe_Icc]
  rfl

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

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

Tactic:
simp [ha]

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

Goal state before:
pp: x y z : ℝ≥0∞
h1 : x ≠ 0
h2 : x ≠ ∞
⊢ x * x⁻¹ * y ≤ x * z ↔ y ≤ x * z

Tactic:
ENNReal.mul_inv_cancel h1 h2,

Goal state after:
x y z : ℝ≥0∞
h1 : x ≠ 0
h2 : x ≠ ∞
⊢ 1 * y ≤ x * z ↔ y ≤ x * z
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
i : β
hi : p i
H : f i ≤ ε
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s

Tactic:
exact ⟨i, hi, fun x hx => hε <| lt_of_lt_of_le hx.out H⟩

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

Goal state before:
pp: x : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
m n : ℤ
⊢ x ^ (m + n) = x ^ m * x ^ n

Tactic:
lift x to ℝ≥0 using h'x
  replace hx : x ≠ 0 := by simpa only [Ne, coe_eq_zero] using hx
  simp only [← coe_zpow hx, zpow_add₀ hx, coe_mul]

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0

Tactic:
simp [ha]

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = ∞ → Nonempty ι

Tactic:
simp [ha]

Goal state after: