mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥LieSubalgebra.root
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H ⇑(S.root' γ) ≤ LieSubmodule.restr I H
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H

Tactic:
have h_neg : S.pairing (S.reflectionPerm γ δ) γ ≠ 0 := by
      rwa [← S.pairing_reflectionPerm γ δ γ, S.pairing_reflectionPerm_self_right, neg_ne_zero]

Goal state after:
case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥LieSubalgebra.root
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H ⇑(S.root' γ) ≤ LieSubmodule.restr I H
h_neg : S.pairing ((S.reflectionPerm γ) δ) γ ≠ 0
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
h : ↥H
hI : ↑h ∈ I
β : ↥LieSubalgebra.root
hβ : β ∉ I.rootSet
⊢ ↑β h = 0

Tactic:
by
  simp only [LieIdeal.mem_rootSet] at hβ
  contrapose! hβ
  intro y hy
  have h_smul : (β : Weight K H L) h • y ∈ I.toSubmodule := by
    rw [← lie_eq_smul_of_mem_rootSpace hy h]
    exact lie_mem_left K L I h y hI
  rwa [I.toSubmodule.smul_mem_iff hβ] at h_smul

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case a
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ LieSubmodule.restr I H ≤ ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯

pp: case a
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯ ≤ LieSubmodule.restr I H

Tactic:
· rw [lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, restr_inf_cartan_eq_biSup_corootSubmodule]
    apply sup_le
    · exact iSup₂_le fun β hβ ↦ le_iSup₂_of_le β hβ
        (by rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_right)
    · exact iSup₂_le fun α hα ↦ le_iSup₂_of_le α hα
        (by rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_of_le_left le_sup_left)

Goal state after:
case a
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯ ≤ LieSubmodule.restr I H
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥R⁰
x : R
hx : (algebraMap R K) x = ↑z • y
⊢ (algebraMap R K) x ∈ I

Tactic:
· rw [hx]
    exact smul_mem _ _ y_mem

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ WellFounded DvdNotUnit

Tactic:
by
    have : WellFoundedGT (Ideal A) := inferInstance
    convert! this.wf using 3
    exact Ideal.dvdNotUnit_iff_lt

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I < Multiset.replicate (i + 1) (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I

Tactic:
Multiset.lt_replicate_succ

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2.refine_4
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (a_1 : A), ∀ x ∈ Submodule.span A (f '' ↑s), a * x ∈ ↑J → a * a_1 • x ∈ ↑J

Tactic:
intro b x _ hx; rw [mul_smul_comm]; exact Submodule.smul_mem _ b hx

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V₂ : Type u_4
V₃ : Type u_6
inst✝⁴ : CommRing K
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u u' : V₃ →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h : u.IsQuasiInverse v
h' : u'.IsQuasiInverse v'
hu : u ≈ u'
⊢ v ∘ₗ id ≈ v ∘ₗ u' ∘ₗ v'

Tactic:
h'.1.equiv

Goal state after:
K : Type u_1
V₂ : Type u_4
V₃ : Type u_6
inst✝⁴ : CommRing K
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u u' : V₃ →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h : u.IsQuasiInverse v
h' : u'.IsQuasiInverse v'
hu : u ≈ u'
⊢ v ∘ₗ id ≈ v ∘ₗ id
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : CommRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S T : Submodule K V
hST : IsCompl S T
⊢ S.subtype.IsQuasiInverse (S.projectionOnto T hST) ↔ IsNoetherian K ↥T

Tactic:
IsQuasiInverse,

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : CommRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S T : Submodule K V
hST : IsCompl S T
⊢ S.subtype.IsLeftQuasiInverse (S.projectionOnto T hST) ∧ S.subtype.IsRightQuasiInverse (S.projectionOnto T hST) ↔
    IsNoetherian K ↥T
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
R : Type u_3
inst✝² : Ring R
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ↑(finrank R ↥⊤) - ↑(finrank R (N ⧸ range 0)) = ↑(finrank R M) - ↑(finrank R N)

Tactic:
range_zero

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
R : Type u_3
inst✝² : Ring R
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ↑(finrank R ↥⊤) - ↑(finrank R (N ⧸ ⊥)) = ↑(finrank R M) - ↑(finrank R N)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case mp.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
σ : ↥⋯.toFinset → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : ↥⋯.toFinset), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] ↥⋯.toFinset →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : ↥⋯.toFinset →₀ R
hx : (linearCombination R Subtype.val) x = 0
⊢ mapDomain π (mapDomain σ x) = x

Tactic:
rw [← Finsupp.mapDomain_comp, hσ₁, Finsupp.mapDomain_id]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
x : ↥s → R
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i

Tactic:
by
  obtain ⟨y, hy⟩ :=
    exists_representative_mod_finset P e prime coprime fun i =>
      Ideal.Quotient.mk _ (x i)
  exact ⟨y, fun i hi => Ideal.Quotient.eq.mp (hy i hi)⟩

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case pos.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) :=
  (R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : a • (Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k)) (p ^ k) = f.symm ⟨p ^ k • x, h⟩
⊢ ∃ a, p ^ k • x = p ^ k • a • y

Tactic:
use a

Goal state after:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) := ⋯
a : R
ha : a • (Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k)) (p ^ k) = f.symm ⟨p ^ k • x, h⟩
⊢ p ^ k • x = p ^ k • a • y
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway S r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (RingHom.ker (mvPolynomialQuotientEquiv S r)) =
    Ideal.span {C r * X () - 1}

Tactic:
simp [RingHom.ker_equiv, ← RingHom.ker_eq_comap_bot]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span (Set.range (Sum.elim (Q.compRelationAux P) fun rp ↦ (rename Sum.inr) (P.relation rp))) =
    Ideal.span (Set.range (Q.compRelationAux P)) ⊔ RingHom.ker (Q.aux P)

Tactic:
Set.Sum.elim_range,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span (Set.range (Q.compRelationAux P) ∪ Set.range fun rp ↦ (rename Sum.inr) (P.relation rp)) =
    Ideal.span (Set.range (Q.compRelationAux P)) ⊔ RingHom.ker (Q.aux P)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
s : T
⊢ (aeval (Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val)))
      ((Q.σ s).coeff.sum fun n r ↦ (rename Sum.inr) (P.σ r) * (monomial (Finsupp.mapDomain Sum.inl n)) 1) =
    s

Tactic:
have (x : P.Ring) : aeval (algebraMap S T ∘ P.val) x = algebraMap S T (aeval P.val x) := by
      rw [map_aeval, aeval_def, coe_eval₂Hom, ← IsScalarTower.algebraMap_eq, Function.comp_def]
    conv_rhs => rw [← Q.aeval_val_σ s, (Q.σ s).as_sum]
    simp [aeval_rename, this, aeval_monomial, Finsupp.prod_mapDomain_index_inj Sum.inl_injective,
      Finsupp.sum, MvPolynomial.finsupp_support_eq_support, MvPolynomial.coeff]

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
s : T
⊢ (aeval (Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val)))
      ((Q.σ s).coeff.sum fun n r ↦ (rename Sum.inr) (P.σ r) * (monomial (Finsupp.mapDomain Sum.inl n)) 1) =
    s

Tactic:
by
    have (x : P.Ring) : aeval (algebraMap S T ∘ P.val) x = algebraMap S T (aeval P.val x) := by
      rw [map_aeval, aeval_def, coe_eval₂Hom, ← IsScalarTower.algebraMap_eq, Function.comp_def]
    conv_rhs => rw [← Q.aeval_val_σ s, (Q.σ s).as_sum]
    simp [aeval_rename, this, aeval_monomial, Finsupp.prod_mapDomain_index_inj Sum.inl_injective,
      Finsupp.sum, MvPolynomial.finsupp_support_eq_support, MvPolynomial.coeff]

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Generators R T ι
s : T
⊢ (aeval P.val) ((MvPolynomial.map (algebraMap R S)) (P.σ s)) = s

Tactic:
simp [@aeval_def S, ← IsScalarTower.algebraMap_eq, ← @aeval_def R]

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
b : ι' → S
s : S
⊢ ∃ a, (aeval (Sum.elim P.val b)) a = s

Tactic:
use rename Sum.inl (P.σ s)

Goal state after:
case h
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
b : ι' → S
s : S
⊢ (aeval (Sum.elim P.val b)) ((rename Sum.inl) (P.σ s)) = s
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S'
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : Algebra S' T
inst✝ : IsScalarTower R S' T
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this✝³ : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S
⊢ (map R R S' S) ((map R R S S') x) = x

Tactic:
change ((map R R S' S).restrictScalars S ∘ₗ map R R S S') x = x

Goal state after:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S'
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : Algebra S' T
inst✝ : IsScalarTower R S' T
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this✝³ : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S
⊢ (↑S (map R R S' S) ∘ₗ map R R S S') x = x
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
w✝ : ℕ
K : Submodule R (Fin w✝ → R)
ϕ : P ≃ₗ[R] (Fin w✝ → R) ⧸ K
hK : K.FG
this : Module.Finite R ↥K
⊢ h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ ∘ₗ K.subtype = 0

Tactic:
(LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
w✝ : ℕ
K : Submodule R (Fin w✝ → R)
ϕ : P ≃ₗ[R] (Fin w✝ → R) ⧸ K
hK : K.FG
this : Module.Finite R ↥K
⊢ h₁ ∘ₗ ↑ϕ.symm ∘ₗ 0 = 0
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
l : Fin (n + n)
⊢ Even ↑(l + l)

Tactic:
val_add_eq_ite

Goal state after:
n : ℕ
l : Fin (n + n)
⊢ Even (if n + n ≤ ↑l + ↑l then ↑l + ↑l - (n + n) else ↑l + ↑l)
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.mk ↑(⇑((TensorProduct.mk R A M) 1) '' s) ≤ Cardinal.lift.{u_2, u_3} (Cardinal.mk ↑s)

Tactic:
convert! Cardinal.mk_image_le_lift (f := TensorProduct.mk R A M 1) (s := s)

Goal state after:
case e'_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.mk ↑(⇑((TensorProduct.mk R A M) 1) '' s) =
    Cardinal.lift.{u_3, max u_2 u_3} (Cardinal.mk ↑(⇑((TensorProduct.mk R A M) 1) '' s))

case e'_4
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.lift.{u_2, u_3} = Cardinal.lift.{max u_2 u_3, u_3}
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
this✝ : Module k (M ⧸ 𝔪 • ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := map_tensorProduct_mk_eq_top._proof_1_9
⊢ N = ⊤

Tactic:
let f := AlgebraTensorModule.lift (((LinearMap.ringLmapEquivSelf k k _).symm
      (Submodule.mkQ (𝔪 • ⊤ : Submodule R M))).restrictScalars R)

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
this✝ : Module k (M ⧸ 𝔪 • ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := map_tensorProduct_mk_eq_top._proof_1_9
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
⊢ N = ⊤
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ : ∀ I ∈ {P | ⊥.colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ⊥.colon {y}}, ¬⊥.colon {y} < I
l : ⊥.colon {x} ≤ ⊥.colon {y}
h₁ : ⊥.colon {y} ≠ ⊤
⊢ ∃ P, (P.IsPrime ∧ ∃ x, P = ⊥.colon {x}) ∧ ⊥.colon {x} ≤ P

Tactic:
refine ⟨_, ⟨⟨h₁, ?_⟩, y, rfl⟩, l⟩

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ : ∀ I ∈ {P | ⊥.colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ⊥.colon {y}}, ¬⊥.colon {y} < I
l : ⊥.colon {x} ≤ ⊥.colon {y}
h₁ : ⊥.colon {y} ≠ ⊤
⊢ ∀ {x y_1 : R}, x * y_1 ∈ ⊥.colon {y} → x ∈ ⊥.colon {y} ∨ y_1 ∈ ⊥.colon {y}
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : IsNoetherianRing A
inst✝ : IsFractionRing A A
I : Ideal A
hI : I.IsMaximal
fin : (associatedPrimes A A).Finite
⊢ ↑I ⊆ ⋃ i ∈ associatedPrimes A A, ↑(id i)

Tactic:
id,

Goal state after:
A : Type u
inst✝² : CommRing A
inst✝¹ : IsNoetherianRing A
inst✝ : IsFractionRing A A
I : Ideal A
hI : I.IsMaximal
fin : (associatedPrimes A A).Finite
⊢ ↑I ⊆ ⋃ i ∈ associatedPrimes A A, ↑i
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : IsNoetherianRing A
I : Ideal A
inst✝ : FaithfulSMul A ↥I
⊢ (↑I ∩ ↑(nonZeroDivisors A)).Nonempty

Tactic:
by
  by_contra!
  exact (bot_lt_annihilator_of_disjoint_nonZeroDivisors
    (Set.disjoint_iff_inter_eq_empty.mpr this)).ne' <| by rwa [Module.annihilator_eq_bot]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
⊢ IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] ↑(basicOpen f)

Tactic:
@isOpen_iff_forall_mem_open

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
⊢ ∀ x ∈ ↑(basicOpen f),
    ∃ t ⊆ ↑(basicOpen f), IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ x ∈ t