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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
s : Finset m
hz : ∀ x ∉ ↑s, A.row x = 0
B : Matrix m (↥s) R := of fun i a ↦ if ↑a = i then 1 else 0
hBdef : B = of fun i a ↦ if ↑a = i then 1 else 0
i : m
j : n
hi : i ∈ s
a : ↥s
ha : a ≠ ⟨i, hi⟩
⊢ (if ↑a = i then 1 else 0) * A (↑a) j = 0

Tactic:
if_neg fun he => ha (Subtype.ext he),

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
s : Finset m
hz : ∀ x ∉ ↑s, A.row x = 0
B : Matrix m (↥s) R := of fun i a ↦ if ↑a = i then 1 else 0
hBdef : B = of fun i a ↦ if ↑a = i then 1 else 0
i : m
j : n
hi : i ∈ s
a : ↥s
ha : a ≠ ⟨i, hi⟩
⊢ 0 * A (↑a) j = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
⊢ diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod *
      ((List.map toMatrix L).prod * diagonal D *
        ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)) =
    diagonal fun i ↦ if i ∈ s then 1 else 0

Tactic:
prod_mul_reverse_inv_prod,

Goal state after:
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
⊢ diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod *
      ((List.map toMatrix L).prod * diagonal D * 1) =
    diagonal fun i ↦ if i ∈ s then 1 else 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
⊢ ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e

Tactic:
obtain ⟨L, L', D, hM0⟩ := Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec M
  set E := fun i ↦ if D i = 0 then 1 else (D i)⁻¹ with E_def
  set s : Finset m := .filter (fun i ↦ D i ≠ 0) .univ with s_def
  set V := diagonal E * (L.reverse.map (toMatrix ∘ .inv)).prod with V_def
  set U := (L'.reverse.map (toMatrix ∘ .inv)).prod with U_def
  have hUdet : IsUnit U.det := (isUnit_iff_isUnit_det _).1 <| isUnit_prod_comp_inverse _
  have hVdet : IsUnit V.det := by
    rw [V_def, det_mul, det_diagonal]
    exact IsUnit.mk0 _ (Finset.prod_ne_zero_iff.2 (by grind)) |>.mul <|
      (isUnit_iff_isUnit_det _).1 (isUnit_prod_comp_inverse _)
  have hM : V * M * U = diagonal (fun i ↦ if i ∈ s then 1 else 0) := by
    rw [V_def, U_def, hM0, mul_assoc, mul_assoc _ (L'.map _).prod, prod_mul_reverse_inv_prod,
      mul_one, ← mul_assoc, mul_assoc _ (L.reverse.map _).prod, reverse_inv_prod_mul_prod, mul_one]
    ext
    simp only [E_def, mul_diagonal, diagonal_apply, ite_mul, one_mul, zero_mul, s_def,
      Finset.mem_filter, Finset.mem_univ, true_and, ite_not]
    split_ifs with h1 h2 <;> first | rw [← h1, h2] | rw [← h1, inv_mul_cancel₀ h2] | rfl
  have hs : s.card = M.rank := by
    simp [← rank_mul_eq_right_of_isUnit_det V M hVdet, ← rank_mul_eq_left_of_isUnit_det U (V * M)
      hUdet, hM, rank_diagonal]
  set e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank) :=
    (Equiv.sumCompl (· ∈ s)).symm.trans <| (Finset.equivFinOfCardEq hs).sumCongr <|
      Fintype.equivFinOfCardEq <| by rw [Fintype.card_subtype_compl, Fintype.card_coe, hs] with he
  refine ⟨V, U, e, (isUnit_iff_isUnit_det _).2 hVdet, isUnit_prod_comp_inverse _, ?_⟩
  rw [hM, ← diagonal_one, ← diagonal_zero, fromBlocks_diagonal, submatrix_diagonal_equiv]
  refine congrArg _ (funext fun i ↦ ?_)
  split_ifs with hi <;> simp [he, hi]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
M : Matrix (l ⊕ l) (l ⊕ l) R
hM : M ∈ symplecticGroup l R
A : Matrix l l R := M.toBlocks₁₁
B : Matrix l l R := M.toBlocks₁₂
C : Matrix l l R := M.toBlocks₂₁
D : Matrix l l R := M.toBlocks₂₂
X : Matrix l l R
hX_symm : X.IsSymm
hA_isUnit : IsUnit (M.toBlocks₁₁ + X * M.toBlocks₂₁).det
Lx_mul : fromBlocks 1 X 0 1 * M = fromBlocks (A + X * C) (B + X * D) C D
h_fromBlocks_in : fromBlocks (A + X * C) (B + X * D) C D ∈ symplecticGroup l R
x✝ : Invertible (A + X * C)
h_main : (fromBlocks 1 X 0 1).det * M.det = 1
⊢ M.det = 1

Tactic:
det_fromBlocks_zero₂₁,

Goal state after:
l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
M : Matrix (l ⊕ l) (l ⊕ l) R
hM : M ∈ symplecticGroup l R
A : Matrix l l R := M.toBlocks₁₁
B : Matrix l l R := M.toBlocks₁₂
C : Matrix l l R := M.toBlocks₂₁
D : Matrix l l R := M.toBlocks₂₂
X : Matrix l l R
hX_symm : X.IsSymm
hA_isUnit : IsUnit (M.toBlocks₁₁ + X * M.toBlocks₂₁).det
Lx_mul : fromBlocks 1 X 0 1 * M = fromBlocks (A + X * C) (B + X * D) C D
h_fromBlocks_in : fromBlocks (A + X * C) (B + X * D) C D ∈ symplecticGroup l R
x✝ : Invertible (A + X * C)
h_main : det 1 * det 1 * M.det = 1
⊢ M.det = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
hl : (x :: l).Nodup
hn : 2 ≤ (x :: l).length
⊢ (x :: l).formPerm.IsCycle

Tactic:
induction l generalizing x with
  | nil => norm_num at hn
  | cons y l =>
    use x
    constructor
    · rwa [formPerm_apply_mem_ne_self_iff _ hl _ mem_cons_self]
    · intro w hw
      have : w ∈ x::y::l := mem_of_formPerm_apply_ne hw
      obtain ⟨k, hk, rfl⟩ := getElem_of_mem this
      use k
      simp only [zpow_natCast, formPerm_pow_apply_head _ _ hl k, Nat.mod_eq_of_lt hk]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ l.formPerm x = l.next x hx

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.formPerm l[k] = l.next l[k] hx
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ (p ^ n) x ∈ p.toList x ↔ x ∈ p.support

Tactic:
mem_toList_iff,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ p.SameCycle x ((p ^ n) x) ∧ x ∈ p.support ↔ x ∈ p.support
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
⊢ ((LinearMap.compr₂ (residuePairing R A L Φ) ↑(TrivialLieModule.equiv R (loopAlgebra R A L) R).symm) f) f = 0

Tactic:
suffices ((F f).sum fun a v ↦ a • Φ (F f (-a)) v) = 0 by simpa

Goal state after:
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
⊢ ((F f).sum fun a v ↦ a • (Φ ((F f) (-a))) v) = 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ E₈.IsSimplyLaced

Tactic:
rw [Matrix.isSimplyLaced_iff_of_linearOrder E₈ E₈_isSymm]

Goal state after:
⊢ ∀ ⦃i j : Fin 8⦄, j < i → E₈ i j = 0 ∨ E₈ i j = -1
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: case pos
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 = 0
⊢ ↑I.num ≤ I * I⁻¹

pp: case neg
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 = 0
⊢ ↑I.num ≤ I * I⁻¹

Tactic:
· rw [hI, num_zero_eq <| FaithfulSMul.algebraMap_injective R₁ K, zero_mul, zero_eq_bot,
      coeIdeal_bot]

Goal state after:
case neg
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 = 0
⊢ ↑I.num ≤ I * I⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case pos
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
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : J = ⊤
⊢ ↑I * (↑I)⁻¹ = 1

Tactic:
← hJ,

Goal state after:
case pos
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
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : J = ⊤
⊢ ↑J = 1
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
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
⊢ ↑I * (↑I)⁻¹ = 1

Tactic:
obtain ⟨J, hJ⟩ : ∃ J : Ideal A, (J : FractionalIdeal A⁰ K) = I * (I : FractionalIdeal A⁰ K)⁻¹ :=
    le_one_iff_exists_coeIdeal.mp mul_one_div_le_one
  by_cases hJ0 : J = ⊥
  · subst hJ0
    refine absurd ?_ hI0
    rw [eq_bot_iff, ← coeIdeal_le_coeIdeal K, hJ]
    exact coe_ideal_le_self_mul_inv K I
  by_cases hJ1 : J = ⊤
  · rw [← hJ, hJ1, coeIdeal_top]
  exact (not_inv_le_one_of_ne_bot (K := K) hJ0 hJ1 (hJ ▸ hI)).elim

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst✝ : p.IsMaximal
⊢ P.LiesOver p ↔ P ∣ map (algebraMap R A) p

Tactic:
liesOver_iff,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst✝ : p.IsMaximal
⊢ p = under R P ↔ P ∣ map (algebraMap R A) p
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
⊢ P ∣ I * J → P ∣ I ∨ P ∣ J

Tactic:
have : P.IsMaximal := by
          refine ⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩
          intro J hJ
          obtain ⟨_J_ne, H, hunit, P_eq⟩ := Ideal.dvdNotUnit_iff_lt.mpr hJ
          exact Ideal.isUnit_iff.mp ((hirr.isUnit_or_isUnit P_eq).resolve_right hunit)
        rw [Ideal.dvd_iff_le, Ideal.dvd_iff_le, Ideal.dvd_iff_le, SetLike.le_def, SetLike.le_def,
          SetLike.le_def]
        contrapose!
        rintro ⟨⟨x, x_mem, x_notMem⟩, ⟨y, y_mem, y_notMem⟩⟩
        exact
          ⟨x * y, Ideal.mul_mem_mul x_mem y_mem,
            mt this.isPrime.mem_or_mem (not_or_intro x_notMem y_notMem)⟩

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✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
⊢ P.IsPrime ∧ P.LiesOver p ↔ P.IsPrime ∧ map (algebraMap R A) p ≤ P

Tactic:
liesOver_iff,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
⊢ P.IsPrime ∧ p = under R P ↔ P.IsPrime ∧ map (algebraMap R A) p ≤ P
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
⊢ P ^ i ≤ I

Tactic:
have h3 := pow_ne_zero (i + 1) hP

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case inl
K : Type u_3
inst✝ : Field K
⊢ factors (span {0}) = Multiset.map (fun q ↦ span {q}) (factors 0)

pp: case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
⊢ factors (span {p}) = Multiset.map (fun q ↦ span {q}) (factors p)

Tactic:
· simpa [Set.singleton_zero] using! normalizedFactors_zero

Goal state after:
case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
⊢ factors (span {p}) = Multiset.map (fun q ↦ span {q}) (factors p)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case e_a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ count J (normalizedFactors I) = multiplicity J I

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), ← FiniteMultiplicity.emultiplicity_eq_multiplicity,
      emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J]

Goal state after:
case e_a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ FiniteMultiplicity J I
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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
t : Finset M
ht : Submodule.span R ↑t = l.ker
H : Function.Surjective ⇑(linearCombination R Subtype.val)
σ : M → ↥s →₀ R
hσ : ∀ (b : M), (linearCombination R Subtype.val) (σ b) = b
this : ⇑(linearCombination R Subtype.val) '' σ '' ↑t = ↑t
⊢ (Submodule.span R (σ '' ↑t) ⊔ (linearCombination R Subtype.val).ker).FG

Tactic:
← Finset.coe_image

Goal state after:
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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
t : Finset M
ht : Submodule.span R ↑t = l.ker
H : Function.Surjective ⇑(linearCombination R Subtype.val)
σ : M → ↥s →₀ R
hσ : ∀ (b : M), (linearCombination R Subtype.val) (σ b) = b
this : ⇑(linearCombination R Subtype.val) '' σ '' ↑t = ↑t
⊢ (Submodule.span R ↑(Finset.image σ t) ⊔ (linearCombination R Subtype.val).ker).FG
Module: Mathlib.Algebra.Module.FinitePresentation

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

Tactic:
← top_le_iff

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

Goal state before:
pp: case refine_2
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ f ((∏ j ∈ s.erase i, (sec j).2) • (sec i).1) = ↑(∏ i ∈ s, (sec i).2) • g i

Tactic:
· simp only [LinearMap.map_smul_of_tower, Submonoid.coe_finsetProd]
    rw [← hsec, ← mul_smul, Submonoid.smul_def]
    congr
    simp only [Submonoid.coe_mul, Submonoid.coe_finsetProd, mul_comm]
    rw [← Finset.prod_insert (f := fun i ↦ ((sec i).snd).val) (s.notMem_erase i),
      Finset.insert_erase hi]

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

Goal state before:
pp: σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ↑F.vars ⊆ s
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F

Tactic:
rw [← mem_supported, supported_eq_range_rename, AlgHom.mem_range] at hF
  obtain ⟨F', hF'⟩ := hF
  use fun z ↦ aeval z F'
  intro x
  simp only [← hF', aeval_rename]

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
inst✝⁶ : FinitePresentation R M
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
ϕ : Mₚ →ₗ[R] Nₚ
hϕ : Function.Surjective ⇑ϕ
φ : M →ₗ[R] N
s : ↥S
hφ : g ∘ₗ φ = s • ϕ ∘ₗ f
⊢ ∃ φ s, ∃ (_ : (IsLocalizedModule.map S f g) φ = s • ϕ), Function.Surjective ⇑((IsLocalizedModule.map S f g) φ)

Tactic:
have hmap : IsLocalizedModule.map S f g φ = s • ϕ := by
    apply IsLocalizedModule.linearMap_ext S f g
    simp [IsLocalizedModule.map_comp, hφ, LinearMap.smul_comp]

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
inst✝⁶ : FinitePresentation R M
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
ϕ : Mₚ →ₗ[R] Nₚ
hϕ : Function.Surjective ⇑ϕ
φ : M →ₗ[R] N
s : ↥S
hφ : g ∘ₗ φ = s • ϕ ∘ₗ f
hmap : (IsLocalizedModule.map S f g) φ = s • ϕ
⊢ ∃ φ s, ∃ (_ : (IsLocalizedModule.map S f g) φ = s • ϕ), Function.Surjective ⇑((IsLocalizedModule.map S f g) φ)
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✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
⊢ ∃ r ∈ S, ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l)

Tactic:
obtain ⟨s₁, hs₁⟩ := Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule S g _ _ H₁

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
⊢ ∃ r ∈ S, ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l)