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

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
⊢ finrank K ↥V = (charpoly φ).natTrailingDegree

Tactic:
let e := Submodule.prodEquivOfIsCompl V W hVW

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
⊢ finrank K ↥V = (charpoly φ).natTrailingDegree
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ ⁅⊤, ⊤⁆
⊢ χ x = 0

Tactic:
←
    LieSubmodule.mem_toSubmodule,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ ↑⁅⊤, ⊤⁆
⊢ χ x = 0
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: K : Type u
V : Type v
V' V'₁ : Type v'
inst✝⁶ : Semiring K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : AddCommMonoid V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V'₁
inst✝ : Module K V'₁
g : V →ₗ[K] V'
f : V' →ₗ[K] V'₁
⊢ (f ∘ₗ g).rank ≤ g.rank

Tactic:
simpa only [Cardinal.lift_id] using lift_rank_comp_le_right g f

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
⊢ c ≤ f.rank ↔ ∃ s, lift.{v', v} #↑s = lift.{v, v'} c ∧ LinearIndepOn K (⇑f) s

Tactic:
by
  rcases f.rangeRestrict.exists_rightInverse_of_surjective f.range_rangeRestrict with ⟨g, hg⟩
  have fg : LeftInverse f.rangeRestrict g := LinearMap.congr_fun hg
  refine ⟨fun h => ?_, ?_⟩
  · rcases _root_.le_rank_iff_exists_linearIndependent.1 h with ⟨s, rfl, si⟩
    refine ⟨g '' s, Cardinal.mk_image_eq_lift _ _ fg.injective, ?_⟩
    replace fg : ∀ x, f (g x) = x := by
      intro x
      convert! congr_arg Subtype.val (fg x)
    replace si : LinearIndepOn K (fun x => f (g x)) s := by
      simpa only [fg] using! si.map' _ (ker_subtype _)
    exact si.image_of_comp
  · rintro ⟨s, hsc, si⟩
    have : LinearIndepOn K f.rangeRestrict s :=
      LinearIndependent.of_comp (LinearMap.range f).subtype (by convert! si)
    convert! this.id_image.cardinal_le_rank
    rw [← Cardinal.lift_inj, ← hsc, Cardinal.mk_image_eq_of_injOn_lift]
    exact injOn_iff_injective.2 this.injective

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : f ∈ skewAdjointSubmodule B
hg : g ∈ skewAdjointSubmodule B
⊢ ⁅f, g⁆ ∈ skewAdjointSubmodule B

Tactic:
by
  rw [mem_skewAdjointSubmodule] at *
  have hfg : IsAdjointPair B B (f * g) (g * f) := by rw [← neg_mul_neg g f]; exact hg.comp hf
  have hgf : IsAdjointPair B B (g * f) (f * g) := by rw [← neg_mul_neg f g]; exact hf.comp hg
  change IsAdjointPair B B (f * g - g * f) (-(f * g - g * f)); rw [neg_sub]
  exact hfg.sub hgf

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

Goal state before:
pp: R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ cRank 0 = 0

Tactic:
obtain hn | hn := isEmpty_or_nonempty n

Goal state after:
case inl
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : IsEmpty n
⊢ cRank 0 = 0

case inr
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : Nonempty n
⊢ cRank 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
h : LinearIndependent R w'
this : ∀ (a : m), diagonal w a = 0 ∨ ∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a
⊢ insert 0 (range (diagonal w).col) = insert 0 (range w')

Tactic:
by aesop (add simp [col_eq_transpose, subset_def])

Goal state after:
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : Nontrivial ↥N
⊢ HasCentralRadical k L ∧ ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id

Tactic:
replace hχ : N = ⊤ := N.eq_top_of_isIrreducible k L M

Goal state after:
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : N = ⊤
⊢ HasCentralRadical k L ∧ ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
H : p.toList x = [y]
⊢ False

Tactic:
simpa [card_support_ne_one] using congr_arg length H

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 ∈ E.incl.range

Tactic:
by
    rw [E.IsExtension.exact]
    change _ ∈ E.proj.ker
    simp [E.proj_surjective.hasRightInverse.choose_spec (E.proj z)]

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✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
r : R
x : loopAlgebra R A L
⊢ ((F (r • x)).sum fun a v ↦ a • (Φ ((F f) (-a))) v) = (RingHom.id R) r • (F x).sum fun a v ↦ a • (Φ ((F f) (-a))) v

Tactic:
rw [map_smul, sum_of_support_subset _ support_smul _ (by simp), sum, Finset.smul_sum]
        simp [-smul_eq_mul, smul_comm]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case intro.refine_2.mk
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
⊢ l ~r l.formPerm.toList x

Tactic:
refine (toList_formPerm_isRotated_self _ ?_ hn _ ?_).symm

Goal state after:
case intro.refine_2.mk.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
⊢ 2 ≤ l.length

case intro.refine_2.mk.refine_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
⊢ x ∈ l
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ E.charPoly.degree = ↑E.order

Tactic:
rw [charPoly, degree_sub_eq_left_of_degree_lt]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ ((monomial E.order) 1).degree = ↑E.order

R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (E.coeffs i)).degree < ((monomial E.order) 1).degree
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
J : FractionalIdeal S P
hIJ : I ≤ ↑J
⊢ IsFractional S I

Tactic:
obtain ⟨a, a_mem, ha⟩ := J.isFractional
  use a, a_mem
  intro b b_mem
  exact ha b (hIJ b_mem)

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
⊢ ∀ m ∈ I, ∀ n ∈ J, IsInteger R ((aI * aJ) • (m * n))

Tactic:
intro m hm n hn

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
⊢ IsInteger R ((aI * aJ) • (m * n))
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
⊢ ∀ (x y : P), IsInteger R ((aI * aJ) • x) → IsInteger R ((aI * aJ) • y) → IsInteger R ((aI * aJ) • (x + y))

Tactic:
intro x y hx hy
        rw [smul_add]
        apply isInteger_add hx hy

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
J : FractionalIdeal R₁⁰ K
h : J ≠ 0
⊢ 1 / ↑J = IsLocalization.coeSubmodule K ⊤ / ↑J

Tactic:
IsLocalization.coeSubmodule_top

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✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα_span : Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan
⊢ α ∈ I.rootSet

Tactic:
by_contra hα_not

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα_span : Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan
hα_not : α ∉ I.rootSet
⊢ False
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:
rw [smul_zero]
          exact isInteger_zero

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ (algebraMap A (FractionRing A)) a ≠ 0

Tactic:
exact mt ((injective_iff_map_eq_zero (algebraMap A _)).mp (IsFractionRing.injective A _) _) ha

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ∨ b ∈ I ^ n

Tactic:
by
  cases n; · simp
  by_cases hI0 : I = ⊥; · simpa [pow_succ, hI0] using h
  have : I.IsMaximal := hI.isMaximal hI0
  exact IsMaximal.mul_mem_pow I h

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsLinearMap R fun x ↦ x.1 + x.2

Tactic:
by
  apply IsLinearMap.mk
  · intro x y
    simp only [Prod.fst_add, Prod.snd_add]
    abel
  · simp [smul_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ (s.inf fun i ↦ f i ^ e i) = ∏ i ∈ s, f i ^ e i

Tactic:
rw [prod_eq_iInf_of_pairwise_isCoprime, Finset.inf_eq_iInf s fun i ↦ (f i) ^ e i]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ (↑s).Pairwise (Function.onFun IsCoprime fun i ↦ f i ^ e i)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ Function.Surjective ⇑f

Tactic:
← LinearMap.range_eq_top

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ f.range = ⊤
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: case mp
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach → x✝ ∈ commonDenomOfFinset S f s • ↑s

pp: case mpr
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ commonDenomOfFinset S f s • ↑s → x✝ ∈ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach

Tactic:
· rintro ⟨_, ⟨x, -, rfl⟩, rfl⟩
    rw [map_integerMultiple]
    exact Set.mem_image_of_mem _ x.prop

Goal state after:
case mpr
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ commonDenomOfFinset S f s • ↑s → x✝ ∈ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach
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
⊢ span {a} ∈ normalizedFactors (span {b})

Tactic:
by_cases hb : b = 0
  · rw [span_singleton_eq_bot.mpr hb, bot_eq_zero, normalizedFactors_zero]
    rw [hb, normalizedFactors_zero] at ha
    exact absurd ha (Multiset.notMem_zero a)
  · suffices Prime (span ({a} : Set R)) by
      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)))
      rwa [associated_iff_eq.mp hc']
    · by_contra h
      exact hb (span_singleton_eq_bot.mp h)
    rw [prime_iff_isPrime]
    · exact (span_singleton_prime (prime_of_normalized_factor a ha).ne_zero).mpr
        (prime_of_normalized_factor a ha)
    · by_contra h
      exact (prime_of_normalized_factor a ha).ne_zero (span_singleton_eq_bot.mp h)

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

Goal state before:
pp: 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
⊢ FinitePresentation R M

Tactic:
by
  obtain ⟨n, K, e, hK⟩ := Module.FinitePresentation.exists_fin S M
  let f : (Fin n → S) →ₗ[R] M := (e.symm ∘ₗ K.mkQ).restrictScalars R
  refine Module.finitePresentation_of_surjective f (fun m ↦ ?_) ?_
  · obtain ⟨a, ha⟩ := K.mkQ_surjective (e m)
    exact ⟨a, by simp [f, ha]⟩
  · have : Module.Finite S
        (Submodule.restrictScalars R (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ))) :=
      .of_fg <| show (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ)).FG by simpa
    simp only [f, LinearMap.ker_restrictScalars, ← Module.Finite.iff_fg]
    exact Module.Finite.trans S _

Goal state after:
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✝⁴ : IsDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Algebra.IsIntegral R A
inst✝ : Nontrivial (HeightOneSpectrum R)
this : IsDomain R
⊢ Nontrivial (HeightOneSpectrum A)

Tactic:
let f (p : HeightOneSpectrum A) : HeightOneSpectrum R := p.under R

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Algebra.IsIntegral R A
inst✝ : Nontrivial (HeightOneSpectrum R)
this : IsDomain R
f : HeightOneSpectrum A → HeightOneSpectrum R := fun p ↦ HeightOneSpectrum.under R p
⊢ Nontrivial (HeightOneSpectrum A)
Module: Mathlib.Algebra.Module.Presentation.Cokernel

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
⊢ f.range ≤ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }).ker

Tactic:
LinearMap.range_eq_map,

Goal state after:
A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
⊢ Submodule.map f ⊤ ≤ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }).ker
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: case mul_X
σ : 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
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
p q : MvPolynomial σ R
i : σ
hq : D (p * q) = p • D q + q • D p
⊢ p • q • D (X i) + (X i • p • D q + X i • q • D p) = p • q • D (X i) + (p • X i • D q + q • X i • D p)

Tactic:
rw [smul_comm (X i), smul_comm (X i)]

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

Goal state before:
pp: case map_units
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
⊢ IsUnit ((algebraMap R (End R (M' →ₗ[R] N'))) ↑s)

Tactic:
rw [Module.End.isUnit_iff]

Goal state after:
case map_units
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
⊢ Function.Bijective ⇑((algebraMap R (End R (M' →ₗ[R] N'))) ↑s)
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
this : (Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.pderiv i
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x

Tactic:
rw [← this]; rfl

Goal state after: