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

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
w : A
x : V
U : Submodule R V := ⨆ k, U' k
hx : x ∈ U.carrier
i : ℕ
⊢ Submodule.map (T χ w) (U' (i + 1)) ≤ U

Tactic:
· exact (T_apply_succ w i).trans (le_iSup _ _)

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
y : M
z : E.L
⊢ Exists.choose ⋯ (E.proj z) - z ∈ LieIdeal.toLieSubalgebra R E.L E.proj.ker

Tactic:
change _ ∈ E.proj.ker

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
y : M
z : E.L
⊢ Exists.choose ⋯ (E.proj z) - z ∈ E.proj.ker
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p.toList x)[k] = y
⊢ (p.toList x).next (p.toList x)[k] ⋯ = p (p.toList x)[k]

Tactic:
rw [next_getElem _ (nodup_toList _ _), getElem_toList, getElem_toList, ← mul_apply, ← pow_succ']

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p.toList x)[k] = y
⊢ (p ^ ((k + 1) % (p.toList x).length)) x = (p ^ (k + 1)) x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
f : { f // f.IsCycle }
⊢ (fun s ↦ ⟨(↑s).formPerm ⋯, ⋯⟩) ((fun f ↦ ⟨(↑f).toCycle ⋯, ⋯⟩) f) = f

Tactic:
by
    obtain ⟨x, hx, -⟩ := id f.prop
    simpa [toCycle_eq_toList (f : Perm α) f.prop x hx, formPerm_toList, Subtype.ext_iff] using
      f.prop.cycleOf_eq hx

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
hx : -x ∈ (F f).support ∨ -x ∈ Finset.image Neg.neg (F f).support
⊢ x ∈ (F f).support ∨ x ∈ Finset.image (⇑(Equiv.neg A)) (F f).support

Tactic:
obtain (h | h) := hx

Goal state after:
case inl
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
h : -x ∈ (F f).support
⊢ x ∈ (F f).support ∨ x ∈ Finset.image (⇑(Equiv.neg A)) (F f).support

case inr
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
h : -x ∈ Finset.image Neg.neg (F f).support
⊢ x ∈ (F f).support ∨ x ∈ Finset.image (⇑(Equiv.neg A)) (F f).support
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
⊢ Eq1 A 0

Tactic:
ext i j

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ (Spec.stepEntry A)^[0] A i j = Matrix.of (fun i j ↦ (-1) ^ 0 * ∑ α ∈ S 0 i, bminor A i j α) i j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p✝ p : ℕ
ih : Eq1 A p
⊢ Eq1 A (p + 1)

Tactic:
ext i j

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p✝ p : ℕ
ih : Eq1 A p
i j : Fin n
⊢ (Spec.stepEntry A)^[p + 1] A i j = Matrix.of (fun i j ↦ (-1) ^ (p + 1) * ∑ α ∈ S (p + 1) i, bminor A i j α) i j
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:
rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
⊢ (A n).diag = 2

Tactic:
by ext; simp [A]

Goal state after:
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
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
⊢ IsInteger R (aI • b)

Tactic:
by
      rcases mem_inf.mp hb with ⟨hbI, _⟩
      exact hI b hbI

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, this✝¹⟩
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
⊢ b = ⊥

Tactic:
suffices x = ⊥ by
      rw [this, OrderIso.map_bot d] at hx
      refine (Subtype.mk_eq_bot_iff ?_ _).mp hx.symm
      simp

Goal state after:
case refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, this✝¹⟩
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
⊢ x = ⊥
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ E₈.IsSimplyLaced

Tactic:
by
  rw [Matrix.isSimplyLaced_iff_of_linearOrder E₈ E₈_isSymm]; decide

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

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ I.num ≤ 1

Tactic:
simp only [Ideal.one_eq_top, le_top]

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

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ Submodule.map (Algebra.linearMap R₁ K) 1 ≤ 1

Tactic:
rw [Ideal.one_eq_top, Submodule.map_top, one_eq_range]

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

Goal state before:
pp: case e'_2
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
I : FractionalIdeal S P
x✝ : P
⊢ x✝ ∈ (algebraMap R P) ↑I.den • ↑I ↔ x✝ ∈ I.den • ↑I

Tactic:
rw [mem_smul_pointwise_iff_exists, mem_smul_pointwise_iff_exists]

Goal state after:
case e'_2
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
I : FractionalIdeal S P
x✝ : P
⊢ (∃ b ∈ ↑I, (algebraMap R P) ↑I.den • b = x✝) ↔ ∃ b ∈ ↑I, I.den • b = x✝
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg.a
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₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x ∈ ↑J / ↑(spanSingleton R₁⁰ d)
⊢ x ∈ 1 / spanSingleton R₁⁰ d * J

Tactic:
Submodule.mem_div_iff_forall_mul_mem

Goal state after:
case neg.a
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₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : ∀ y ∈ ↑(spanSingleton R₁⁰ d), x * y ∈ ↑J
⊢ x ∈ 1 / spanSingleton R₁⁰ d * J
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 : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : y ∈ corootSpace ⇑α
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
exists_root_index : ∀ (γ : Weight K (↥H) L), γ.IsNonZero → ∃ i, S.root i = Weight.toLinear K (↥H) L γ
h_plus_ne_bot : ¬genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) = ⊥
γ : Weight K (↥H) L :=
  { toFun := ⇑(Weight.toLinear K (↥H) L χ) + ⇑(Weight.toLinear K (↥H) L α), genWeightSpace_ne_bot' := h_plus_ne_bot }
hγ_nonzero : γ.IsNonZero
i : ↥LieSubalgebra.root
hi : S.root i = Weight.toLinear K (↥H) L χ
j : ↥LieSubalgebra.root
hj : S.root j = Weight.toLinear K (↥H) L α
h_sum_in_range : S.root i + S.root j ∈ Set.range ⇑S.root
h_equiv : Weight.toLinear K (↥H) L χ ∈ ↑⟨q, ⋯⟩ ↔ S.root j ∈ ↑⟨q, ⋯⟩
⊢ False

Tactic:
exact h_chi_not_in_q (h_equiv.mpr (by rw [hj]; exact hαq))

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

Tactic:
by
    obtain ⟨_, a, hI, hpI⟩ := SetLike.lt_iff_le_and_exists.mp this
    rw [mem_inv_iff hI0] at hI
    refine ⟨a, fun i hi => ?_, ?_⟩
    -- By definition, `a ∈ I⁻¹` multiplies elements of `I` into elements of `1`,
    -- in other words, `a * f i` is an integer.
    · exact (mem_one_iff _).mp (hI (f i) (Submodule.subset_span (Set.mem_image_of_mem f hi)))
    · contrapose! hpI
      -- And if all `a`-multiples of `I` are an element of `J`,
      -- then `a` is actually an element of `J / I`, contradiction.
      refine (mem_div_iff_of_ne_zero hI0).mpr fun y hy => Submodule.span_induction ?_ ?_ ?_ ?_ hy
      · rintro _ ⟨i, hi, rfl⟩; exact hpI i hi
      · rw [mul_zero]; exact Submodule.zero_mem _
      · intro x y _ _ hx hy; rw [mul_add]; exact Submodule.add_mem _ hx hy
      · intro b x _ hx; rw [mul_smul_comm]; exact Submodule.smul_mem _ b hx

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ I ≤ I ⊔ J ∧ I ⊔ J ∣ J

Tactic:
dvd_iff_le

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ I ≤ I ⊔ J ∧ J ≤ I ⊔ J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ≤ I ∧ J ∣ I ⊓ J

Tactic:
dvd_iff_le

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ≤ I ∧ I ⊓ J ≤ J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
hlcm : lcm I J = I ⊓ J
⊢ gcd I J * lcm I J = I * J

Tactic:
associated_iff_eq.mp (gcd_mul_lcm _ _)

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
hlcm : lcm I J = I ⊓ J
⊢ I * J = I * J
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case refine_4
R : Type u_3
M✝ : Type ?u.7
N : Type ?u.12
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι✝ : Sort ?u.18
inst✝⁴ : Finite ι✝
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), FinitePresentation R (M i)
inst✝ : Finite ι
⊢ ∀ {N : Type u_2} {N' : Type (max u_2 u_1)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], FinitePresentation R N → FinitePresentation R N' → FinitePresentation R (N × N')

Tactic:
introv hN hN'

Goal state after:
case refine_4
R : Type u_3
M✝ : Type ?u.7
N✝ : Type ?u.12
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R M✝
inst✝¹⁰ : AddCommGroup N✝
inst✝⁹ : Module R N✝
ι✝ : Sort ?u.18
inst✝⁸ : Finite ι✝
ι : Type u_1
M : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : ∀ (i : ι), FinitePresentation R (M i)
inst✝⁴ : Finite ι
N : Type u_2
N' : Type (max u_2 u_1)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N
inst✝ : Module R N'
hN : FinitePresentation R N
hN' : FinitePresentation R N'
⊢ FinitePresentation R (N × N')
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
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
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : ↥τ → ↥S
hs' : ∀ (x : ↥τ), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i, s' i
x : ↥σ →₀ R
hxσ : x ∈ ↑τ
⊢ ((∏ i, s' i) • linearCombination R i) x = 0

Tactic:
LinearMap.smul_apply,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
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
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : ↥τ → ↥S
hs' : ∀ (x : ↥τ), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i, s' i
x : ↥σ →₀ R
hxσ : x ∈ ↑τ
⊢ (∏ i, s' i) • (linearCombination R i) x = 0
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
i : σ
s : σ →₀ ℕ
r : R
⊢ r • ((monomial s) 1 • D (X i) + X i • D ((monomial s) 1)) =
    r • (monomial s) 1 • D (X i) + X i • D (r • (monomial s) 1)

Tactic:
smul_add,

Goal state after:
case monomial
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
i : σ
s : σ →₀ ℕ
r : R
⊢ r • (monomial s) 1 • D (X i) + r • X i • D ((monomial s) 1) =
    r • (monomial s) 1 • D (X i) + X i • D (r • (monomial s) 1)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : M → ↥S
hs : ∀ (x : M), s x • g₁ x = s x • g₂ x
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
⊢ ⊤ ≤ (σ.prod s • g₁ - σ.prod s • g₂).ker

Tactic:
← hσ,

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : M → ↥S
hs : ∀ (x : M), s x • g₁ x = s x • g₂ x
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
⊢ Submodule.span R ↑σ ≤ (σ.prod s • g₁ - σ.prod s • g₂).ker
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: case add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
i : σ
p q : MvPolynomial σ R
hp : D (p * X i) = p • D (X i) + X i • D p
hq : D (q * X i) = q • D (X i) + X i • D q
⊢ p • D (X i) + X i • D p + (q • D (X i) + X i • D q) = p • D (X i) + q • D (X i) + X i • (D p + D q)

Tactic:
smul_add,

Goal state after:
case add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
i : σ
p q : MvPolynomial σ R
hp : D (p * X i) = p • D (X i) + X i • D p
hq : D (q * X i) = q • D (X i) + X i • D q
⊢ p • D (X i) + X i • D p + (q • D (X i) + X i • D q) = p • D (X i) + q • D (X i) + (X i • D p + X i • D q)
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' : Submodule.span R (insert 0 ((fun a ↦ Submodule.Quotient.mk a) ∘ s '' {j}ᶜ)) = ⊤
⊢ Submodule.span R (Submodule.Quotient.mk ∘ s '' {j}ᶜ) = ⊤

Tactic:
Submodule.span_insert_zero

Goal state after:
case h.succ.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' : Submodule.span R ((fun a ↦ Submodule.Quotient.mk a) ∘ s '' {j}ᶜ) = ⊤
⊢ Submodule.span R (Submodule.Quotient.mk ∘ s '' {j}ᶜ) = ⊤