mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ : ∀ x ∈ {Z | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥}, ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hIM : I ≤ P.asIdeal
hM : P.asIdeal.IsMaximal
hPM : P.asIdeal ≤ P.asIdeal
⊢ (P.asIdeal ::ₘ Multiset.map asIdeal (Z.erase P)).prod ≤ I

Tactic:
convert! hZI
      rw [this, Multiset.cons_erase hPZ']

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (x y : K),
    x ∈ span R₁ (f '' ↑s) →
      y ∈ span R₁ (f '' ↑s) → IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • y) → IsInteger R₁ (↑a' • (x + y))

Tactic:
intro x y _ _ hx hy

Goal state after:
case refine_3
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x✝ : K
hx✝¹ : x✝ ∈ span R₁ (f '' ↑s)
x y : K
hx✝ : x ∈ span R₁ (f '' ↑s)
hy✝ : y ∈ span R₁ (f '' ↑s)
hx : IsInteger R₁ (↑a' • x)
hy : IsInteger R₁ (↑a' • y)
⊢ IsInteger R₁ (↑a' • (x + y))
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
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 : P
I : FractionalIdeal S P
y' : P
hy' : y' ∈ I
⊢ x * y' ∈ spanSingleton S x * I

Tactic:
exact mul_mem_mul ((mem_spanSingleton S).mpr ⟨1, one_smul _ _⟩) hy'

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

Goal state before:
pp: case refine_1
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
⊢ x ∈ I →
    ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
      x = ((algebraMap R₁ K) a_inv)⁻¹ * y'

Tactic:
intro hx

Goal state after:
case refine_1
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
⊢ ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
    x = ((algebraMap R₁ K) a_inv)⁻¹ * y'
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 : P
I J : FractionalIdeal S P
⊢ (∀ {zI : P}, zI ∈ I → zI ∈ spanSingleton S x * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI

Tactic:
simp only [mem_singleton_mul, eq_comm]

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

Goal state before:
pp: R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
J : FractionalIdeal R₁⁰ K
hJ : J ≤ ↑I
⊢ (↑J).FG

Tactic:
obtain ⟨J, rfl⟩ := le_one_iff_exists_coeIdeal.mp (le_trans hJ coeIdeal_le_one)

Goal state after:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I J : Ideal R₁
hJ : ↑J ≤ ↑I
⊢ (↑↑J).FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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

Tactic:
intro x y _ _ hx hy

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

Tactic:
exact
    strictMono_of_le_iff_le (fun _ _ => (coeIdeal_le_coeIdeal K).symm)
      (lt_top_iff_ne_top.mpr hJ)

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.projection T hST ≈ 0 ↔ IsNoetherian K ↥S

Tactic:
equiv_zero_iff_hasNoetherianRange,

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).HasNoetherianRange ↔ IsNoetherian K ↥S
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
inst✝ : StrongRankCondition R
e : M ≃ₗ[R] N
a✝ : Nontrivial R
⊢ (↑e).index = 0

Tactic:
have := index_of_injective e.injective

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
R : Type u_3
inst✝³ : Ring R
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : StrongRankCondition R
e : M ≃ₗ[R] N
a✝ : Nontrivial R
this : (↑e).index = -↑(finrank R (N ⧸ (↑e).range))
⊢ (↑e).index = 0
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case mp
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
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] ↥⋯.toFinset →₀ R := ⋯
x : ↥⋯.toFinset →₀ R
⊢ (linearCombination R Subtype.val) x = 0 → ∃ y, l y = 0 ∧ f y = x

Tactic:
intro hx

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I ≠ ⊥
l : Ideal R
hl : l ∣ I
l' : Ideal R
hl' : l' ∣ I
⊢ ↑((idealFactorsEquivOfQuotEquiv f).toEquiv ⟨l, hl⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f).toEquiv ⟨l', hl'⟩) ↔
    ↑⟨l, hl⟩ ∣ ↑⟨l', hl'⟩

Tactic:
apply idealFactorsEquivOfQuotEquiv_is_dvd_iso f

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

Goal state before:
pp: R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module A N
inst✝¹ : IsScalarTower R A N
f : M →ₗ[R] N
h : IsBaseChange A f
inst✝ : Module.FinitePresentation R M
⊢ (↑h.equiv).ker.FG

Tactic:
by simpa using Submodule.fg_bot

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
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯

Tactic:
have : Function.Bijective (IsLocalizedModule.map S f g l') := by
    have : IsLocalizedModule.map S f g l' = (s • LinearMap.id) ∘ₗ l := by
      apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
      apply LinearMap.ext fun x ↦ ?_
      simp only [LinearMap.coe_comp, Function.comp_apply, IsLocalizedModule.map_apply]
      rw [← LinearMap.comp_apply, H]
      simp
    rw [this]
    exact ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).comp l.bijective

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,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: case single
R : Type u
inst✝ : CommRing R
x y : R[X]
⊢ ((lsmul R R Ω[R[X]⁄R]).toLinearMap.flip ((D R R[X]) X))
      (derivative'.liftKaehlerDifferential.toFun ((Finsupp.linearCombination R[X] ⇑(D R R[X])) (Finsupp.single x y))) =
    (Finsupp.linearCombination R[X] ⇑(D R R[X])) (Finsupp.single x y)

Tactic:
| single x y =>

Goal state after:
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
q₁ q₂ : Submodule K (Dual K ↥H)
hq₁ : ∀ (i : ↥LieSubalgebra.root), q₁ ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
hq₂ : ∀ (i : ↥LieSubalgebra.root), q₂ ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
h : q₁ ≤ q₂
⊢ invtSubmoduleToLieIdeal q₁ hq₁ ≤ invtSubmoduleToLieIdeal q₂ hq₂

Tactic:
change (invtSubmoduleToLieIdeal q₁ hq₁).restr H ≤ (invtSubmoduleToLieIdeal q₂ hq₂).restr H
  exact iSup_le fun ⟨α, hα_mem, hα_nz⟩ ↦ le_iSup_of_le ⟨α, h hα_mem, hα_nz⟩ le_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 ι
x y : S
e : P.σ x = P.σ y
⊢ (aeval P.val) (P.σ x) = y

Tactic:
← P.aeval_val_σ y,

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) = (aeval P.val) (P.σ y)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P✝ P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ Ideal.span (Set.range (⇑(rename ⇑e.symm) ∘ P.relation ∘ ⇑f)) = RingHom.ker (aeval (P.val ∘ ⇑e))

Tactic:
← aeval_comp_rename,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P✝ P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ Ideal.span (Set.range (⇑(rename ⇑e.symm) ∘ P.relation ∘ ⇑f)) = RingHom.ker ((aeval P.val).comp (rename ⇑e))
Module: Mathlib.Algebra.Module.Presentation.DirectSum

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (pres.finsupp ι).var ⟨i, g⟩ = Finsupp.single i (pres.var g)

Tactic:
apply (finsuppLequivDFinsupp A).injective

Goal state after:
A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (finsuppLequivDFinsupp A) ((pres.finsupp ι).var ⟨i, g⟩) = (finsuppLequivDFinsupp A) (Finsupp.single i (pres.var g))
Module: Mathlib.Algebra.Module.Presentation.Finite

Goal state before:
pp: case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ FinitePresentation A M → ∃ pres, Finite pres.G ∧ Finite pres.R

Tactic:
intro
    obtain ⟨G : Type w₀, _, var, hG⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1
        (finite_def.1 (inferInstance : Module.Finite A M))
    obtain ⟨R : Type w₁, _, relation, hR⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1
        (Module.FinitePresentation.fg_ker (Finsupp.linearCombination A var) (by
          rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hG]))
    exact
     ⟨{ G := G
        R := R
        relation := relation
        var := var
        linearCombination_var_relation := fun r ↦ by
          rw [Submodule.ext_iff] at hR
          exact (hR _).1 (Submodule.subset_span ⟨_, rfl⟩)
        toIsPresentation := by
          rw [Relations.Solution.isPresentation_iff]
          exact ⟨hG, hR.symm⟩ },
        inferInstance, inferInstance⟩

Goal state after:
Module: Mathlib.RingTheory.Extension.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.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
⊢ ∃ a, (LinearMap.liftBaseChange S Cotangent.mk) a = Cotangent.mk x

Tactic:
exact ⟨1 ⊗ₜ x, by simp⟩

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

Goal state before:
pp: case mpr
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 ι
x : Q.Ring
⊢ x ∈ Q.ker → ∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x

Tactic:
intro hx

Goal state after:
case mpr
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 ι
x : Q.Ring
hx : x ∈ Q.ker
⊢ ∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x
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'⟩
  rw [← Fin.cast_val_eq_self k]
  exact h.natCast

Goal state after:
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 N : Submodule R S
r : ↥⊥
n : ↥N
⊢ 1 ⊗ₜ[R] N.lTensorOne' (r ⊗ₜ[R] n) = r ⊗ₜ[R] n

Tactic:
obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
r : ↥⊥
n : ↥N
x : R
h : (algebraMap R S) x = ↑r
⊢ 1 ⊗ₜ[R] N.lTensorOne' (r ⊗ₜ[R] n) = r ⊗ₜ[R] n
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 N : Submodule R S
n : ↥M
r : ↥⊥
⊢ M.rTensorOne' (n ⊗ₜ[R] r) ⊗ₜ[R] 1 = n ⊗ₜ[R] r

Tactic:
obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
n : ↥M
r : ↥⊥
x : R
h : (algebraMap R S) x = ↑r
⊢ M.rTensorOne' (n ⊗ₜ[R] r) ⊗ₜ[R] 1 = n ⊗ₜ[R] r
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
m : ↥M
r : ↥⊥
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)

Tactic:
obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R S) x = ↑r
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)
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
r : ↥⊥
m : ↥M
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)

Tactic:
obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R S) x = ↑r
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
s : Finset ι
f : ι → R
hfv : ∑ i ∈ s, f i • v i = 0
i : ι
hi : i ∈ s
⊢ f i = 0

Tactic:
induction s using Finset.induction generalizing v i with
  | empty => exact (Finset.notMem_empty _ hi).elim
  | insert n s hn ih => ?_

Goal state after:
case insert
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n : ι
s : Finset ι
hn : n ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i ∈ insert n s, f i • v i = 0
i : ι
hi : i ∈ insert n s
⊢ f i = 0
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: case e_6
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a✝ : ⨂[R]^na M
b✝ : ⨂[R]^nb M
c✝ : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
      ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
        ↑LinearMap.lflip)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
          (mul na (nb + nc)).flip ∘ₗ
        mul nb nc)).flip
rhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
j : Fin (na + (nb + nc))
⊢ (Fin.append (Fin.append a b) c ∘ Fin.cast ⋯) j = Fin.append a (Fin.append b c) j

Tactic:
rw [Fin.append_assoc]

Goal state after:
case e_6
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a✝ : ⨂[R]^na M
b✝ : ⨂[R]^nb M
c✝ : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
      ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
        ↑LinearMap.lflip)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
          (mul na (nb + nc)).flip ∘ₗ
        mul nb nc)).flip
rhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
j : Fin (na + (nb + nc))
⊢ ((Fin.append a (Fin.append b c) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯) j = Fin.append a (Fin.append b c) j