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

Goal state before:
pp: case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0

pp: case refine_1
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ Fintype.card (L →ₐ[K] AlgebraicClosure L) = pb.dim

Tactic:
· rw [RingHom.map_det, RingHom.mapMatrix_apply,
      traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e,
      embeddingsMatrixReindex_eq_vandermonde, det_mul, det_transpose]
    refine mt mul_self_eq_zero.mp ?_
    simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero]
    rintro i ⟨_, j, hij, h⟩
    exact (Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h)

Goal state after:
case refine_1
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ Fintype.card (L →ₐ[K] AlgebraicClosure L) = pb.dim
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map : Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val
h_multiset_map_sum :
  (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum * ↑↑a ^ k
hzero : (↑↑a ^ k - 1) * (Multiset.map (fun i ↦ ↑↑i ^ k) univ.val).sum = 0
⊢ (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = 0

Tactic:
mul_eq_zero

Goal state after:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map : Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val
h_multiset_map_sum :
  (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum * ↑↑a ^ k
hzero : ↑↑a ^ k - 1 = 0 ∨ (Multiset.map (fun i ↦ ↑↑i ^ k) univ.val).sum = 0
⊢ (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
n : ℕ
a : K
⊢ a ^ q ^ n = a

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]

Goal state after:
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: case mpr.inl
a : ℤ
⊢ a = a * ↑1 ∨ a = -(a * ↑1)

pp: case mpr.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))

Tactic:
· exact Or.inl (by simp)

Goal state after:
case mpr.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m ^ 2).natAbs
⊢ p = 2 ∨ p ∣ m.natAbs

Tactic:
apply Or.intro_right
    rw [sq, Int.natAbs_mul] at hpp
    exact or_self_iff.mp ((Nat.Prime.dvd_mul hp).mp hpp)

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

Goal state before:
pp: n : ℤ
hn : n.natAbs ≠ 1
p : ℕ
pp : Nat.Prime p
pd : p ∣ n.natAbs
⊢ ∃ p, Prime p ∧ p ∣ n

Tactic:
exact ⟨p, Nat.prime_iff_prime_int.mp pp, Int.natCast_dvd.mpr pd⟩

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℕ
x : ZMod p
⊢ x ^ p ^ n = x

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]

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

Goal state before:
pp: K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this : FiniteDimensional L F
⊢ ∏ σ, σ ((algebraMap L F) pb.gen) = (∏ σ, σ pb.gen) ^ finrank L F

Tactic:
have : Algebra.IsSeparable L F := Algebra.isSeparable_tower_top_of_isSeparable K L F

Goal state after:
K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝ : FiniteDimensional L F
this : Algebra.IsSeparable L F
⊢ ∏ σ, σ ((algebraMap L F) pb.gen) = (∏ σ, σ pb.gen) ^ finrank L F
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

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✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ I • ⊤ ≤ Submodule.comap (Submodule.subtype (I ^ n)) (Submodule.mkQ (I ^ (n + 1))).ker

Tactic:
← Submodule.map_le_map_iff_of_injective (I ^ n).subtype_injective,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ Submodule.map (Submodule.subtype (I ^ n)) (I • ⊤) ≤
    Submodule.map (Submodule.subtype (I ^ n))
      (Submodule.comap (Submodule.subtype (I ^ n)) (Submodule.mkQ (I ^ (n + 1))).ker)
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ IsIdempotentElem r

pp: case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

Tactic:
· apply PrimeSpectrum.toPiLocalization_bijective.injective
    simp [map_mul, hr, ← Pi.single_mul]

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
x✝ : Ideal S
⊢ absNorm x✝ ≤ n ↔ (x✝ ∈ (Ideal S)⁰ ∨ x✝ ∉ (Ideal S)⁰) ∧ absNorm x✝ ≤ n

Tactic:
em,

Goal state after:
case refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
x✝ : Ideal S
⊢ absNorm x✝ ≤ n ↔ True ∧ absNorm x✝ ≤ n
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
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
⊢ Nat.card { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } + Nat.card { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } =
    Nat.card { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } + 1

Tactic:
add_right_inj

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
⊢ Nat.card { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } = 1
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : s.Finite
span : Submodule.span R s = ⊤
⊢ IsNoetherian R M

Tactic:
rw [← s.iUnion_of_singleton_coe, Submodule.span_iUnion] at span

Goal state after:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : s.Finite
span : ⨆ i, R ∙ ↑i = ⊤
⊢ IsNoetherian R M
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
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
⊢ p.ramificationIdx' P = Multiset.count P (factors (map f p))

Tactic:
by
  rw [IsDedekindDomain.ramificationIdx'_eq_normalizedFactors_count hp0 hP hP0,
    factors_eq_normalizedFactors]

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

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : I ^ 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
this : Algebra A B := f₁.toAlgebra
⊢ f₁ = f₂

Tactic:
have := IsScalarTower.of_algebraMap_eq' f₁.comp_algebraMap.symm

Goal state after:
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : I ^ 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
this✝ : Algebra A B := f₁.toAlgebra
this : IsScalarTower R A B
⊢ f₁ = f₂
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case neg
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : ¬i = 0
x : A
⊢ RingHom.ker (Ideal.Quotient.mk (I ^ i)) ≤ I

Tactic:
simpa using Ideal.pow_le_self hi

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

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ ∃ T x x_1, Nonempty (S ⊗[R] S ≃ₐ[S] S × T)

Tactic:
by
  obtain ⟨e, he, hsp⟩ : ∃ e, IsIdempotentElem e ∧ KaehlerDifferential.ideal R S = S ⊗[R] S ∙ e :=
    (Ideal.isIdempotentElem_iff_of_fg _ (KaehlerDifferential.ideal_fg R S)).mp <|
      (Ideal.cotangent_subsingleton_iff _).mp <| inferInstanceAs <| Subsingleton Ω[S⁄R]
  let e₁ := AlgEquiv.prodQuotientOfIsIdempotentElem (R := S) he he.one_sub (by simp) (by simp [he])
  let e₂ : (S ⊗[R] S ⧸ Ideal.span {e}) ≃ₐ[S] S :=
    ((Ideal.span {e}).quotientEquivAlgOfEq S hsp.symm).trans <|
      Ideal.quotientKerAlgEquivOfSurjective <|
        (⟨· ⊗ₜ 1, by simp [Algebra.TensorProduct.lmul'']⟩)
  exact ⟨(S ⊗[R] S) ⧸ Ideal.span {1 - e}, inferInstance, inferInstance,
    ⟨e₁.trans (.prodCongr e₂ .refl)⟩⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
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)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (a i) 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 ↦ (a i) k • z • b j ⊗ₜ[R] b k
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ k ∈ f.support.biUnion fun i ↦ ((fun i ↦ b.repr (b i * x)) i).support,
      (b.repr (f.sum fun i y ↦ ((fun i ↦ b.repr (b i * x)) i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k

Tactic:
have h₂ : ∀ (x : S), ((b.repr x).support.sum fun a ↦ b.repr x a • b a) = x := by
    simpa only [Finsupp.linearCombination_apply, Finsupp.sum] using b.linearCombination_repr

Goal state after:
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)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (a i) 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 ↦ (a i) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ k ∈ f.support.biUnion fun i ↦ ((fun i ↦ b.repr (b i * x)) i).support,
      (b.repr (f.sum fun i y ↦ ((fun i ↦ b.repr (b i * x)) i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case hg
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 ∈ (f.support.biUnion fun i ↦ (b.repr (b i * x)).support) \ (a i).support,
    ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1 = 0

Tactic:
simp only [a, Finset.mem_sdiff, Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_not,
      and_imp, forall_exists_index]

Goal state after:
case hg
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)
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 x_2 : I),
    ¬f x_2 = 0 →
      ¬(b.repr (b x_2 * x)) x_1 = 0 → (b.repr (b i * x)) x_1 = 0 → ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1 = 0
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
⊢ QuasiFinite R T

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `A)
   []
   []
   ":="
   (Term.app
    `Algebra.adjoin
    [`R
     (choice
      («term{_}» "{" [`s] "}")
      (Term.structInst
       "{"
       []
       (Term.structInstFields [(Term.structInstField (Term.structInstLVal `s []) [])])
       (Term.optEllipsis [])
       []
       "}"))]))))

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
⊢ QuasiFinite R T
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 = ⊥
⊢ Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro f
  let P : Algebra.Generators R A A := Generators.self R A
  have hP : Function.Injective P.toExtension.cotangentComplex := by
    rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot]
    exact FormallySmooth.subsingleton_h1Cotangent
  obtain ⟨l, hl⟩ := ((P.toExtension.exact_cotangentComplex_toKaehler.split_tfae'.out 0 1 rfl rfl).mp
    ⟨P.toExtension.subsingleton_h1Cotangent.mp FormallySmooth.subsingleton_h1Cotangent,
      Module.projective_lifting_property _ _ P.toExtension.toKaehler_surjective⟩).2
  obtain ⟨g, hg⟩ := retractionKerCotangentToTensorEquivSection (R := R) P.algebraMap_surjective
    ⟨⟨⟨Cotangent.val, by simp⟩, by simpa using! Cotangent.val_smul' (P := P.toExtension)⟩ ∘ₗ
      l.restrictScalars P.toExtension.Ring, LinearMap.ext fun x ↦ congr($hl x)⟩
  let σ := Function.surjInv (f := algebraMap B (B ⧸ I)) Ideal.Quotient.mk_surjective
  have H (x : P.Ring) : ↑(aeval (σ ∘ f) x) = f (algebraMap _ A x) := by
    rw [← Ideal.Quotient.algebraMap_eq, ← aeval_algebraMap_apply, P.algebraMap_eq,
      AlgHom.coe_toRingHom, comp_aeval_apply, ← Function.comp_assoc, Function.comp_surjInv,]
    simp [P]
  let l : P.Ring ⧸ (RingHom.ker (algebraMap P.Ring A)) ^ 2 →ₐ[R] B :=
    Ideal.Quotient.liftₐ _ (aeval (σ ∘ f)) <|
      have : RingHom.ker (algebraMap P.Ring A) ≤ I.comap (aeval (σ ∘ f)).toRingHom := fun x hx ↦ by
        simp_all [← Ideal.Quotient.eq_zero_iff_mem (I := I), -map_aeval]
      show RingHom.ker _ ^ 2 ≤ RingHom.ker _ from
        (Ideal.pow_right_mono this 2).trans ((Ideal.le_comap_pow _ _).trans_eq (hI ▸ rfl))
  have : f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift =
      (Ideal.Quotient.mkₐ R _).comp l := by
    refine Ideal.Quotient.algHom_ext _ (MvPolynomial.algHom_ext fun i ↦ ?_)
    change f (algebraMap P.Ring A (.X i)) = algebraMap _ _ (MvPolynomial.aeval (σ ∘ f) (.X i))
    simpa using! (Function.surjInv_eq _ _).symm
  exact ⟨l.comp g, by rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]⟩

Goal state after:
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
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
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
lift : P₁.Ring →ₐ[R] P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
this : ∀ r ∈ P₁.ker, lift r ∈ P₂.infinitesimal.ker
r : P₁.Ring
hr : r ∈ P₁.ker
s : P₁.Ring
hs : s ∈ P₁.ker
⊢ lift r * lift s ∈ ⊥

Tactic:
← P₂.ker.cotangentIdeal_square,

Goal state after:
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
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
lift : P₁.Ring →ₐ[R] P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
this : ∀ r ∈ P₁.ker, lift r ∈ P₂.infinitesimal.ker
r : P₁.Ring
hr : r ∈ P₁.ker
s : P₁.Ring
hs : s ∈ P₁.ker
⊢ lift r * lift s ∈ P₂.ker.cotangentIdeal ^ 2
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
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
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
lift : P₁.Ring →ₐ[R] P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
x : P₁.Ring
⊢ (algebraMap P₂.infinitesimal.Ring A)
      ((Ideal.Quotient.liftₐ (P₁.ker ^ 2) lift ⋯).toRingHom ((Ideal.Quotient.mk (P₁.ker ^ 2)) x)) =
    (algebraMap A A) ((algebraMap P₁.infinitesimal.Ring A) ((Ideal.Quotient.mk (P₁.ker ^ 2)) x))

Tactic:
exact FormallySmooth.liftOfSurjective_apply _
            (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) _ _ x

Goal state after:
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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
x : Q.Ring
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
⊢ (δAux R Q') (f.toAlgHom x) =
    (δAux R Q) x +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x))

Tactic:
have : IsScalarTower Q.Ring Q.Ring T := IsScalarTower.left _

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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
x : Q.Ring
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
⊢ (δAux R Q') (f.toAlgHom x) =
    (δAux R Q) x +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x))
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 = ⊥
f₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
x : L
⊢ f₁ x = f₂ x

Tactic:
have : f₁ x - f₂ x ∈ I := by
    simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun e x

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₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
x : L
this : f₁ x - f₂ x ∈ I
⊢ f₁ x = f₂ x