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

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
con3 : IsUnit (f Q).toBlocks₂₂
Y : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
Y_def : Y = fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
hY_symm : Y.IsSymm
X : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R := f Vᵀ * Y * f V
X_def : X = f Vᵀ * Y * f V
⊢ f A + f (X.submatrix ⇑s ⇑s * C) = f Vᵀ * (f (Vᵀ⁻¹ * A * U) + Y * f (V * C * U)) * f U⁻¹

Tactic:
f_mul,

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
con3 : IsUnit (f Q).toBlocks₂₂
Y : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
Y_def : Y = fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
hY_symm : Y.IsSymm
X : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R := f Vᵀ * Y * f V
X_def : X = f Vᵀ * Y * f V
⊢ f A + f (X.submatrix ⇑s ⇑s) * f C = f Vᵀ * (f Vᵀ⁻¹ * f A * f U + Y * (f V * f C * f U)) * f U⁻¹
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: case refine_2
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
con3 : IsUnit (f Q).toBlocks₂₂
Y : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
Y_def : Y = fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
hY_symm : Y.IsSymm
X : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R := f Vᵀ * Y * f V
X_def : X = f Vᵀ * Y * f V
⊢ IsUnit ((A + X.submatrix ⇑s ⇑s * C).submatrix ⇑s.symm ⇑s.symm)

Tactic:
have heq' : f (A + X.submatrix s s * C) = (f Vᵀ) * (f Q + Y * (f P)) * f (U⁻¹) := by
      simp_rw [hf, submatrix_add, Pi.add_apply, Q_def, P_def, ← hf, f_mul, hf, mul_add, ← mul_assoc,
        ← inv_submatrix_equiv, add_mul, mul_assoc _ (U.submatrix _ _), mul_inv_of_invertible]
      simp [X_def]; rfl
    rw [← hf, heq', IsUnit.mul_iff, IsUnit.mul_iff]
    refine ⟨⟨isUnit_of_invertible _, ?_⟩, ?_⟩
    · nth_rw 1 [Y_def, heq, ← (f Q).fromBlocks_toBlocks, con2.2]
      simpa [hf, fromBlocks_multiply, fromBlocks_add]
    · exact f_unit <| isUnit_nonsing_inv_iff.2 hU

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
hs : s.Nodup
hs' : s'.Nodup
⊢ s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.Subsingleton ∧ s'.Subsingleton

Tactic:
by
  rw [Cycle.length_subsingleton_iff, Cycle.length_subsingleton_iff]
  induction s, s' using Quotient.inductionOn₂'
  simpa using formPerm_eq_formPerm_iff hs hs'

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
h : f x ≠ x
⊢ x ∈ f.toCycle hf

Tactic:
simp only [toCycle_eq_toList f hf x h, Cycle.mem_coe_iff, toList, mem_iterate, iterate_eq_pow]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
h : f x ≠ x
⊢ ∃ m < (f.cycleOf x).support.card, x = (f ^ m) 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:
obtain ⟨x, hx, -⟩ := id f.prop

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : { f // f.IsCycle }
x : α
hx : ↑f x ≠ x
⊢ (fun s ↦ ⟨(↑s).formPerm ⋯, ⋯⟩) ((fun f ↦ ⟨(↑f).toCycle ⋯, ⋯⟩) f) = f
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
⊢ ∃ c, ((toEnd k L ↥W) z).HasEigenvalue c

Tactic:
have : Nontrivial W := inferInstanceAs (Nontrivial (weightSpace V χ₀))

Goal state after:
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
this : Nontrivial ↥W
⊢ ∃ c, ((toEnd k L ↥W) z).HasEigenvalue c
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ C n i j ≤ 0

Tactic:
simp only [C, Matrix.of_apply]; split_ifs <;> omega

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
n : ℕ
⊢ ↑u n = ↑((fun u ↦ ⟨E.mkSol u, ⋯⟩) ((fun u x ↦ ↑u ↑x) u)) n

Tactic:
apply E.eq_mk_of_is_sol_of_eq_init u.2

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
n : ℕ
⊢ ∀ (n : Fin E.order), ↑u ↑n = (fun u x ↦ ↑u ↑x) u n
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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H

Tactic:
by_cases hp : S.pairing δ γ = 0

Goal state after:
case pos
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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : S.pairing δ γ = 0
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H

case neg
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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_2.inr.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ DvdNotUnit (c j.castSucc) (c j.succ)

Tactic:
refine Associates.dvdNotUnit_iff_lt.2 (h₁ ?_)

Goal state after:
case succ.refine_2.inr.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ j.castSucc < j.succ
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
x : L
⊢ x ∈ LieSubmodule.restr I H ⊓ H.toLieSubmodule → x ∈ ⨆ α ∈ I.rootSet, corootSubmodule ↑α

Tactic:
⟨hxI, hxH⟩

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
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
⊢ x ∈ ⨆ α ∈ I.rootSet, corootSubmodule ↑α
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.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case a
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
⊢ LieSubmodule.restr I H ≤ ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯

Tactic:
rw [lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, restr_inf_cartan_eq_biSup_corootSubmodule]
    apply sup_le
    · exact iSup₂_le fun β hβ ↦ le_iSup₂_of_le β hβ
        (by rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_right)
    · exact iSup₂_le fun α hα ↦ le_iSup₂_of_le α hα
        (by rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_of_le_left le_sup_left)

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
⊢ spanSingleton S x * spanSingleton S y = spanSingleton S (x * y)

Tactic:
by
  apply coeToSubmodule_injective
  simp only [coe_mul, coe_spanSingleton, span_mul_span, singleton_mul_singleton]

Goal state after:
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
⊢ ∀ (a b : FractionalIdeal A⁰ K), a / b = a * b⁻¹

Tactic:
let := (isDedekindDomain_iff_isDedekindDomainInv.mp ‹_›).commGroupWithZero K

Goal state after:
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
this : CommGroupWithZero (FractionalIdeal A⁰ K) :=
  @IsDedekindDomainInv.commGroupWithZero A K inst✝⁴ inst✝³ inst✝¹ inst✝ ⋯ ⋯
⊢ ∀ (a b : FractionalIdeal A⁰ K), a / b = a * b⁻¹
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
this : WellFoundedGT (Ideal A)
x✝¹ x✝ : Ideal A
⊢ DvdNotUnit x✝¹ x✝ ↔ x✝ < x✝¹

Tactic:
exact Ideal.dvdNotUnit_iff_lt

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
this : Multiset.count p (normalizedFactors ?m.252) = 0
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤

Tactic:
rw [this, zero_min, pow_zero, Ideal.one_eq_top]

Goal state after:
Module: Mathlib.LinearAlgebra.LeftExact

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁸ : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst✝⁷ : AddCommGroup M1
inst✝⁶ : AddCommGroup M2
inst✝⁵ : AddCommGroup M3
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M1
inst✝² : Module R M2
inst✝¹ : Module R M3
inst✝ : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact ⇑f ⇑g
surj : Function.Surjective ⇑g
h : M2 →ₗ[R] N
x✝ : ∃ y, y ∘ₗ g = h
y : M3 →ₗ[R] N
hy : y ∘ₗ g = h
⊢ (y ∘ₗ g) ∘ₗ f = 0

Tactic:
LinearMap.comp_assoc,

Goal state after:
case refine_2
R : Type u_1
inst✝⁸ : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst✝⁷ : AddCommGroup M1
inst✝⁶ : AddCommGroup M2
inst✝⁵ : AddCommGroup M3
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M1
inst✝² : Module R M2
inst✝¹ : Module R M3
inst✝ : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact ⇑f ⇑g
surj : Function.Surjective ⇑g
h : M2 →ₗ[R] N
x✝ : ∃ y, y ∘ₗ g = h
y : M3 →ₗ[R] N
hy : y ∘ₗ g = h
⊢ y ∘ₗ g ∘ₗ f = 0
Module: Mathlib.RingTheory.Flat.IsBaseChange

Goal state before:
pp: R : Type u_1
inst✝²¹ : CommRing R
S : Type u_2
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : AddCommGroup M₂
inst✝¹⁶ : AddCommGroup M₃
inst✝¹⁵ : AddCommGroup N₁
inst✝¹⁴ : AddCommGroup N₂
inst✝¹³ : AddCommGroup N₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R N₁
inst✝⁸ : Module R N₂
inst✝⁷ : Module R N₃
inst✝⁶ : Module S N₁
inst✝⁵ : Module S N₂
inst✝⁴ : Module S N₃
inst✝³ : IsScalarTower R S N₁
inst✝² : IsScalarTower R S N₂
inst✝¹ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
inst✝ : Module.Flat R S
isb₂ : IsBaseChange S h₂
isb₃ : IsBaseChange S h₃
exact₁ : Function.Exact ⇑f ⇑g
inj₁ : Function.Injective ⇑f
exact₂ : Function.Exact ⇑f' ⇑g'
inj₂ : Function.Injective ⇑f'
⊢ IsBaseChange S h₁

Tactic:
by
  simp only [IsBaseChange, IsTensorProduct] at isb₂ isb₃ ⊢
  refine LinearMap.bijective_of_bijective_of_injective_of_left_exact
    ((f.baseChange S).restrictScalars R) ((g.baseChange S).restrictScalars R)
    (f'.restrictScalars R) (g'.restrictScalars R) _ _ _ ?_ ?_ ?_ exact₂ isb₂ isb₃.1 ?_ inj₂
  · ext s m
    simpa using congr(s • ($comm₁ m)).symm
  · ext s m
    simpa using congr(s • ($comm₂ m)).symm
  · exact Module.Flat.lTensor_exact S exact₁
  · exact Module.Flat.lTensor_preserves_injective_linearMap f inj₁

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
⊢ IsCoprime I J ↔ gcd I J = 1

Tactic:
rw [isCoprime_iff_codisjoint, codisjoint_iff, one_eq_top, gcd_eq_sup]

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
I J : FractionalIdeal A⁰ K
this :
  spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I + J)) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I ⊓ J))) =
    spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J))
⊢ (I ⊓ J) * (I + J) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * spanSingleton A⁰ ((algebraMap A K) ↑I.den) *
          spanSingleton A⁰ ((algebraMap A K) ↑J.den) *
        spanSingleton A⁰ ((algebraMap A K) ↑J.den)) =
    I * J *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * spanSingleton A⁰ ((algebraMap A K) ↑I.den) *
          spanSingleton A⁰ ((algebraMap A K) ↑J.den) *
        spanSingleton A⁰ ((algebraMap A K) ↑J.den))

Tactic:
convert! this using 1 <;> ring

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
x✝ : ↥⋯.toFinset
x : N
hx : x ∈ ⋯.toFinset
⊢ ∃ a, l (b a) = x

Tactic:
by simpa using hx

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✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf : Function.Injective ⇑(↑e.symm ∘ₗ LinearMap.inl R M P)
hl : (LinearMap.snd R M P ∘ₗ ↑e) ∘ₗ l = LinearMap.id
hg : Function.Surjective ⇑(LinearMap.snd R M P ∘ₗ ↑e)
H : Function.Exact ⇑(↑e.symm ∘ₗ LinearMap.inl R M P) ⇑(LinearMap.snd R M P ∘ₗ ↑e)
⊢ FinitePresentation R M

Tactic:
refine Module.finitePresentation_of_surjective (LinearMap.fst _ _ _ ∘ₗ e.toLinearMap)
    (Prod.fst_surjective.comp e.surjective) ?_

Goal state after:
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf : Function.Injective ⇑(↑e.symm ∘ₗ LinearMap.inl R M P)
hl : (LinearMap.snd R M P ∘ₗ ↑e) ∘ₗ l = LinearMap.id
hg : Function.Surjective ⇑(LinearMap.snd R M P ∘ₗ ↑e)
H : Function.Exact ⇑(↑e.symm ∘ₗ LinearMap.inl R M P) ⇑(LinearMap.snd R M P ∘ₗ ↑e)
⊢ (LinearMap.fst R M P ∘ₗ ↑e).ker.FG
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:
← mem_supported,

Goal state after:
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : F ∈ supported ℤ s
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F
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
this : π.ker ≤ (s₁ • linearCombination R i).ker
x : ↥σ →₀ R
⊢ ((f ∘ₗ π.ker.liftQ (s₁ • linearCombination R i) this ∘ₗ ↑(π.quotKerEquivOfSurjective hπ).symm) ∘ₗ π) x =
    (f ∘ₗ (s₁ • linearCombination R i)) x

Tactic:
LinearMap.comp_assoc,

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
this : π.ker ≤ (s₁ • linearCombination R i).ker
x : ↥σ →₀ R
⊢ (f ∘ₗ (π.ker.liftQ (s₁ • linearCombination R i) this ∘ₗ ↑(π.quotKerEquivOfSurjective hπ).symm) ∘ₗ π) x =
    (f ∘ₗ (s₁ • linearCombination R i)) x