mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ invFun p (toFun p (Quotient.mk x')) = Quotient.mk x'

Tactic:
by
    dsimp only [toFun, invFun]
    rw [quotientPiLift_mk p, funext fun i => (mkQ_apply (p i) (x' i)), piQuotientLift_mk p,
      lsum_single, id_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: E : Type u_1
inst✝² : AddCommGroup E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ : Basis ι ℤ ↥(toIntSubmodule L₁)
b₂ : Basis ι ℤ ↥(toIntSubmodule L₂)
⊢ (L₁.addSubgroupOf L₂).index = (b₂.det fun i ↦ ⟨↑(b₁ i), ⋯⟩).natAbs

Tactic:
index_eq_natAbs_det b₂ _ (b₁.map (addSubgroupOfEquivOfLe H).toIntLinearEquiv.symm)

Goal state after:
E : Type u_1
inst✝² : AddCommGroup E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ : Basis ι ℤ ↥(toIntSubmodule L₁)
b₂ : Basis ι ℤ ↥(toIntSubmodule L₂)
⊢ (b₂.det fun x ↦ ↑((b₁.map (addSubgroupOfEquivOfLe H).toIntLinearEquiv.symm) x)).natAbs =
    (b₂.det fun i ↦ ⟨↑(b₁ i), ⋯⟩).natAbs
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsNoetherianRing R
this : Function.Injective asIdeal
⊢ (asIdeal '' {x | IsMin x}).Finite

Tactic:
isMin_iff

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsNoetherianRing R
this : Function.Injective asIdeal
⊢ (asIdeal '' {x | x.asIdeal ∈ minimalPrimes R}).Finite
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
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
hI' : IsUnit ⊤
hI : p ∣ ↑(absNorm ⊤)
⊢ p ∣ 1

Tactic:
by simpa using hI

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
x : X
⊢ x ∈ f ⁻¹' closedPoints Y ↔ x ∈ closedPoints X

Tactic:
simp [mem_closedPoints_iff, ← Set.image_singleton, hf.isClosed_iff_image_isClosed]

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsArtinianRing R ↔ Ring.KrullDimLE 0 R

Tactic:
rwa [isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, and_iff_right]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hle : map f p ≤ P ^ n
hgt : ¬map f p ≤ P ^ (n + 1)
⊢ p.ramificationIdx' P = n

Tactic:
let Q : ℕ → Prop := fun m => ∀ k : ℕ, map f p ≤ P ^ k → k ≤ m
  have : Q n := by
    intro k hk
    refine le_of_not_gt fun hnk => ?_
    exact hgt (hk.trans (Ideal.pow_le_pow_right hnk))
  rw [ramificationIdx'_eq_find ⟨n, this⟩]
  refine le_antisymm (Nat.find_min' _ this) (le_of_not_gt fun h : Nat.find _ < n => ?_)
  obtain this' := Nat.find_spec ⟨n, this⟩
  exact h.not_ge (this' _ hle)

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
I : Ideal R
hI : IsUnit I
h : I ≠ ⊥
⊢ I = ⊤

Tactic:
by simpa using hI

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

Goal state before:
pp: case mp
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
⊢ FormallyUnramified R A →
    ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intros

Goal state after:
case mp
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Small.{w, u} A
a✝ : FormallyUnramified R A
B✝ : Type w
inst✝¹ : CommRing B✝
inst✝ : Algebra R B✝
I✝ : Ideal B✝
x✝ : I✝ ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I✝).comp
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
⊢ ∀ ⦃S : Type w⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [inst_1 : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst_1 : Algebra R (S ⧸ I)],
            Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst_1 : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R J).comp

Tactic:
intro B _ I J hIJ h₁ h₂ _ g₁ g₂ e
    apply h₁
    apply h₂
    ext x
    replace e := AlgHom.congr_fun e x
    dsimp only [AlgHom.comp_apply, Ideal.Quotient.mkₐ_eq_mk] at e ⊢
    rwa [Ideal.Quotient.eq, ← map_sub, Ideal.mem_quotient_iff_mem hIJ, ← Ideal.Quotient.eq]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I✝ : Ideal B
x✝ : I✝ ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I✝).comp

Tactic:
f₁

Goal state after:
R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I✝ : Ideal B
x✝ : I✝ ^ 2 = ⊥
f₁ : R →ₐ[R] B
⊢ ∀ ⦃a₂ : R →ₐ[R] B⦄, (Ideal.Quotient.mkₐ R I✝).comp f₁ = (Ideal.Quotient.mkₐ R I✝).comp a₂ → f₁ = a₂
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
f₁

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ : B →ₐ[R] C
⊢ ∀ ⦃a₂ : B →ₐ[R] C⦄, (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp a₂ → f₁ = a₂
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
A : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
B : Type u_3
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
f₁

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
A : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
B : Type u_3
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ : B →ₐ[R] C
⊢ ∀ ⦃a₂ : B →ₐ[R] C⦄, (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp a₂ → f₁ = a₂
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ A I).comp

Tactic:
f₁

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ : B →ₐ[A] Q
⊢ ∀ ⦃a₂ : B →ₐ[A] Q⦄, (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp a₂ → f₁ = a₂
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
f₁

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ : B →ₐ[R] Q
⊢ ∀ ⦃a₂ : B →ₐ[R] Q⦄, (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp a₂ → f₁ = a₂
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
C : Type (max u_2 u_3)
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ B I).comp

Tactic:
f₁

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
C : Type (max u_2 u_3)
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ : B ⊗[R] A →ₐ[B] C
⊢ ∀ ⦃a₂ : B ⊗[R] A →ₐ[B] C⦄, (Ideal.Quotient.mkₐ B I).comp f₁ = (Ideal.Quotient.mkₐ B I).comp a₂ → f₁ = a₂
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
f₁

Goal state after:
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ : Rₘ →ₐ[R] Q
⊢ ∀ ⦃a₂ : Rₘ →ₐ[R] Q⦄, (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp a₂ → f₁ = a₂
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case h_add
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 : I
⊢ ∀ (a : I) (b₁ b₂ : R), (b₁ + b₂) • b a ⊗ₜ[R] b i = b₁ • b a ⊗ₜ[R] b i + b₂ • b a ⊗ₜ[R] b i

Tactic:
intros

Goal state after:
case h_add
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 a✝ : I
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • b a✝ ⊗ₜ[R] b i = b₁✝ • b a✝ ⊗ₜ[R] b i + b₂✝ • b a✝ ⊗ₜ[R] b i
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : QuasiFinite R S
inst✝¹ : IsArtinianRing R
inst✝ : IsLocalRing R
⊢ Module.Finite R S

Tactic:
let e : (maximalIdeal R).Fiber S ≃ₐ[R] S ⧸ (maximalIdeal R).map (algebraMap R S) :=
    (Algebra.TensorProduct.congr (.symm <| .ofBijective _
      (Ideal.bijective_algebraMap_quotient_residueField (maximalIdeal R))) .refl).trans <|
    (Algebra.TensorProduct.comm _ _ _).trans
    ((Algebra.TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)).symm.restrictScalars _)
  have : Module.Finite R (S ⧸ (maximalIdeal R).map (algebraMap R S)) :=
    have : Module.Finite R ((maximalIdeal R).Fiber S) :=
      .trans (maximalIdeal R).ResidueField _
    .of_surjective e.toLinearMap e.surjective
  refine Module.finite_of_surjective_of_ker_le_nilradical (Ideal.Quotient.mkₐ R
    ((maximalIdeal R).map (algebraMap R S))) Ideal.Quotient.mk_surjective ?_ ?_
  · refine Ideal.mk_ker.trans_le ?_
    rw [Ideal.map_le_iff_le_comap, ← Ring.KrullDimLE.nilradical_eq_maximalIdeal]
    exact fun x hx ↦ IsNilpotent.map hx _
  · rw [← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker]
    exact Ideal.FG.map (IsNoetherian.noetherian _) _

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

Goal state before:
pp: case hfg
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 := ⋯
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (a i).support, ((a i) x_1 • f i) ⊗ₜ[R] b x_1 = ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1

Tactic:
· exact fun _ _ ↦ rfl

Goal state after:
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₀
⊢ IsUnramifiedAt P.ResidueField Q'

Tactic:
let f : P.Fiber (Localization.AtPrime Q) →ₐ[P.ResidueField] Localization.AtPrime Q' :=
    Algebra.TensorProduct.lift (Algebra.ofId _ _) f₀ fun _ _ ↦ .all _ _

Goal state after:
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₀ ⋯
⊢ IsUnramifiedAt P.ResidueField Q'
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✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ K I).comp

Tactic:
f₁

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ : L →ₐ[K] B
⊢ ∀ ⦃a₂ : L →ₐ[K] B⦄, (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp a₂ → f₁ = a₂
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
⊢ { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
    { g // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S }

Tactic:
have h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥ := by
    rw [RingHom.algebraMap_toAlgebra, AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
⊢ { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
    { g // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S }
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)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a : K
e : a • 1 + 0 = 0
hab : a = 0 → ¬0 = 0
⊢ False

Tactic:
← algebraMap_eq_smul_one,

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)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a : K
e : (algebraMap K L) a + 0 = 0
hab : a = 0 → ¬0 = 0
⊢ False
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
let f : Sq ≃ₐ[R] Sq' :=
      Localization.localAlgEquiv q (q.map f₀) f₀ (comap_map_of_bijective f₀ f₀.bijective).symm

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
⊢ (g • q).ramificationIdx R = q.ramificationIdx R
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mpr
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
x : M
⊢ (∃ y, ((∃ n, ∀ a ∈ I ^ n, a • y = 0) ∧ y ∈ N₁) ∧ ∃ z, ((∃ n, ∀ a ∈ I ^ n, a • z = 0) ∧ z ∈ N₂) ∧ y + z = x) →
    (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x

Tactic:
· rintro ⟨y, ⟨⟨n₁, hy⟩, hymem⟩, z, ⟨⟨n₂, hz⟩, hzmem⟩, rfl⟩
    constructor
    · use (max n₁ n₂)
      intro a ha
      specialize hy a (Ideal.pow_le_pow_right (by simp : n₁ ≤ max n₁ n₂) ha)
      specialize hz a (Ideal.pow_le_pow_right (by simp : n₂ ≤ max n₁ n₂) ha)
      aesop
    · use y, hymem, z, hzmem

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
⊢ ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a +
      ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a

Tactic:
by
      rw [sum_filter_add_sum_filter_not]

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
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.biUnion S, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a = 0

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
case inl
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ ∅.biUnion S, (∏ i ∈ ∅, ((↑(∅.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a = 0

case inr
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
hs : s.Nonempty
⊢ ∑ a ∈ s.biUnion S, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

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

Tactic:
exact csInf_le_csSup hne h₁ h₂

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
hx' : x⁻¹ ≠ 0
⊢ a < x⁻¹⁻¹

Tactic:
inv_inv

Goal state after:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a < 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
h0 : spanSingleton R⁰ (mk' K n d) ≠ 0
⊢ spanSingleton R⁰ (mk' K n d) = spanSingleton R⁰ ((algebraMap R K) ↑d)⁻¹ * spanSingleton R⁰ ((algebraMap R K) n)

Tactic:
spanSingleton_mul_spanSingleton

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

Goal state before:
pp: case coe
b x✝ : ℝ≥0
⊢ ↑x✝ - ↑b ≤ max (↑x✝ - ↑b) 0

Tactic:
exact le_max_left _ _

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

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

Tactic:
by
  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∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ a⁻¹ * b⁻¹⁻¹ = a⁻¹ * b

Tactic:
inv_inv

Goal state after:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ a⁻¹ * b = a⁻¹ * b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h : a < b * c
⊢ a < b * c⁻¹⁻¹

Tactic:
inv_inv

Goal state after:
a b c : ℝ≥0∞
h : a < b * c
⊢ a < b * c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : b = c / a
⊢ a * (c / a) = c

Tactic:
ENNReal.mul_div_cancel ha ha'

Goal state after:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : b = c / a
⊢ c = c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : a * b = c
⊢ b = a * (b / a)

Tactic:
ENNReal.mul_div_cancel ha ha'

Goal state after:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : a * b = c
⊢ b = b