mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
val✝ : Fintype α
x : α
hx : f x ≠ x
hy : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ (↑(f.toList x)).formPerm ⋯ = f

Tactic:
simp [formPerm_toList, hf.cycleOf_eq hx]

Goal state after:
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x✝¹ : R
x✝ : L
⊢ E.toKer.symm ⟨s₁ (x✝¹ • x✝) - s₂ (x✝¹ • x✝), ⋯⟩ = (RingHom.id R) x✝¹ • E.toKer.symm ⟨s₁ x✝ - s₂ x✝, ⋯⟩

Tactic:
by
    rw [RingHom.id_apply, ← map_smul, EquivLike.apply_eq_iff_eq, SetLike.mk_smul_of_tower_mk,
      Subtype.mk_eq_mk, LinearMap.map_smul_of_tower, smul_sub, LinearMap.map_smul_of_tower]

Goal state after:
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
this : ∀ {s' : L → E.L}, LeftInverse (⇑E.proj) s' → ⁅s x - s' x, s' y - s y⁆ = 0
⊢ (↑((d₁₂ R L M) (E.oneCochainOfTwoSplitting hs₁ hs₂)) x) y = (↑(↑(E.twoCocycleOf hs₁) - ↑(E.twoCocycleOf hs₂)) x) y

Tactic:
replace this {s' : L → E.L} (h : LeftInverse E.proj s') :
      ⁅s x, s' y⁆ = ⁅s' x, s' y⁆ + (⁅s x, s y⁆ - ⁅s' x, s y⁆) := by
    simpa [sub_sub, sub_eq_zero] using this h

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
this : ∀ {s' : L → E.L}, LeftInverse (⇑E.proj) s' → ⁅s x, s' y⁆ = ⁅s' x, s' y⁆ + (⁅s x, s y⁆ - ⁅s' x, s y⁆)
⊢ (↑((d₁₂ R L M) (E.oneCochainOfTwoSplitting hs₁ hs₂)) x) y = (↑(↑(E.twoCocycleOf hs₁) - ↑(E.twoCocycleOf hs₂)) x) y
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin (p + 1) → Fin n
i : Fin n
s : Fin (p + 1)
⊢ (-1) ^ ↑s * ((A.submatrix (Fin.cons i (s.removeNth α)) α).submatrix id ⇑(Equiv.symm s.cycleRange)).det =
    (-1) ^ ↑s * bminor A i (α s) (s.removeNth α)

Tactic:
by
      congrm _ * Matrix.det ?_
      simp [Fin.cons_removeNth_eq_comp_cycleRange_symm]

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : LieRing L
inst✝¹⁰ : Module A L
L' : LieRinehartSubalgebra A L
inst✝⁹ : LieRingModule L A
inst✝⁸ : LieRinehartRing A L
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R A
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRinehartAlgebra R A L
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L M
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅↑(t • x), m⁆ = t • ⁅x, m⁆

Tactic:
Submodule.coe_smul_of_tower,

Goal state after:
A : Type u_1
L : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : LieRing L
inst✝¹⁰ : Module A L
L' : LieRinehartSubalgebra A L
inst✝⁹ : LieRingModule L A
inst✝⁸ : LieRinehartRing A L
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R A
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRinehartAlgebra R A L
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L M
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅t • ↑x, m⁆ = t • ⁅x, m⁆
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) ↔ E.charPoly.IsRoot q

Tactic:
rw [charPoly, Polynomial.IsRoot.def, Polynomial.eval]

Goal state after:
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) ↔ eval₂ (RingHom.id R) q ((monomial E.order) 1 - ∑ i, (monomial ↑i) (E.coeffs i)) = 0
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = p * ↑ha.unit⁻¹

Tactic:
hab,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = b * a * ↑ha.unit⁻¹
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : IsCancelMulZero M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
inst✝ : IsCancelMulZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
⊢ ↑(d ⟨u, hu'⟩) = 1

Tactic:
hu

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : IsCancelMulZero M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
inst✝ : IsCancelMulZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
⊢ ↑(d ⟨1, ⋯⟩) = 1
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
n : ℕ
h : IsFractional S I
⊢ IsFractional S (n • I + I)

Tactic:
exact (IsFractional.nsmul n h).sup h

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
s : Set P
x✝¹ : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x✝ : P
hb : x✝ ∈ span R s
⊢ IsInteger R (a • 0)

Tactic:
by
          rw [smul_zero]
          exact isInteger_zero

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
P' : Type u_3
inst✝⁶ : CommRing P'
inst✝⁵ : Algebra R P'
inst✝⁴ : IsLocalization S P
inst✝³ : IsLocalization S P'
P'' : Type u_5
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
inst✝ : IsLocalization S P''
I : FractionalIdeal S P
x✝ : P''
⊢ x✝ ∈ (canonicalEquiv S P' P'') ((canonicalEquiv S P P') I) ↔ x✝ ∈ (canonicalEquiv S P P'') I

Tactic:
simp [IsLocalization.map_map]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: 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 ∉ ⊥
⊢ ∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I

Tactic:
have y_ne_zero : y ≠ 0 := by simpa using y_notMem

Goal state after:
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
⊢ ∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : ⟨a, haI⟩ ≠ 0
⊢ ¬(↑I)⁻¹ ≤ 1

Tactic:
replace ha0 : a ≠ 0 := Subtype.coe_injective.ne ha0

Goal state after:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
⊢ ¬(↑I)⁻¹ ≤ 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ y ∈ ↑(Ideal.span {x}) ↔ y ∈ spanSingleton S ((algebraMap R P) x)

Tactic:
refine (mem_coeIdeal S).trans (Iff.trans ?_ (mem_spanSingleton S).symm)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ (∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y) ↔ ∃ z, z • (algebraMap R P) x = y
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
⊢ ((smulAddMonoidHom A M) ((of A 0) GOne.one)) ((of M i) xi) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) xi)

Tactic:
rw [smulAddMonoidHom_apply_of_of]

Goal state after:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
⊢ (of M (0 +ᵥ i)) (GSMul.smul GOne.one xi) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) xi)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: K : Type u_3
inst✝ : Field K
p : K[X]
⊢ factors (span {p}) = Multiset.map (fun q ↦ span {q}) (factors p)

Tactic:
rcases eq_or_ne p 0 with rfl | hp; · simpa [Set.singleton_zero] using! normalizedFactors_zero
  have : ∀ q ∈ (factors p).map (fun q ↦ span {q}), Prime q := fun q hq ↦ by
    obtain ⟨r, hr, rfl⟩ := Multiset.mem_map.mp hq
    exact prime_span_singleton_iff.mpr <| prime_of_factor r hr
  rw [← span_singleton_eq_span_singleton.mpr (factors_prod hp), ← multiset_prod_span_singleton,
    factors_eq_normalizedFactors, normalizedFactors_prod_of_prime this]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
hf : f.HasNoetherianRange
⊢ (-f).HasNoetherianRange

Tactic:
rwa [HasNoetherianRange, LinearMap.range_neg]

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 ∘ₗ u' ∘ₗ v' ≈ v ∘ₗ u ∘ₗ v'

Tactic:
hu

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 ∘ₗ u' ∘ₗ v' ≈ v ∘ₗ u' ∘ₗ v'
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✝¹ : 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.ChooseBasisIndex R M → ↥⋯.toFinset := ⋯
σ : ↥⋯.toFinset → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : ↥⋯.toFinset), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
i : ↥⋯.toFinset
⊢ ↑((π ∘ σ) i) = ↑(id i)

Tactic:
exact congr_arg Subtype.val (hσ i)

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✝¹ : 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
i : ↥⋯.toFinset
⊢ (⇑l ∘ ⇑b ∘ σ) i = ↑i

Tactic:
exact congr_arg Subtype.val (hσ i)

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
⊢ span {a} ∈ normalizedFactors (span {b})

Tactic:
obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd ?_ this.irreducible
          (dvd_iff_le.mpr (span_singleton_le_span_singleton.mpr (dvd_of_mem_normalizedFactors ha)))

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
c : Ideal R
hc : c ∈ normalizedFactors (span {b})
hc' : Associated (span {a}) c
⊢ span {a} ∈ normalizedFactors (span {b})
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case refine_1
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FinitePresentation R S
inst✝ : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : (Fin n → S) →ₗ[R] M := ↑R (↑e.symm ∘ₗ K.mkQ)
m : M
⊢ ∃ a, f a = m

Tactic:
obtain ⟨a, ha⟩ := K.mkQ_surjective (e m)
    exact ⟨a, by simp [f, ha]⟩

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k • f1.choose ∈ R ∙ z

Tactic:
rw [← Quotient.mk_eq_zero, mk_smul, f1.choose_spec, ← f.map_smul]

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ f (p ^ k • 1) = 0
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case map_units.left
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommGroup N'✝
inst✝⁸ : Module R N'✝
S : Submonoid R
f✝ : N →ₗ[R] N'✝
inst✝⁷ : IsLocalizedModule S f✝
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
s : ↥S
this : Function.Bijective ⇑((algebraMap R (End R N')) ↑s)
⊢ Function.Injective ⇑((algebraMap R (End R (M' →ₗ[R] N'))) ↑s)

pp: case map_units.right
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommGroup N'✝
inst✝⁸ : Module R N'✝
S : Submonoid R
f✝ : N →ₗ[R] N'✝
inst✝⁷ : IsLocalizedModule S f✝
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
s : ↥S
this : Function.Bijective ⇑((algebraMap R (End R N')) ↑s)
⊢ Function.Surjective ⇑((algebraMap R (End R (M' →ₗ[R] N'))) ↑s)

Tactic:
· exact fun _ _ e ↦ LinearMap.ext fun m ↦ this.left (LinearMap.congr_fun e m)

Goal state after:
case map_units.right
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommGroup N'✝
inst✝⁸ : Module R N'✝
S : Submonoid R
f✝ : N →ₗ[R] N'✝
inst✝⁷ : IsLocalizedModule S f✝
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
s : ↥S
this : Function.Bijective ⇑((algebraMap R (End R N')) ↑s)
⊢ Function.Surjective ⇑((algebraMap R (End R (M' →ₗ[R] N'))) ↑s)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case surj
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ Function.Surjective ⇑(baseChange S f)

Tactic:
· exact LinearMap.lTensor_surjective S hf

Goal state after:
Module: Mathlib.RingTheory.Extension.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
ι : Type u_1
s : ι → P.Ring
hs : Ideal.span (Set.range s) = P.ker
⊢ Submodule.span S (Set.range fun i ↦ mk ⟨s i, ⋯⟩) = ⊤

Tactic:
rw [Ideal.span, ← Submodule.span_range_subtype_eq_top_iff] at hs

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs✝¹ : Ideal.span (Set.range s) = P.ker
hs✝ : Submodule.span P.Ring (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range fun i ↦ ⟨s i, ⋯⟩) = ⊤
⊢ Submodule.span S (Set.range fun i ↦ mk ⟨s i, ⋯⟩) = ⊤

case hs
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs✝ : Ideal.span (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range s) = P.ker
⊢ ∀ (i : ι), s i ∈ P.ker
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case e_g
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 ι σ
r : σ'
⊢ (fun a b ↦
      (aeval (⇑C ∘ P.val)) (P.σ b) *
        ((algebraMap R (MvPolynomial ι' S)) 1 *
          (Finsupp.mapDomain Sum.inl a).prod fun i k ↦ Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    fun i n ↦ AddMonoidAlgebra.ofCoeff (Finsupp.single i n)

Tactic:
ext u s m

Goal state after:
case e_g
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 ι σ
r : σ'
u : ι' →₀ ℕ
s : S
m : ι' →₀ ℕ
⊢ coeff m
      ((aeval (⇑C ∘ P.val)) (P.σ s) *
        ((algebraMap R (MvPolynomial ι' S)) 1 *
          (Finsupp.mapDomain Sum.inl u).prod fun i k ↦ Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    coeff m (AddMonoidAlgebra.ofCoeff (Finsupp.single u s))
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 ⋯
α : ↥LieSubalgebra.root
⊢ α ∈ J.rootSet ↔ α ∈ I.rootSet

Tactic:
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:
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 ι
s : Set S
hs : adjoin R s = ⊤
⊢ adjoin R {x | x ∈ s} = ⊤

Tactic:
Set.ofPred_mem_eq

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 ι
s : Set S
hs : adjoin R s = ⊤
⊢ adjoin R s = ⊤
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:
rw [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.QuotSMulTop

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : R
⊢ x ∈ Module.annihilator R (QuotSMulTop x M)

Tactic:
by
  refine Module.mem_annihilator.mpr (fun m ↦ ?_)
  rcases Submodule.Quotient.mk_surjective _ m with ⟨m', hm'⟩
  simpa [← hm', ← Submodule.Quotient.mk_smul] using Submodule.smul_mem_pointwise_smul m' x ⊤ trivial

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
ι : Type u_3
inst✝ : Fintype ι
f : ι → R
x : ι → M
h : ∑ i, f i • x i = 0
⊢ ∑ i, (f ∘ ⇑(Fintype.equivFin ι).symm) i • (x ∘ ⇑(Fintype.equivFin ι).symm) i = 0

Tactic:
by
    simpa only [← (Fintype.equivFin ι).symm.sum_comp] using! h

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers 1, r • m = 0) ↔ ∀ (y : M), y = 0

Tactic:
simp only [Submonoid.powers_one, Submonoid.mem_bot, exists_eq_left, one_smul]

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : f m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
⊢ (s * r) • m = 0

Tactic:
rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]

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

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
hji : j.castSucc < i
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)

Tactic:
have : 1 ≤ (i : ℕ) := (Nat.zero_le j).trans_lt hji
    simp [succAbove_of_castSucc_lt _ _ hji, predAbove_of_castSucc_lt _ _ hji, this, iff_comm,
      parity_simps]

Goal state after: