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

Goal state before:
pp: case neg
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
⊢ (trace K L) x = 0 x

Tactic:
rw [trace_eq_finrank_mul_minpoly_nextCoeff]

Goal state after:
case neg
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
⊢ ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = 0 x
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit (GCDMonoid.gcd a b)

Tactic:
← coe_gcd,

Goal state after:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit ↑(a.gcd b)
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁸ : Group G
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h : E ≤ F
this✝³ : Algebra ↥E ↥F := (IntermediateField.inclusion h).toAlgebra
this✝² : SMul G ↥F := smulOfNormal G (↥F) L N
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := mulSemiringActionOfSmulDistribClass (↥F) L G
this : IsScalarTower (↥E) (↥F) L
⊢ ∀ (m : ↥(Subgroup.map (QuotientGroup.mk' N) H)) (n : ↥E) (a : ↥F), m • n • a = n • m • a

Tactic:
intro ⟨_, g, hg, rfl⟩ x y

Goal state after:
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁸ : Group G
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h : E ≤ F
this✝³ : Algebra ↥E ↥F := (IntermediateField.inclusion h).toAlgebra
this✝² : SMul G ↥F := smulOfNormal G (↥F) L N
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := mulSemiringActionOfSmulDistribClass (↥F) L G
this : IsScalarTower (↥E) (↥F) L
g : G
hg : g ∈ ↑H
x : ↥E
y : ↥F
⊢ ⟨(QuotientGroup.mk' N) g, ⋯⟩ • x • y = x • ⟨(QuotientGroup.mk' N) g, ⋯⟩ • y
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range ⇑b₁)
h₂ : L₂ = closure (Set.range ⇑b₂)
⊢ |(algebraMap ℤ ℚ)
        ((Basis.addSubgroupOfClosure L₂ b₂ h₂).det fun i ↦ ⟨↑((Basis.addSubgroupOfClosure L₁ b₁ h₁) i), ⋯⟩)| =
    |b₂.det ⇑b₁|

Tactic:
Basis.det_apply,

Goal state after:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range ⇑b₁)
h₂ : L₂ = closure (Set.range ⇑b₂)
⊢ |(algebraMap ℤ ℚ)
        ((Basis.addSubgroupOfClosure L₂ b₂ h₂).toMatrix fun i ↦ ⟨↑((Basis.addSubgroupOfClosure L₁ b₁ h₁) i), ⋯⟩).det| =
    |b₂.det ⇑b₁|
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range ⇑b₁)
h₂ : L₂ = closure (Set.range ⇑b₂)
⊢ |(algebraMap ℤ ℚ)
        ((Basis.addSubgroupOfClosure L₂ b₂ h₂).toMatrix fun i ↦ ⟨↑((Basis.addSubgroupOfClosure L₁ b₁ h₁) i), ⋯⟩).det| =
    |b₂.det ⇑b₁|

Tactic:
Basis.det_apply,

Goal state after:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range ⇑b₁)
h₂ : L₂ = closure (Set.range ⇑b₂)
⊢ |(algebraMap ℤ ℚ)
        ((Basis.addSubgroupOfClosure L₂ b₂ h₂).toMatrix fun i ↦ ⟨↑((Basis.addSubgroupOfClosure L₁ b₁ h₁) i), ⋯⟩).det| =
    |(b₂.toMatrix ⇑b₁).det|
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ f ((Multiset.map id (normalizedFactors a)).prod * (Multiset.map id (normalizedFactors b)).prod) =
    f (Multiset.map id (normalizedFactors a)).prod * f (Multiset.map id (normalizedFactors b)).prod

Tactic:
Finset.prod_multiset_map_count,

Goal state after:
case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ f
      ((∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a)) *
        (Multiset.map id (normalizedFactors b)).prod) =
    f (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a)) *
      f (Multiset.map id (normalizedFactors b)).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ f
      ((∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a)) *
        (Multiset.map id (normalizedFactors b)).prod) =
    f (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a)) *
      f (Multiset.map id (normalizedFactors b)).prod

Tactic:
Finset.prod_multiset_map_count,

Goal state after:
case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ f
      ((∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a)) *
        ∏ m ∈ (normalizedFactors b).toFinset, id m ^ Multiset.count m (normalizedFactors b)) =
    f (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a)) *
      f (∏ m ∈ (normalizedFactors b).toFinset, id m ^ Multiset.count m (normalizedFactors b))
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I J : Ideal S
coprime : IsCoprime I J
⊢ cardQuot (I * J) = cardQuot I * cardQuot J

Tactic:
rw [cardQuot_apply, cardQuot_apply, cardQuot_apply,
    Nat.card_congr (Ideal.quotientMulEquivQuotientProd I J coprime).toEquiv,
    Nat.card_prod]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ P ^ i
⊢ ∃ d, ∃ e ∈ P ^ (i + 1), a * d + e = c

Tactic:
by
  suffices eq_b : P ^ i = Ideal.span {a} ⊔ P ^ (i + 1) by
    rw [eq_b] at c_mem
    simp only [mul_comm a]
    exact Ideal.mem_span_singleton_sup.mp c_mem
  refine (Ideal.eq_prime_pow_of_succ_lt_of_le hP (lt_of_le_of_ne le_sup_right ?_)
    (sup_le (Ideal.span_le.mpr (Set.singleton_subset_iff.mpr a_mem))
      (Ideal.pow_succ_lt_pow hP i).le)).symm
  contrapose a_notMem with this
  rw [this]
  exact mem_sup.mpr ⟨a, mem_span_singleton_self a, 0, by simp, by simp⟩

Goal state after:
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:
simpa using hI

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₃
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
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
hI : p ∣ ↑(absNorm (P * I))
⊢ ∃ P_1, P_1.IsMaximal ∧ under ℤ P_1 = span {p} ∧ P_1 ∣ P * I

Tactic:
simp only [_root_.map_mul, Nat.cast_mul, hp.dvd_mul] at hI

Goal state after:
case h₃
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
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
hI : p ∣ ↑(absNorm P) ∨ p ∣ ↑(absNorm I)
⊢ ∃ P_1, P_1.IsMaximal ∧ under ℤ P_1 = span {p} ∧ P_1 ∣ P * I
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
x : X
hx : IsLocallyClosed {x}
⊢ IsClosed[inst✝¹] {x}

Tactic:
obtain ⟨_, ⟨y, rfl : y = x, rfl⟩, hy'⟩ :=
    nonempty_inter_closedPoints (Set.singleton_nonempty x) hx

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
x : X
hx : IsLocallyClosed {x}
hy' : x ∈ closedPoints X
⊢ IsClosed[inst✝¹] {x}
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:
simpa using hI

Goal state after:
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
⊢ Multiset.count Q (normalizedFactors (map (algebraMap S T) (map f p))) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))

Tactic:
have hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I := by rw [← map_sup, hcp, map_top]

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
⊢ Multiset.count Q (normalizedFactors (map (algebraMap S T) (map f p))) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: case pos
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
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht : (algebraMap S P.ResidueField) ↑t = 0
⊢ (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t))
      ((↑S (Algebra.linearMap P.ResidueField (P.Fiber T))) (s • p / (algebraMap S P.ResidueField) ↑t)) =
    (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t)) (p ⊗ₜ[S] IsLocalization.mk' T s t)

pp: case neg
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
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht : ¬(algebraMap S P.ResidueField) ↑t = 0
⊢ (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t))
      ((↑S (Algebra.linearMap P.ResidueField (P.Fiber T))) (s • p / (algebraMap S P.ResidueField) ↑t)) =
    (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t)) (p ⊗ₜ[S] IsLocalization.mk' T s t)

Tactic:
· simp [ht]

Goal state after:
case neg
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
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht : ¬(algebraMap S P.ResidueField) ↑t = 0
⊢ (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t))
      ((↑S (Algebra.linearMap P.ResidueField (P.Fiber T))) (s • p / (algebraMap S P.ResidueField) ↑t)) =
    (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t)) (p ⊗ₜ[S] IsLocalization.mk' T s t)
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 := 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
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
this✝ : F = G
this : ∀ (j : I), x * f j = f.sum fun i y ↦ (a i) j • y
⊢ ∑ i ∈ f.support, ∑ x ∈ f.support, (a x) i • (f x * b i) ∈
    Submodule.span R (Set.image2 (fun i j ↦ f i * b j) ↑f.support ↑f.support)

Tactic:
apply Submodule.sum_mem

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 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := ⋯
F : I →₀ I →₀ R := ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R := ⋯
this✝ : F = G
this : ∀ (j : I), x * f j = f.sum fun i y ↦ (a i) j • y
⊢ ∀ c ∈ f.support,
    ∑ x ∈ f.support, (a x) c • (f x * b c) ∈ Submodule.span R (Set.image2 (fun i j ↦ f i * b j) ↑f.support ↑f.support)
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 R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) := e ⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩
this✝ : QuasiFiniteAt p.ResidueField qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq : ↑(PrimeSpectrum.basicOpen r) = {{ asIdeal := qF.asIdeal, isPrime := ⋯ }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
this :
  1 ⊗ₜ[R] x ∉
    RingHom.ker
      (TensorProduct.lift
          (Ideal.ResidueField.mapₐ { asIdeal := p, isPrime := ⋯ }.asIdeal
            (↑⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩).asIdeal (ofId R S) ⋯)
          (IsScalarTower.toAlgHom R S (↑⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩).asIdeal.ResidueField) ⋯).toRingHom
⊢ x ∉ q

Tactic:
simpa using this

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 := 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
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
this✝ : F = G
this : ∀ (j : I), x * f j = f.sum fun i y ↦ (a i) j • y
i : I
hi : i ∈ f.support
⊢ ∑ x ∈ f.support, (a x) i • (f x * b i) ∈ Submodule.span R (Set.image2 (fun i j ↦ f i * b j) ↑f.support ↑f.support)

Tactic:
apply Submodule.sum_mem

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 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := ⋯
F : I →₀ I →₀ R := ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R := ⋯
this✝ : F = G
this : ∀ (j : I), x * f j = f.sum fun i y ↦ (a i) j • y
i : I
hi : i ∈ f.support
⊢ ∀ c ∈ f.support, (a c) i • (f c * b i) ∈ Submodule.span R (Set.image2 (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

pp: case e'_2
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)
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
    Function.Surjective ⇑(↑P (mapBaseChange R P A)) ∧ ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id

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

Goal state after:
case e'_2
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)
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
    Function.Surjective ⇑(↑P (mapBaseChange R P A)) ∧ ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id