mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos
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 = ⊤
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)

Tactic:
← length_compositionSeries s hs_bot hs_top

Goal state after:
case pos
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 = ⊤
⊢ length A M = ↑s.length * length (ResidueField A) (ResidueField B)
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
q : Ideal S
inst✝² : q.LiesOver p
inst✝¹ : p.IsMaximal
inst✝ : q.IsMaximal
this✝ : Field (R ⧸ p) := Quotient.field p
this : Field (S ⧸ q) := Quotient.field q
⊢ q.inertiaDeg R = Module.finrank (R ⧸ p) (S ⧸ q)

Tactic:
exact inertiaDeg_eq_of_isFractionRing p q (R ⧸ p) (S ⧸ q)

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Length

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

Tactic:
← length_compositionSeries s hs_bot hs_top

Goal state after:
case pos
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 = ⊤
⊢ length B (B ⊗[A] M) = ↑s.length * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case refine_1
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ normalizedFactors (P ^ Multiset.count P (normalizedFactors (map f p))) ≤ normalizedFactors (map f p)

Tactic:
normalizedFactors_pow,

Goal state after:
case refine_1
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ Multiset.count P (normalizedFactors (map f p)) • normalizedFactors P ≤ normalizedFactors (map f p)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case refine_2
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ¬normalizedFactors (P ^ (Multiset.count P (normalizedFactors (map f p)) + 1)) ≤ normalizedFactors (map f p)

Tactic:
normalizedFactors_pow,

Goal state after:
case refine_2
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ¬(Multiset.count P (normalizedFactors (map f p)) + 1) • normalizedFactors P ≤ normalizedFactors (map f p)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I
hntq : ¬⊤ ≤ Q
⊢ Multiset.count Q (normalizedFactors (map (algebraMap S T) P ^ Multiset.count P (normalizedFactors (map f p)))) +
      Multiset.count Q (normalizedFactors (map (algebraMap S T) I)) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))

Tactic:
normalizedFactors_pow,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I
hntq : ¬⊤ ≤ Q
⊢ Multiset.count Q (Multiset.count P (normalizedFactors (map f p)) • normalizedFactors (map (algebraMap S T) P)) +
      Multiset.count Q (normalizedFactors (map (algebraMap S T) I)) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case e_g
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
i j : I
s : S
⊢ (((a j) i • b.repr s).sum fun j z ↦ z • b j ⊗ₜ[R] b i) = (b.repr s).sum fun j_1 z ↦ (a j) i • z • b j_1 ⊗ₜ[R] b i

Tactic:
rw [Finsupp.sum_smul_index]

Goal state after:
case e_g
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
i j : I
s : S
⊢ ((b.repr s).sum fun i_1 a_1 ↦ ((a j) i * a_1) • b i_1 ⊗ₜ[R] b i) =
    (b.repr s).sum fun j_1 z ↦ (a j) i • z • b j_1 ⊗ₜ[R] b i

case e_g
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
i j : I
s : S
⊢ ∀ (i_1 : I), 0 • b i_1 ⊗ₜ[R] b i = 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✝ : QuasiFinite R S
f : S →ₐ[R] T
H : ∀ (x : T), ∃ s, IsUnit (f s) ∧ x * f s ∈ f.range
⊢ QuasiFinite R T

Tactic:
by
  let φ : Localization ((IsUnit.submonoid T).comap f) →ₐ[R] T :=
    IsLocalization.liftAlgHom (M := (IsUnit.submonoid T).comap f) (f := f)
      (by simp [IsUnit.mem_submonoid_iff])
  suffices Function.Surjective φ from .of_surjective_algHom φ this
  intro x
  obtain ⟨s, hs, t, ht⟩ := H x
  refine ⟨IsLocalization.mk' (M := (IsUnit.submonoid T).comap f) _ t ⟨s, hs⟩, ?_⟩
  simpa [φ, IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul, IsUnit.coe_liftRight]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case h
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 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
⊢ Submodule.span R ↑(Finset.image₂ (fun i j ↦ f i * b j) f.support f.support) = ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
case h
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
⊢ ⊤ ≤ Submodule.span R ↑(Finset.image₂ (fun i j ↦ f i * b j) f.support f.support)
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case e'_1
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
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (∃ i, mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔ ∃ l, ↑P (mapBaseChange R P A) ∘ₗ l = LinearMap.id

Tactic:
rw [← (LinearMap.extendScalarsOfSurjectiveEquiv hf).exists_congr_right]
    simp [LinearMap.ext_iff]

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

Goal state before:
pp: R : Type u_4
inst✝⁸ : CommRing R
A : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R A
inst✝ : FormallySmooth R B
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra A C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[A] C ⧸ I
algInst✝ : Algebra R C := ((algebraMap A C).comp (algebraMap R A)).toAlgebra
scalarTowerInst✝ : IsScalarTower R A C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R C))
g : B →ₐ[R] C
hg : (Ideal.Quotient.mkₐ R I).comp g = AlgHom.restrictScalars R f
⊢ ∃ a, (Ideal.Quotient.mkₐ A I).comp a = f

Tactic:
suffices g.comp (IsScalarTower.toAlgHom R A B) = IsScalarTower.toAlgHom R A C from
    ⟨{ __ := g, commutes' x := congr($this x) }, AlgHom.ext fun x ↦ congr($hg x)⟩

Goal state after:
R : Type u_4
inst✝⁸ : CommRing R
A : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R A
inst✝ : FormallySmooth R B
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra A C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[A] C ⧸ I
algInst✝ : Algebra R C := ((algebraMap A C).comp (algebraMap R A)).toAlgebra
scalarTowerInst✝ : IsScalarTower R A C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R C))
g : B →ₐ[R] C
hg : (Ideal.Quotient.mkₐ R I).comp g = AlgHom.restrictScalars R f
⊢ g.comp (IsScalarTower.toAlgHom R A B) = IsScalarTower.toAlgHom R A C
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u_4
Rₘ : Type u_6
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x✝¹ : CommRing Q
x✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
⊢ (Ideal.Quotient.mk I) ((algebraMap R Q) ↑x) = f ((algebraMap R Rₘ) ↑x)

Tactic:
simp only [Ideal.Quotient.mk_algebraMap, AlgHom.commutes]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this : Nontrivial (L ⊗[K] L)
⊢ (algebraMap K L).range = ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this : Nontrivial (L ⊗[K] L)
⊢ ⊤ ≤ (algebraMap K L).range
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 σ
⊢ Extension.Cotangent.map (Q.ofComp P).toExtensionHom ∘ₗ Extension.h1Cotangentι =
    Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom

pp: case h
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 ⇑Extension.h1Cotangentι

Tactic:
· ext x; rfl

Goal state after:
case h
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 ⇑Extension.h1Cotangentι
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 σ
⊢ Set.range ⇑(Extension.H1Cotangent.map (Q.toComp P).toExtensionHom) ⊆
    ↑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker

Tactic:
Set.range_subset_iff

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 σ
⊢ ∀ (y : P.toExtension.H1Cotangent),
    (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom) y ∈
      ↑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker
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 σ
z : T ⊗[S] P.toExtension.H1Cotangent
⊢ (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((LinearMap.lTensor T Extension.h1Cotangentι) z) ∈
    (Q.comp P).toExtension.cotangentComplex.ker

Tactic:
induction z with

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
r : PrimeSpectrum (p.Fiber S) := (PrimeSpectrum.primesOverOrderIsoFiber R S p) (primesOver.mk p q)
⊢ q = ↑((PrimeSpectrum.primesOverOrderIsoFiber R S p).symm r)

Tactic:
OrderIso.symm_apply_apply

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
r : PrimeSpectrum (p.Fiber S) := (PrimeSpectrum.primesOverOrderIsoFiber R S p) (primesOver.mk p q)
⊢ q = ↑(primesOver.mk p q)
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 σ
inst✝ : Flat S T
x : (Q.comp P).toExtension.Cotangent
x_in : x ∈ (Q.comp P).toExtension.cotangentComplex.ker
hx : ⟨x, x_in⟩ ∈ (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker
⊢ (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x = 0

Tactic:
simpa [← Extension.h1Cotangentι_injective.eq_iff] using hx

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

Tactic:
· obtain ⟨i, hi⟩ := hs
    have ha : a ∉ S i := by aesop
    exact prod_eq_zero hi <| by simp [*, -coe_biUnion]

Goal state after:
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
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
⊢ v.maxPowDividing I = 1

Tactic:
IsDedekindDomain.HeightOneSpectrum.maxPowDividing,

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
⊢ v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors = 1
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ¬BddAbove (toReal '' s)

Tactic:
contrapose H

Goal state after:
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove (toReal '' s)
⊢ BddAbove s
Module: Mathlib.RingTheory.DedekindDomain.Factorization

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

Tactic:
finprod_def

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

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal

Tactic:
rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]

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

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ |x| = x

Tactic:
abs_of_nonneg h

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ x = x
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) =
    ∏ᶠ (a : HeightOneSpectrum R), ↑(a.maxPowDividing I)

Tactic:
IsDedekindDomain.HeightOneSpectrum.maxPowDividing,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) =
    ∏ᶠ (a : HeightOneSpectrum R), ↑(a.asIdeal ^ (Associates.mk a.asIdeal).count (Associates.mk I).factors)
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case pos
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
⊢ f ↑g < f 1

Tactic:
exact hf hu1

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

Goal state before:
pp: b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑(a + (c - a)) < b

Tactic:
add_tsub_cancel_of_le ac.le

Goal state after:
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑c < b
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)

Tactic:
· have : Nonempty s := hs.to_subtype
            refine ciSup_le fun p ↦ (map_add_le_max p.1 x y).trans ?_
            gcongr
            all_goals
              apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p
              simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

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

Goal state before:
pp: case inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
rcases eq_or_lt_of_le (le_top : q ≤ ∞) with (rfl | hq)

Goal state after:
case inr.inl
p : ℝ≥0∞
hp : 0 < p
hpq : p ≤ ∞
⊢ p = 0 ∧ ∞ = 0 ∨
    p = 0 ∧ ∞ = ∞ ∨
      p = 0 ∧ 0 < ∞.toReal ∨ p = ∞ ∧ ∞ = ∞ ∨ 0 < p.toReal ∧ ∞ = ∞ ∨ 0 < p.toReal ∧ 0 < ∞.toReal ∧ p.toReal ≤ ∞.toReal

case inr.inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ∞
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ ↑y ∈ s.ordConnectedComponent (s.ordConnectedProj y)

Tactic:
ordConnectedComponent_ordConnectedProj,

Goal state after:
case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ ↑y ∈ s.ordConnectedComponent ↑y
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ ∞.toNNReal = 0

Tactic:
toNNReal_top

Goal state after:
case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ 0 = 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
simp_rw [iSup_add, add_iSup]; exact iSup₂_le h

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

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

Tactic:
rw [toENNReal, if_neg (fun h ↦ ?_)]

Goal state after:
x : EReal
hx : x ≤ 0
⊢ ENNReal.ofReal x.toReal = 0

x : EReal
hx : x ≤ 0
h : x = ⊤
⊢ False
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
v w : HeightOneSpectrum R
hw : w ≠ v
⊢ count K v ↑w.asIdeal = 0

Tactic:
by
  have hw_fact : (w.asIdeal : FractionalIdeal R⁰ K) =
      spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal := by
    rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]
  have hw_ne_zero : (w.asIdeal : FractionalIdeal R⁰ K) ≠ 0 :=
    coeIdeal_ne_zero.mpr w.ne_bot
  have hv : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible
  have hw' : Irreducible (Associates.mk w.asIdeal) := by apply w.associates_irreducible
  rw [count_well_defined K v hw_ne_zero hw_fact, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero hv, ofNat_zero, sub_zero,
    natCast_eq_zero, ← pow_one (Associates.mk w.asIdeal), Associates.factors_prime_pow hw',
    Associates.count_some hv, Multiset.replicate_one, Multiset.count_eq_zero,
    Multiset.mem_singleton]
  simp only [Subtype.mk.injEq]
  rw [Associates.mk_eq_mk_iff_associated, associated_iff_eq, ← HeightOneSpectrum.ext_iff]
  exact Ne.symm hw

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

Goal state before:
pp: a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd✝ : d < a * b
a' : ℝ≥0∞
ha' : a' < a
hd : d < a' * b
⊢ d ≤ c

Tactic:
obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd

Goal state after:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd✝¹ : d < a * b
a' : ℝ≥0∞
ha' : a' < a
hd✝ : d < a' * b
b' : ℝ≥0∞
hb' : b' < b
hd : d < a' * b'
⊢ d ≤ c