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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
⊢ J = I

Tactic:
have h_eq : ∀ α : H.root, α ∈ J.rootSet ↔ α ∈ I.rootSet := fun α ↦ by
    rw [mem_rootSet_invtSubmoduleToLieIdeal, rootSystem_root_apply]
    exact ⟨I.mem_rootSet_of_mem_rootSpan, fun h ↦ Submodule.subset_span ⟨α, h, rfl⟩⟩

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
⊢ J = I
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case add
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 ι σ
q : MvPolynomial ι' S
hq : ∃ a, (Q.aux P) a = q
a : MvPolynomial (ι' ⊕ ι) R
⊢ ∃ a_1, (Q.aux P) a_1 = (Q.aux P) a + q

Tactic:
obtain ⟨b, rfl⟩ := hq

Goal state after:
case add
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 ι σ
a b : MvPolynomial (ι' ⊕ ι) R
⊢ ∃ a_1, (Q.aux P) a_1 = (Q.aux P) a + (Q.aux P) b
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 ι
x y : S
e : P.σ x = P.σ y
⊢ x = y

Tactic:
← P.aeval_val_σ x,

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S ι
x y : S
e : P.σ x = P.σ y
⊢ (aeval P.val) (P.σ x) = y
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ i ∈ Finset.map (↑e).toEmbedding (support x) with i.1 = i, (monomial (e.symm i)) (coeff (e.symm i) x) ∈
    Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker

Tactic:
convert_to monomial (e.symm (i, 0)) 1 * (Q.toComp P).toAlgHom.toRingHom
      (∑ j ∈ (support x).map e.toEmbedding with j.1 = i, monomial j.2 (coeff (e.symm j) x)) ∈ _

Goal state after:
case e'_5
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ i ∈ Finset.map (↑e).toEmbedding (support x) with i.1 = i, (monomial (e.symm i)) (coeff (e.symm i) x) =
    (monomial (e.symm (i, 0))) 1 *
      (Q.toComp P).toAlgHom.toRingHom
        (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i, (monomial j.2) (coeff (e.symm j) x))

case a.convert_4
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ (monomial (e.symm (i, 0))) 1 *
      (Q.toComp P).toAlgHom.toRingHom
        (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i, (monomial j.2) (coeff (e.symm j) x)) ∈
    Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
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
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : S
y : Ω[P.Ring⁄R]
⊢ (CotangentSpace.map f) (x ⊗ₜ[P.Ring] y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.map R R' P.Ring P'.Ring) y

Tactic:
CotangentSpace.map,

Goal state after:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : S
y : Ω[P.Ring⁄R]
⊢ (LinearMap.liftBaseChange S
        (↑P.Ring ((TensorProduct.mk P'.Ring S' Ω[P'.Ring⁄R']) 1) ∘ₗ KaehlerDifferential.map R R' P.Ring P'.Ring))
      (x ⊗ₜ[P.Ring] y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.map R R' P.Ring P'.Ring) y
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
⊢ (y' • 1) • ↑s = y' • ↑s

Tactic:
smul_assoc,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
⊢ y' • 1 • ↑s = y' • ↑s
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case h
R : Type u
inst✝¹¹ : CommSemiring R
S : Submonoid R
Rₚ : Type v
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : IsLocalization S Rₚ
M : Type w
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
Mₚ : Type t
inst✝⁵ : AddCommMonoid Mₚ
inst✝⁴ : Module R Mₚ
inst✝³ : Module Rₚ Mₚ
inst✝² : IsScalarTower R Rₚ Mₚ
f : M →ₗ[R] Mₚ
inst✝¹ : IsLocalizedModule S f
inst✝ : Module.Finite R M
T : Finset M
hT : Submodule.span R ↑T = ⊤
⊢ Submodule.span Rₚ ↑(Finset.image (⇑f) T) = ⊤

Tactic:
simpa using span_eq_top_of_isLocalizedModule Rₚ S f hT

Goal state after:
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
h : Even ↑k
⊢ Even k

Tactic:
have : NeZero n := ⟨k.pos.ne'⟩

Goal state after:
n : ℕ
k : Fin n
h : Even ↑k
this : NeZero n
⊢ Even k
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
hn : Odd n
k : Fin n
⊢ Even k

Tactic:
have : NeZero n := ⟨k.pos.ne'⟩

Goal state after:
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
⊢ Even k
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
i j : Fin n
hij : i ≤ j
h'' : ∀ (a_1 : Fin n), a a_1 = b (σ a_1)
⊢ σ i ≤ σ j

Tactic:
← a.map_rel_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
i j : Fin n
hij : a i ≤ a j
h'' : ∀ (a_1 : Fin n), a a_1 = b (σ a_1)
⊢ σ i ≤ σ j
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) ((⇑b ∘ ⇑(ofFinEmbEquiv.symm s)) i)).det = 1

Tactic:
suffices Matrix.of (fun i j => b.coord (powersetCard.ofFinEmbEquiv.symm s j)
    (b (powersetCard.ofFinEmbEquiv.symm s i))) = 1 by
    simp_rw [Function.comp_apply, this, Matrix.det_one]

Goal state after:
R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) (b ((ofFinEmbEquiv.symm s) i))) = 1
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
r' : R
f : (i : ι) → s i
i : ι
hf : f i = 0
⊢ (FreeAddMonoid.lift φ) (FreeAddMonoid.of (r', f)) = (FreeAddMonoid.lift φ) 0

Tactic:
simp [FreeAddMonoid.lift_eval_of, C0 r' f i hf]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum = x
a : R
⊢ (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i)
        (FreeAddMonoid.toList ((FreeAddMonoid.map fun y ↦ (a * y.1, y.2)) p))).sum =
    a • (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum

Tactic:
simp [Function.comp_def, mul_smul, List.smul_sum]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
M' : Submodule R S
h : M' ≤ M
inst✝ : Flat R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective ⇑i
x✝¹ : ↥M'
x✝ : ↥N
⊢ ((TensorProduct.AlgebraTensorModule.curry i) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (M'.mulMap N)) x✝¹) x✝

Tactic:
simp [i]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
N' : Submodule R S
h : N' ≤ N
inst✝ : Flat R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective ⇑i
x✝¹ : ↥M
x✝ : ↥N'
⊢ ((TensorProduct.AlgebraTensorModule.curry i) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (M.mulMap N')) x✝¹) x✝

Tactic:
simp [i]

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
⊢ ∃ x', I = N.colon {x'}

Tactic:
obtain ⟨hn0, J, hJ, hJI⟩ := Nat.find_spec key

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
hn0 : Nat.find key ≠ 0
J : Ideal R
hJ : I ^ Nat.find key * J ≤ ann
hJI : ¬J ≤ I
⊢ ∃ x', I = N.colon {x'}
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
H : motive ↥⊤
⊢ motive M

Tactic:
exact equiv _ _ Submodule.topEquiv H

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
⊢ Function.Surjective ⇑mk0

Tactic:
by
  rintro ⟨I⟩
  refine ⟨⟨ClassGroup.integralRep I.1, ClassGroup.integralRep_mem_nonZeroDivisors I.ne_zero⟩, ?_⟩
  rw [ClassGroup.mk0_integralRep, ClassGroup.Quot_mk_eq_mk]

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

Goal state before:
pp: case h
R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, spanSingleton S⁰ ↑x = ↑I
u : Lˣ
hu : spanSingleton S⁰ ↑u = ↑I
⊢ spanSingleton R⁰ ((IsFractionRing.ringEquivOfRingEquiv f.symm) ↑u) = (↑(ringEquivOfRingEquiv K L f)).symm ↑I

Tactic:
rw [← FractionalIdeal.ringEquivOfRingEquiv_spanSingleton,
        ← FractionalIdeal.ringEquivOfRingEquiv_symm_eq, hu]

Goal state after:
case h
R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, spanSingleton S⁰ ↑x = ↑I
u : Lˣ
hu : spanSingleton S⁰ ↑u = ↑I
⊢ (ringEquivOfRingEquiv K L f).symm ↑I = (↑(ringEquivOfRingEquiv K L f)).symm ↑I
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: case intro
R : Type uR
inst✝⁵ : CommRing R
ι : Type u_1
inst✝⁴ : Finite ι
M : ι → Type u_2
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Flat R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
p : PrimeSpectrum R
val✝ : Fintype ι
f : ((i : ι) → M i) →ₗ[R] (i : ι) → LocalizedModule p.asIdeal.primeCompl (M i) :=
  LinearMap.pi fun i ↦ mkLinearMap p.asIdeal.primeCompl (M i) ∘ₗ LinearMap.proj i
e : LocalizedModule p.asIdeal.primeCompl ((i : ι) → M i) ≃ₗ[Localization.AtPrime p.asIdeal]
  (i : ι) → LocalizedModule p.asIdeal.primeCompl (M i) :=
  LinearEquiv.extendScalarsOfIsLocalization p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
    (IsLocalizedModule.linearEquiv p.asIdeal.primeCompl (mkLinearMap p.asIdeal.primeCompl ((i : ι) → M i)) f)
this : ∀ (i : ι), Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (M i))
⊢ finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl ((i : ι) → M i)) =
    ∑ᶠ (i : ι), finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (M i))

Tactic:
e.finrank_eq,

Goal state after:
case intro
R : Type uR
inst✝⁵ : CommRing R
ι : Type u_1
inst✝⁴ : Finite ι
M : ι → Type u_2
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Flat R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
p : PrimeSpectrum R
val✝ : Fintype ι
f : ((i : ι) → M i) →ₗ[R] (i : ι) → LocalizedModule p.asIdeal.primeCompl (M i) :=
  LinearMap.pi fun i ↦ mkLinearMap p.asIdeal.primeCompl (M i) ∘ₗ LinearMap.proj i
e : LocalizedModule p.asIdeal.primeCompl ((i : ι) → M i) ≃ₗ[Localization.AtPrime p.asIdeal]
  (i : ι) → LocalizedModule p.asIdeal.primeCompl (M i) :=
  LinearEquiv.extendScalarsOfIsLocalization p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
    (IsLocalizedModule.linearEquiv p.asIdeal.primeCompl (mkLinearMap p.asIdeal.primeCompl ((i : ι) → M i)) f)
this : ∀ (i : ι), Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (M i))
⊢ finrank (Localization.AtPrime p.asIdeal) ((i : ι) → LocalizedModule p.asIdeal.primeCompl (M i)) =
    ∑ᶠ (i : ι), finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (M i))
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N).symm ≪≫ₗ
    (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[R] M) N).symm
⊢ finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N)) =
    (rankAtStalk M * rankAtStalk N) p

Tactic:
e.finrank_eq,

Goal state after:
R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N).symm ≪≫ₗ
    (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[R] M) N).symm
⊢ finrank (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal]
        (Localization.AtPrime p.asIdeal ⊗[R] N)) =
    (rankAtStalk M * rankAtStalk N) p
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case inl
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
h : Normal F L
h✝ : IsEmpty (K →ₐ[F] L)
⊢ Normal F ↥(normalClosure F K L)

Tactic:
rw [normalClosure, iSup_of_empty]

Goal state after:
case inl
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
h : Normal F L
h✝ : IsEmpty (K →ₐ[F] L)
⊢ Normal F ↥⊥
Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin

Goal state before:
pp: case hC
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom ⋯
x✝ : F
⊢ (((↑i).comp (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F)))).comp C) x✝ = ((↑(aeval x)).comp C) x✝

Tactic:
simp [i]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin

Goal state before:
pp: case hX
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom ⋯
i✝ : ι
⊢ ((↑i).comp (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F)))) (X i✝) = ↑(aeval x) (X i✝)

Tactic:
simp [i]

Goal state after: