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

Goal state before:
pp: case refine_1
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
h : M2 →ₗ[R] N
hh : h ∘ₗ f = 0
⊢ ∃ y, y ∘ₗ g = h

pp: case refine_2
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
h : M2 →ₗ[R] N
x✝ : ∃ y, y ∘ₗ g = h
y : M3 →ₗ[R] N
hy : y ∘ₗ g = h
⊢ h ∘ₗ f = 0

Tactic:
· use ((LinearMap.range f).liftQ h (LinearMap.range_le_ker_iff.mpr hh)).comp
      (exac.linearEquivOfSurjective surj).symm.toLinearMap
    ext x
    simp

Goal state after:
case refine_2
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
h : M2 →ₗ[R] N
x✝ : ∃ y, y ∘ₗ g = h
y : M3 →ₗ[R] N
hy : y ∘ₗ g = h
⊢ h ∘ₗ f = 0
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: 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 : a ∈ I⁻¹
hpI : a ∉ ↑J / I
⊢ ∃ a, (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ ↑J

Tactic:
rw [mem_inv_iff hI0] at hI

Goal state after:
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 : a ∉ ↑J / I
⊢ ∃ a, (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ ↑J
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : CommRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
e : V ≃ₗ[K] V₂
⊢ (↑e.symm).IsQuasiInverse ↑e

Tactic:
by
  simp [IsQuasiInverse, IsLeftQuasiInverse, IsRightQuasiInverse]

Goal state after:
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 ∘ₗ S.projectionOnto T hST ≈ id ↔ IsNoetherian K ↥T

Tactic:
← projection,

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.projection T hST ≈ id ↔ 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
f : M →ₗ[R] N
⊢ f.index = ↑(finrank R ↥f.ker) - ↑(finrank R (N ⧸ f.range))

Tactic:
by
  rfl

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

Goal state before:
pp: 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✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
H : Function.Surjective ⇑(linearCombination R Subtype.val)
f : (↥s →₀ R) →ₗ[R] M
hf : l ∘ₗ f = linearCombination R Subtype.val
x : M
y : ↥s →₀ R
hy : l (x - f y) = 0
⊢ f.range.mkQ x ∈ Submodule.map f.range.mkQ l.ker

Tactic:
exact ⟨_, hy, by simp⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case monomial
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
⊢ coeff m ((pderiv i) ((monomial n) a)) = coeff (m + single i 1) ((monomial n) a) * (↑(m i) + 1)

Tactic:
rw [pderiv_monomial, coeff_monomial, coeff_monomial]
    by_cases h : n = m + single i 1
    · simp [h]
    simp only [h, ↓reduceIte, zero_mul]
    by_cases hn : n i = 0
    · simp [hn]
    apply if_neg
    rwa [tsub_eq_iff_eq_add_of_le (fun _ ↦ by grind)]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this✝ : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := ⋯
Rᵣₛ : Type u_3 := ⋯
hsu : IsUnit ((algebraMap R Rᵣₛ) ↑s)
this : Function.Bijective ⇑(↑hsu.unit⁻¹ • (LocalizedModule.map rs) l')
x : M
⊢ ((algebraMap R (End R N')) ↑s)
      (((LocalizedModule.lift (Submonoid.powers (r * ↑s)) g ⋯ ∘ₗ
            ↑R ↑(LinearEquiv.ofBijective (↑hsu.unit⁻¹ • (LocalizedModule.map rs) l') this)) ∘ₗ
          LocalizedModule.mkLinearMap rs M)
        x) =
    ((algebraMap R (End R N')) ↑s)
      (((↑l ∘ₗ LocalizedModule.lift (Submonoid.powers (r * ↑s)) f ⋯) ∘ₗ LocalizedModule.mkLinearMap rs M) x)

Tactic:
have : ∀ x, g (l' x) = s.1 • (l (f x)) := LinearMap.congr_fun H

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this✝¹ : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := Submonoid.powers (r * ↑s)
Rᵣₛ : Type u_3 := Localization rs
hsu : IsUnit ((algebraMap R Rᵣₛ) ↑s)
this✝ : Function.Bijective ⇑(↑hsu.unit⁻¹ • (LocalizedModule.map rs) l')
x : M
this : ∀ (x : M), g (l' x) = ↑s • l (f x)
⊢ ((algebraMap R (End R N')) ↑s)
      (((LocalizedModule.lift (Submonoid.powers (r * ↑s)) g ⋯ ∘ₗ
            ↑R ↑(LinearEquiv.ofBijective (↑hsu.unit⁻¹ • (LocalizedModule.map rs) l') this✝)) ∘ₗ
          LocalizedModule.mkLinearMap rs M)
        x) =
    ((algebraMap R (End R N')) ↑s)
      (((↑l ∘ₗ LocalizedModule.lift (Submonoid.powers (r * ↑s)) f ⋯) ∘ₗ LocalizedModule.mkLinearMap rs M) x)
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
f : R[X]
⊢ ((mkDerivation R) a) f = derivative f • a

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
⊢ (mkDerivationEquiv R) a = (mkDerivation R) a

Tactic:
by
  rfl

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

Goal state before:
pp: case succ
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
m : ℕ
e : M ≃ₗ[R] (Fin (m + 1) →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
h :
  (∀ (a : Fin (m + 1)),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).1
          a =
        0.1 a) ∧
    ∀ (i : ι),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).2
          i =
        0.2 i
⊢ x ∈ annihilator R M

Tactic:
· rw [show x = 0 by simpa using h.1 0]
    exact zero_mem _

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ pres.differentialsSolution.IsPresentation

Tactic:
Module.Relations.Solution.isPresentation_iff

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤ ∧
    pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_1.refine_2
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁶ : CommRing R''
inst✝¹⁵ : CommRing S''
inst✝¹⁴ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
⊢ ∀ (x : P.Ring) (hx : x ∈ P.ker • P.ker) (y : P.Ring) (hy : y ∈ P.ker • P.ker),
    1 ⊗ₜ[P.Ring] ⟨x, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨y, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨x + y, ⋯⟩ = 0

Tactic:
· intro a ha b hb ha' hb'
      convert! congr($ha' + $hb')
      rw [← tmul_add]
      rfl

Goal state after:
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₂
⊢ ∀ (r : (relations₁.tensor relations₂).R),
    (Finsupp.linearCombination A fun x ↦
          match x with
          | (g₁, g₂) => solution₁.var g₁ ⊗ₜ[A] solution₂.var g₂)
        ((relations₁.tensor relations₂).relation r) =
      0

Tactic:
by
    rintro (⟨r₁, g₂⟩ | ⟨g₁, r₂⟩)
    · dsimp
      rw [Finsupp.linearCombination_embDomain]
      exact (solution₁.postcomp (curry (TensorProduct.comm A M₂ M₁).toLinearMap
        (solution₂.var g₂))).linearCombination_var_relation r₁
    · dsimp
      rw [Finsupp.linearCombination_embDomain]
      exact (solution₂.postcomp (curry .id (solution₁.var g₁))).linearCombination_var_relation r₂

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

Goal state before:
pp: case refine_1
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 g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x) ∈ P'.ker

Tactic:
simp only [RingHom.algebraMap_toAlgebra, RingHom.coe_comp,
        Function.comp_apply,
        ker, RingHom.mem_ker, map_sub, algebraMap_toRingHom,
        algebraMap_σ, sub_self, toAlgHom_apply]

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

Goal state before:
pp: case refine_2
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 g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ f.toAlgHom y - g.toAlgHom y ∈ P'.ker

Tactic:
simp only [RingHom.algebraMap_toAlgebra, RingHom.coe_comp,
        Function.comp_apply,
        ker, RingHom.mem_ker, map_sub, algebraMap_toRingHom,
        algebraMap_σ, sub_self, toAlgHom_apply]

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

Goal state before:
pp: case refine_3
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 g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y) ∈ P'.ker

Tactic:
simp only [RingHom.algebraMap_toAlgebra, RingHom.coe_comp,
        Function.comp_apply,
        ker, RingHom.mem_ker, map_sub, algebraMap_toRingHom,
        algebraMap_σ, sub_self, toAlgHom_apply]

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

Goal state before:
pp: case refine_4
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 g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ f.toAlgHom x - g.toAlgHom x ∈ P'.ker

Tactic:
simp only [RingHom.algebraMap_toAlgebra, RingHom.coe_comp,
        Function.comp_apply,
        ker, RingHom.mem_ker, map_sub, algebraMap_toRingHom,
        algebraMap_σ, sub_self, toAlgHom_apply]

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
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
this : (algebraMap R S) y' • ↑s = y' • ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
rw [← e, this] at hx₁

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
y' : R
hx₁ : y' • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
Module: Mathlib.Algebra.Module.StablyFree.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type w
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsStablyFree R M
⊢ Projective R M

Tactic:
obtain ⟨N, _, _, _, _, _⟩ := IsStablyFree.exist_free_prod R M

Goal state after:
R : Type u
inst✝⁵ : Ring R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N✝ : Type w
inst✝² : AddCommGroup N✝
inst✝¹ : Module R N✝
inst✝ : IsStablyFree R M
N : Type u
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
⊢ Projective R M
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝¹ : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
⊢ domCoprodDep' (a ⊗ₜ[R] b) = a.domCoprodDep b

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: case neg
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 t : ↑(powersetCard I n)
hst : s ≠ t
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) t)) s = (ιMultiDual R n b s) (ιMulti_family R n (⇑b) t)

Tactic:
· rw [ιMultiDual_apply_nondiag R n b s t hst, ← basis_apply, Basis.repr_self,
      Finsupp.single_eq_of_ne hst]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective ⇑f
⊢ (Submodule.map (↑f) M).LinearDisjoint (Submodule.map (↑f) N)

Tactic:
linearDisjoint_iff

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N))
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : x ∉ I
y : R
hy : y ∉ I
h : x * y ∈ I
⊢ False

Tactic:
rw [← Ideal.span_singleton_le_iff_mem, ← left_lt_sup] at hx hy

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
⊢ 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 ∈ associatedPrimes R (R ⧸ I) ↔ J = I.radical

Tactic:
refine ⟨IsAssociatedPrime.eq_radical hI, ?_⟩

Goal state after:
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)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ?m.64) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑1 = ↑?m.64

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ Ideal R

Tactic:
any_goals rfl

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
⊢ Submodule.span R ↑s = ⊤

Tactic:
convert! hs

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
x✝ : X
⊢ x✝ ∈ (fun x a ↦ (f a) x) ⁻¹' {g} ↔ x✝ ∈ ⋂ a, ⇑(f a) ⁻¹' {g a}

Tactic:
simp [funext_iff]

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case pos
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∈ C₁
⊢ f ⟨x, h⟩ = g ⟨x, hx⟩

pp: case neg
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∉ C₁
⊢ g ⟨x, ⋯⟩ = g ⟨x, hx⟩

Tactic:
· exact hfg x ⟨h, hx⟩

Goal state after:
case neg
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∉ C₁
⊢ g ⟨x, ⋯⟩ = g ⟨x, hx⟩
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

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
inst✝² : IsLocalRing R
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom (algebraMap R S)
eSp : ResidueField R ⊗[R] S ≃ₐ[R] S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R) :=
  (Algebra.TensorProduct.comm R (ResidueField R) S).trans
    (AlgEquiv.restrictScalars R (quotIdealMapEquivTensorQuot S (maximalIdeal R)).symm)
⊢ Nontrivial (ResidueField R ⊗[R] S)

Tactic:
rw [eSp.nontrivial_congr, Ideal.Quotient.nontrivial_iff]
    exact ((((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp inferInstance).trans_lt
      (inferInstance : (maximalIdeal S).IsMaximal).lt_top).ne

Goal state after: