mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
⊢ ∀ (m : M) (r : R) (x : R[M]),
    m ∉ x.coeff.support →
      r ≠ 0 →
        (∀ (hx : x ∈ gradeBy R (⇑f) i),
            (decomposeAux f) ↑⟨x, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨x, hx⟩) →
          ∀ (hx : single m r + x ∈ gradeBy R (⇑f) i),
            (decomposeAux f) ↑⟨single m r + x, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m r + x, hx⟩

Tactic:
intro m

Goal state after:
case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
⊢ ∀ (r : R) (x : R[M]),
    m ∉ x.coeff.support →
      r ≠ 0 →
        (∀ (hx : x ∈ gradeBy R (⇑f) i),
            (decomposeAux f) ↑⟨x, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨x, hx⟩) →
          ∀ (hx : single m r + x ∈ gradeBy R (⇑f) i),
            (decomposeAux f) ↑⟨single m r + x, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m r + x, hx⟩
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ℳ : ι → Submodule R M
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
⊢ ↑(decomposeLinearEquiv ℳ) ∘ₗ (ℳ i).subtype = lof R ι (fun i ↦ ↥(ℳ i)) i

Tactic:
by
  ext; simp

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

Goal state before:
pp: 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)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
⊢ ∀ a < n + 1 + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}

Tactic:
intro m

Goal state after:
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)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
m : ℕ
⊢ m < n + 1 + 1 → (T χ w) (((toEnd R L V) z ^ m) v) ∈ Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : s.Nodup
x : α
hx : x ∉ s
⊢ (s.formPerm h) x = x

Tactic:
by
  induction s using Quot.inductionOn
  simpa using List.formPerm_apply_of_notMem hx

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
⊢ ⁅E.proj z, y⁆ = E.toKer.symm ⁅z, E.toKer y⁆

Tactic:
obtain ⟨x, hx⟩ : E.proj_surjective.hasRightInverse.choose (E.proj z) - z ∈ E.incl.range := by
    rw [E.IsExtension.exact]
    change _ ∈ E.proj.ker
    simp [E.proj_surjective.hasRightInverse.choose_spec (E.proj z)]
  rw [ringModuleOf_bracket, EmbeddingLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie,
    Subtype.ext_iff, LieSubmodule.coe_bracket, lie_toKer_apply, ZeroMemClass.coe_zero, ← hx,
    LieHom.coe_toLinearMap, ← LieHom.map_lie, trivial_lie_zero M M x y, map_zero]

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

Goal state before:
pp: case neg.succ.succ.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ ∀ x_1 ∈ (p.cycleOf x ^ (m + 1)).support, (p.cycleOf x ^ (n + 1)) x_1 = (p.cycleOf x ^ (m + 1)) x_1

Tactic:
rw [hm']
    intro y hy
    obtain ⟨k, rfl⟩ := hc.exists_pow_eq (mem_support.mp hx) (mem_support.mp hy)
    rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
      (Commute.pow_pow_self _ _ _).eq]

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

Goal state before:
pp: R : Type u_1
N : Type u_2
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
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y : L
⊢ { toFun := fun y_1 ↦ ⟨⁅s (x + y), s y_1⁆ - s ⁅x + y, y_1⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun y ↦ ⟨⁅s x, s y⁆ - s ⁅x, y⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun y_1 ↦ ⟨⁅s y, s y_1⁆ - s ⁅y, y_1⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp; abel

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ (f.toList x).formPerm = f.cycleOf x

pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ (f.toList x).formPerm = f.cycleOf x

Tactic:
· rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (notMem_support.mpr hx),
      formPerm_nil]

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ (f.toList x).formPerm = f.cycleOf x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: 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
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
hx : l.length < 2
⊢ (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x = x

Tactic:
suffices formPerm l = 1 by simp [this]

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
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
hx : l.length < 2
⊢ l.formPerm = 1
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
k : Fin n
α : Fin p → Fin n
i : Fin n
hk : k ∈ Set.range α
⊢ bminor A i k α = 0

Tactic:
obtain ⟨q, rfl⟩ := hk

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin p → Fin n
i : Fin n
q : Fin p
⊢ bminor A i (α q) α = 0
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

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
⊢ m ∈ I → ∀ n ∈ J, IsInteger R ((aI * aJ) • (m * n))
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 : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : (algebraMap R P) n' = aJ • n
⊢ IsInteger R (aI • aJ • (m * n))

Tactic:
mul_comm m,

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
n' : R
hn' : (algebraMap R P) n' = aJ • n
⊢ IsInteger R (aI • aJ • (n * m))
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) (1 / I) = 1 / map (↑h) I

Tactic:
by
  rw [FractionalIdeal.map_div, FractionalIdeal.map_one]

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✝
I : { x // 0 < x }
J K : Ideal A
e : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) I J) ((fun x y ↦ ↑x * y) I K)
⊢ ↑(↑I * J) ≤ ↑(↑I * K)

Tactic:
FractionalIdeal.coeIdeal_le_coeIdeal

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✝
I : { x // 0 < x }
J K : Ideal A
e : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) I J) ((fun x y ↦ ↑x * y) I K)
⊢ ↑I * J ≤ ↑I * K
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : IsNoetherian R₁ ↥↑I
⊢ IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)

Tactic:
by
  classical
  by_cases hx : x = 0
  · rw [hx, map_zero, inv_zero, spanSingleton_zero, zero_mul]
    exact isNoetherian_zero
  have h_gx : algebraMap R₁ K x ≠ 0 :=
    mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).mp (IsFractionRing.injective _ _) x) hx
  have h_spanx : spanSingleton R₁⁰ (algebraMap R₁ K x) ≠ 0 := spanSingleton_ne_zero_iff.mpr h_gx
  rw [isNoetherian_iff] at hI ⊢
  intro J hJ
  rw [← div_spanSingleton, le_div_iff_mul_le h_spanx] at hJ
  obtain ⟨s, hs⟩ := hI _ hJ
  use s * {(algebraMap R₁ K x)⁻¹}
  rw [Finset.coe_mul, Finset.coe_singleton, ← span_mul_span, hs, ← coe_spanSingleton R₁⁰, ←
    coe_mul, mul_assoc, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ h_gx, spanSingleton_one,
    mul_one]

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

Goal state before:
pp: R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
⊢ (ringEquivOfRingEquiv K L f).symm = ringEquivOfRingEquiv L K f.symm

Tactic:
by
  exact (RingEquiv.coe_nonUnitalRingHom_inj_iff (ringEquivOfRingEquiv K L f).symm
          (ringEquivOfRingEquiv L K f.symm)).mpr rfl

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
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ (⇑{ toFun := fun X ↦ ⟨comap (Ideal.Quotient.mk L) (map g (map (Ideal.Quotient.mk J) ↑X)), ⋯⟩, monotone' := ⋯ } ∘
        ⇑{ toFun := fun X ↦ ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩, monotone' := ⋯ })
      x =
    (idealFactorsFunOfQuotHom ⋯) x

Tactic:
OrderHom.coe_mk,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ ((fun X ↦ ⟨comap (Ideal.Quotient.mk L) (map g (map (Ideal.Quotient.mk J) ↑X)), ⋯⟩) ∘
        ⇑{ toFun := fun X ↦ ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩, monotone' := ⋯ })
      x =
    (idealFactorsFunOfQuotHom ⋯) x
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ ((fun X ↦ ⟨comap (Ideal.Quotient.mk L) (map g (map (Ideal.Quotient.mk J) ↑X)), ⋯⟩) ∘
        ⇑{ toFun := fun X ↦ ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩, monotone' := ⋯ })
      x =
    (idealFactorsFunOfQuotHom ⋯) x

Tactic:
OrderHom.coe_mk,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ ((fun X ↦ ⟨comap (Ideal.Quotient.mk L) (map g (map (Ideal.Quotient.mk J) ↑X)), ⋯⟩) ∘ fun X ↦
        ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩)
      x =
    (idealFactorsFunOfQuotHom ⋯) x
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ ⟨comap (Ideal.Quotient.mk L)
        (map g (map (Ideal.Quotient.mk J) ↑⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑x)), ⋯⟩)),
      ⋯⟩ =
    { toFun := fun X ↦ ⟨comap (Ideal.Quotient.mk L) (map (g.comp f) (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩,
        monotone' := ⋯ }
      x

Tactic:
OrderHom.coe_mk,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ ⟨comap (Ideal.Quotient.mk L)
        (map g (map (Ideal.Quotient.mk J) ↑⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑x)), ⋯⟩)),
      ⋯⟩ =
    ⟨comap (Ideal.Quotient.mk L) (map (g.comp f) (map (Ideal.Quotient.mk I) ↑x)), ⋯⟩
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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
I : Ideal R
J : Ideal A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : IsDedekindDomain B
L : Ideal B
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
⊢ ↑{p | p ∣ I} ≃o ↑{p | p ∣ J}

Tactic:
have f_surj : Function.Surjective (f : R ⧸ I →+* A ⧸ J) := f.surjective
  have fsym_surj : Function.Surjective (f.symm : A ⧸ J →+* R ⧸ I) := f.symm.surjective
  refine OrderIso.ofHomInv (idealFactorsFunOfQuotHom f_surj) (idealFactorsFunOfQuotHom fsym_surj)
    ?_ ?_
  · simpa using! idealFactorsFunOfQuotHom_comp fsym_surj f_surj
  · simpa using! idealFactorsFunOfQuotHom_comp f_surj fsym_surj

Goal state after:
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
hf : Function.Surjective ⇑f
this : π.ker ≤ (l ∘ₗ π).ker
⊢ (Submodule.map (l ∘ₗ π).ker.subtype (π ∘ₗ (l ∘ₗ π).ker.subtype).ker).FG

Tactic:
e,

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
hf : Function.Surjective ⇑f
this : π.ker ≤ (l ∘ₗ π).ker
⊢ (Submodule.map (l ∘ₗ π).ker.subtype (l.ker.subtype ∘ₗ f).ker).FG
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₁
⊢ Nonempty (pres₂.CokernelData f g₁)

Tactic:
obtain ⟨s, hs⟩ := pres₂.surjective_π.hasRightInverse

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₁
s : M₂ → pres₂.G →₀ A
hs : Function.RightInverse s ⇑pres₂.π
⊢ Nonempty (pres₂.CokernelData 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✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯

Tactic:
let rs : Submonoid R := (.powers <| r * s)

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := Submonoid.powers (r * ↑s)
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ Function.LeftInverse (⇑((lsmul R R Ω[R[X]⁄R]).toLinearMap.flip ((D R R[X]) X)))
    derivative'.liftKaehlerDifferential.toFun

Tactic:
by
    intro x
    obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ x
    induction x using Finsupp.induction_linear with
    | zero => simp
    | add x y hx hy =>
      simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.flip_apply,
        AlgHom.toLinearMap_apply, lsmul_coe] at *; simp only [*]
    | single x y => simp [polynomial_D_apply _ x]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
⊢ (rootSystem H).IsIrreducible ↔ IsSimple K L

Tactic:
nontriviality L
  have hL : ¬ IsLieAbelian L :=
    (isLieAbelian_iff_subsingleton K (L := L)).not.mpr (not_subsingleton L)
  rw [RootPairing.isIrreducible_iff_invtRootSubmodule, ← isSimple_iff_of_not_isLieAbelian K L hL,
    (lieIdealOrderIso H).isSimpleOrder_iff]

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : ↑x ∈ Ideal.comap f.toRingHom (Ideal.map f.toRingHom (P.ker ^ 2))
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))

Tactic:
Ideal.comap_map_of_surjective' f.toRingHom h,

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : ↑x ∈ P.ker ^ 2 ⊔ RingHom.ker f.toRingHom
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))