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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst✝⁷ : AddCommGroup M1
inst✝⁶ : AddCommGroup M2
inst✝⁵ : AddCommGroup M3
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M1
inst✝² : Module R M2
inst✝¹ : Module R M3
inst✝ : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact ⇑f ⇑g
surj : Function.Surjective ⇑g
⊢ Function.Exact ⇑(lcomp R N g) ⇑(lcomp R N f)

Tactic:
by
  intro h
  simp only [LinearMap.lcomp_apply', Set.mem_range]
  refine ⟨fun hh ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩
  · use ((LinearMap.range f).liftQ h (LinearMap.range_le_ker_iff.mpr hh)).comp
      (exac.linearEquivOfSurjective surj).symm.toLinearMap
    ext x
    simp
  · rw [← hy, LinearMap.comp_assoc, exac.linearMap_comp_eq_zero, LinearMap.comp_zero y]

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

Goal state before:
pp: case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
⊢ P ≠ ⊤

Tactic:
rintro rfl

Goal state after:
case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
h : Prime ⊤
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
⊢ ⨅ i, I * J i ≤ I * ⨅ i, J i

Tactic:
have H : ⨅ i, I * J i ≤ I := (iInf_le _ (Nonempty.some ‹_›)).trans mul_le_left

Goal state after:
case neg
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
⊢ ⨅ i, I * J i ≤ I * ⨅ i, J i
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁵ : Semiring K
inst✝⁴ : AddCommMonoid V
inst✝³ : Module K V
inst✝² : AddCommMonoid V₂
inst✝¹ : Module K V₂
inst✝ : Module.Finite K V
f : V →ₗ[K] V₂
⊢ f.HasFiniteRange

Tactic:
by
  simp [HasFiniteRange]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ I ≤ J ^ (Associates.mk J).count (Associates.mk I).factors

Tactic:
rw [← dvd_iff_le, ← Associates.mk_dvd_mk, Associates.mk_pow]
    simp only [Associates.dvd_eq_le]
    rw [Associates.prime_pow_dvd_iff_le hI hJ']

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ ¬I ≤ J ^ ((Associates.mk J).count (Associates.mk I).factors + 1)

Tactic:
rw [← dvd_iff_le, ← Associates.mk_dvd_mk, Associates.mk_pow]
    simp only [Associates.dvd_eq_le]
    rw [Associates.prime_pow_dvd_iff_le hI hJ']

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ ¬(Associates.mk J).count (Associates.mk I).factors + 1 ≤ (Associates.mk J).count (Associates.mk I).factors
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
⊢ adjoin R (Set.range fun x ↦ X ↑x) = (rename Subtype.val).range

Tactic:
adjoin_range_eq_range_aeval,

Goal state after:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
⊢ (aeval fun x ↦ X ↑x).range = (rename Subtype.val).range
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
⊢ supported R s = (rename Subtype.val).range

Tactic:
rw [supported, Set.image_eq_range, adjoin_range_eq_range_aeval, rename_eq_aeval]
  congr

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

Goal state before:
pp: 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 : M
⊢ Associates.mk (generator (torsionOf R M x)) = Associates.mk p ^ Nat.find ⋯

Tactic:
have prop :
    (fun n : ℕ => p ^ n • x = 0) = fun n : ℕ =>
      (Associates.mk <| generator <| torsionOf R M x) ∣ Associates.mk p ^ n := by
    ext n; rw [← Associates.mk_pow, Associates.mk_dvd_mk, ← mem_iff_generator_dvd]; rfl

Goal state after:
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 : M
prop : (fun n ↦ p ^ n • x = 0) = fun n ↦ Associates.mk (generator (torsionOf R M x)) ∣ Associates.mk p ^ n
⊢ Associates.mk (generator (torsionOf R M x)) = Associates.mk p ^ Nat.find ⋯
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case pos
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : m i = 0
⊢ (monomial (single i 1 + (m - single i 1))) 0 = (monomial m) 0

Tactic:
monomial_zero

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ (auxInv S r).comp (auxHom S r).toRingHom = RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})

Tactic:
← RingHom.cancel_right (Ideal.Quotient.mk_surjective)

Goal state after:
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ((auxInv S r).comp (auxHom S r).toRingHom).comp (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) =
    (RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
      (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : M →ₗ[A] N✝
h : (tautologicalSolution A M).postcomp f✝ = (tautologicalSolution A M).postcomp f'✝
⊢ f✝ = f'✝

Tactic:
ext m

Goal state after:
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : M →ₗ[A] N✝
h : (tautologicalSolution A M).postcomp f✝ = (tautologicalSolution A M).postcomp f'✝
m : M
⊢ f✝ m = f'✝ m
Module: Mathlib.Algebra.Module.Presentation.Tensor

Goal state before:
pp: A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
r₁ : relations₁.R
g₂ : relations₂.G
⊢ (Finsupp.linearCombination A
        (⇑(LinearMap.applyₗ (solution₂.var g₂)) ∘ fun g₁ ↦
          h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }))
      (relations₁.relation r₁) =
    0

Tactic:
have := s.linearCombination_var_relation (.inl ⟨r₁, g₂⟩)

Goal state after:
A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
r₁ : relations₁.R
g₂ : relations₂.G
this : (Finsupp.linearCombination A s.var) ((relations₁.tensor relations₂).relation (Sum.inl (r₁, g₂))) = 0
⊢ (Finsupp.linearCombination A
        (⇑(LinearMap.applyₗ (solution₂.var g₂)) ∘ fun g₁ ↦
          h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }))
      (relations₁.relation r₁) =
    0
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
⊢ Subsingleton P.H1Cotangent ↔ Function.Injective ⇑P.cotangentComplex

Tactic:
delta Extension.H1Cotangent

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Subsingleton ↥P.cotangentComplex.ker ↔ Function.Injective ⇑P.cotangentComplex
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n) ↔
    ∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)

Tactic:
by
  constructor
  · intro h
    exact rTensor_injective_of_forall_vanishesTrivially R h
  · intro h k m n hmn
    exact vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R (h _) hmn

Goal state after:
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
c : R
x : S
⊢ (algebraMap S S') (c • x) = c • (algebraMap S S') x

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Goal state after:
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:
comp_assoc,

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 ∘ₗ K.mkQ ∘ₗ K.subtype = 0
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
⊢ N₁ = N₂ → Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂

Tactic:
rintro rfl

Goal state after:
case mpr
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
h : N₁ ≤ N₁
h' : N₁.FG
⊢ Submodule.map (𝔪 • N₁).mkQ N₁ = Submodule.map (𝔪 • N₁).mkQ N₁
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mpr
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
⊢ N = ⊤ → Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤

Tactic:
rintro rfl

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R M
⊢ Submodule.map ((TensorProduct.mk R k M) 1) ⊤ = ⊤
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
⊢ LinearIndependent (ι := ↑(powersetCard I n)) K (ιMulti_family K n v)

Tactic:
let W := Submodule.span K (Set.range v)

Goal state after:
K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
⊢ LinearIndependent (ι := ↑(powersetCard I n)) K (ιMulti_family K n v)
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ ↑(M.rTensorOne' (m ⊗ₜ[R] (algebraMap R ↥⊥) y)) = ↑(y • m)

Tactic:
rTensorOne',

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ ↑((↑(LinearEquiv.ofEq (M.mulMap (Subalgebra.toSubmodule ⊥)).range M ⋯) ∘ₗ
          (M.mulMap (Subalgebra.toSubmodule ⊥)).rangeRestrict)
        (m ⊗ₜ[R] (algebraMap R ↥⊥) y)) =
    ↑(y • m)
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
⊢ M.LinearDisjoint N'

Tactic:
let i := mulMap M N ∘ₗ (inclusion h).lTensor M

Goal state after:
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)
⊢ M.LinearDisjoint N'
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
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
⊢ Module.rank R ↥(M ⊓ N) ≤ 1

Tactic:
refine _root_.rank_le fun s h ↦ ?_

Goal state after:
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
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
⊢ s.card ≤ 1
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
⊢ (map fun i ↦ f (e.symm i)) ∘ₗ ↑(reindex R s e) = ↑(reindex R t e) ∘ₗ map f

Tactic:
ext m

Goal state after:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
m : (i : ι) → s i
⊢ (((map fun i ↦ f (e.symm i)) ∘ₗ ↑(reindex R s e)).compMultilinearMap (tprod R)) m =
    ((↑(reindex R t e) ∘ₗ map f).compMultilinearMap (tprod R)) m
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
⊢ map f ∘ₗ ↑(reindex R s e).symm = ↑(reindex R t e).symm ∘ₗ map fun i ↦ f (e.symm i)

Tactic:
ext m

Goal state after:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
m : (i : ι₂) → s (e.symm i)
⊢ ((map f ∘ₗ ↑(reindex R s e).symm).compMultilinearMap (tprod R)) m =
    ((↑(reindex R t e).symm ∘ₗ map fun i ↦ f (e.symm i)).compMultilinearMap (tprod R)) m
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
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
⊢ (associatedPrimes R M).Nonempty

Tactic:
by
  obtain ⟨x, hx⟩ := exists_ne (0 : M)
  obtain ⟨P, hP, _⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x hx
  exact ⟨P, hP⟩

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ IsAssociatedPrime I M ↔ I.IsPrime ∧ ∃ f, Function.Injective ⇑f

Tactic:
isAssociatedPrime_iff,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ (I.IsPrime ∧ ∃ x, I = ⊥.colon {x}) ↔ I.IsPrime ∧ ∃ f, Function.Injective ⇑f
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Bijective
    ⇑((IsLocalizedModule.map P.primeCompl (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization P.primeCompl)))
          ((TensorProduct.mk R (Localization P.primeCompl) M) 1))
        (Finsupp.linearCombination R b))

Tactic:
rw [IsLocalizedModule.map_linearCombination, LinearMap.coe_restrictScalars]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Bijective
    ⇑(Finsupp.linearCombination (Localization P.primeCompl)
        (⇑((TensorProduct.mk R (Localization P.primeCompl) M) 1) ∘ b))
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = (⊥.colon {x}).radical
⊢ x ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
e : J = (⊥.colon {0}).radical
⊢ False
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ J = I.radical → J ∈ associatedPrimes R (R ⧸ I)

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
⊢ I.radical ∈ associatedPrimes R (R ⧸ I)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ x ≠ 0

Tactic:
rintro rfl

Goal state after:
case mpr
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
hx : spanSingleton R⁰ 0 = ↑I
⊢ False
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case subsingleton
A : Type u
inst✝⁷ : CommRing A
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module A M
inst✝⁴ : IsNoetherianRing A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
inst✝¹ : Module.Finite A N
inst✝ : Subsingleton N
⊢ (associatedPrimes A N).Finite

Tactic:
| subsingleton N =>

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

Goal state before:
pp: case mp.refine_1
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
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
X : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ x ≠ 0

Tactic:
rintro rfl

Goal state after:
case mp.refine_1
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
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
X : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
hX : spanSingleton R⁰ 0 = ↑X
⊢ False
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero
G : Type u_1
inst✝² : Group G
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ derivedSeries G (n + 0) ≤ map f (derivedSeries G' 0)

Tactic:
exact f.range_eq_map ▸ ((derivedSeries G n).map_eq_bot_iff.mp
      (le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans hfg

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝² : Group G
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)

Tactic:
induction m with
  | zero =>
    exact f.range_eq_map ▸ ((derivedSeries G n).map_eq_bot_iff.mp
      (le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans hfg
  | succ m hm => exact commutator_le_map_commutator hm hm

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
⊢ ¬Group.IsSolvable (Perm (Fin 5))

Tactic:
have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹ := by unfold x y z; decide

Goal state after:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ ¬Group.IsSolvable (Perm (Fin 5))
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
this :
  curry ↑e =
    ↑(LinearEquiv.congrLeft (M ⊗[R] N) R (TensorProduct.lid R N) ≪≫ₗ e.congrRight) ∘ₗ
      rTensorHom N ∘ₗ ↑(ringLmapEquivSelf R R M).symm
⊢ Function.Bijective ⇑(curry ↑e)

Tactic:
simpa [this] using! (rTensorEquiv R M <| TensorProduct.comm R N M ≪≫ₗ e).bijective

Goal state after: