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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x y x✝¹ x✝ : L
⊢ ⁅x, (a y) (x✝¹ + x✝)⁆ - ⁅y, (a x) (x✝¹ + x✝)⁆ + ⁅x✝¹ + x✝, (a x) y⁆ - (a ⁅x, y⁆) (x✝¹ + x✝) + (a ⁅x, x✝¹ + x✝⁆) y -
      (a ⁅y, x✝¹ + x✝⁆) x =
    ⁅x, (a y) x✝¹⁆ - ⁅y, (a x) x✝¹⁆ + ⁅x✝¹, (a x) y⁆ - (a ⁅x, y⁆) x✝¹ + (a ⁅x, x✝¹⁆) y - (a ⁅y, x✝¹⁆) x +
      (⁅x, (a y) x✝⁆ - ⁅y, (a x) x✝⁆ + ⁅x✝, (a x) y⁆ - (a ⁅x, y⁆) x✝ + (a ⁅x, x✝⁆) y - (a ⁅y, x✝⁆) x)

Tactic:
simp; abel

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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (⁅((ofProd c).symm x).1, ((ofProd c).symm (y + z)).1⁆,
      (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm (y + z)).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm (y + z)).2⁆ -
        ⁅((ofProd c).symm (y + z)).1, ((ofProd c).symm x).2⁆) =
    (⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆,
        (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ -
          ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆) +
      (⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
        (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
          ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆)

Tactic:
simp; abel

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝² + x✝¹, x✝⁆ = ⁅x✝², x✝⁆ + ⁅x✝¹, x✝⁆

Tactic:
simp; abel

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝², x✝¹ + x✝⁆ = ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆

Tactic:
simp; abel

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 x✝¹ x✝ : L
⊢ ⟨⁅s x, s (x✝¹ + x✝)⁆ - s ⁅x, x✝¹ + x✝⁆, ⋯⟩ = ⟨⁅s x, s x✝¹⁆ - s ⁅x, x✝¹⁆, ⋯⟩ + ⟨⁅s x, s x✝⁆ - s ⁅x, x✝⁆, ⋯⟩

Tactic:
simp; abel

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

Goal state before:
pp: case inl
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
H : ↑(derivedSeries k L 1) = ⊤
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

pp: case inr
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
· obtain _ | _ := subsingleton_or_nontrivial L
    · use 0
      simpa [trivial_lie_zero, mem_weightSpace, nontrivial_iff] using exists_pair_ne V
    · rw [LieSubmodule.toSubmodule_eq_top] at H
      exact ((derivedSeries_lt_top_of_solvable k L).ne H).elim

Goal state after:
case inr
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u n = ∑ k, E.coeffs k * E.mkSol init (n - E.order + ↑k)

Tactic:
← tsub_add_cancel_of_le (le_of_not_gt h'),

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u (n - E.order + E.order) = ∑ k, E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)
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
inst✝ : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x✝ : ↥(Submodule.map (Algebra.linearMap R P) I.num)
y : P
hy : y ∈ Submodule.map (Algebra.linearMap R P) I.num
x : P
hx : x ∈ ↑↑I
hxy : (DistribSMul.toLinearMap R P ↑I.den) x = y
⊢ (DistribSMul.toLinearMap R P I.den) x = y

Tactic:
← hxy

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x✝ : ↥(Submodule.map (Algebra.linearMap R P) I.num)
y : P
hy : y ∈ Submodule.map (Algebra.linearMap R P) I.num
x : P
hx : x ∈ ↑↑I
hxy : (DistribSMul.toLinearMap R P ↑I.den) x = y
⊢ (DistribSMul.toLinearMap R P I.den) x = (DistribSMul.toLinearMap R P ↑I.den) x
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
r : Associates N
hr : r ≤ ↑(d ⟨c₁ 1 ^ s, hs'⟩)
this : r ≤ n
| ⟨c₁ 1 ^ s, hs'⟩

Tactic:
rw [← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩]

Goal state after:
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
r : Associates N
hr : r ≤ ↑(d ⟨c₁ 1 ^ s, hs'⟩)
this : r ≤ n
| d.symm (d ⟨c₁ 1 ^ s, hs'⟩)
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: 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
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
μ : Weight K (↥H) L
hμ : μ.IsZero
⊢ b ∈ Weight.ker

Tactic:
exact LinearMap.mem_ker.mpr (congr_fun hμ b)

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
⊢ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α ≤ ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯

Tactic:
· 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: case mp
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 : R
y : P
⊢ (∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y) → ∃ z, z • (algebraMap R P) x = y

Tactic:
rintro ⟨y', hy', rfl⟩
    obtain ⟨x', rfl⟩ := Submodule.mem_span_singleton.mp hy'
    use x'
    rw [smul_eq_mul, map_mul, Algebra.smul_def]

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
x✝ : DvdNotUnit I J
hI : I ≠ 0
H : Ideal A
hunit : ¬IsUnit H
hmul : J = I * H
h : J = I
⊢ I * H = I * 1

Tactic:
by rw [← hmul, h, mul_one]

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

Goal state before:
pp: case neg.a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ J / spanSingleton R₁⁰ d ≤ 1 / spanSingleton R₁⁰ d * J

pp: case a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ 1 / spanSingleton R₁⁰ d * J ≤ J / spanSingleton R₁⁰ d

Tactic:
· intro x hx
    rw [← mem_coe, coe_div h_spand, Submodule.mem_div_iff_forall_mul_mem] at hx
    specialize hx d (mem_spanSingleton_self R₁⁰ d)
    have h_xd : x = d⁻¹ * (x * d) := by field
    rw [← mem_coe, coe_mul, one_div_spanSingleton, h_xd]
    exact Submodule.mul_mem_mul (mem_spanSingleton_self R₁⁰ _) hx

Goal state after:
case a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ 1 / spanSingleton R₁⁰ d * J ≤ J / spanSingleton R₁⁰ d
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₁
J : FractionalIdeal R₁⁰ K
d : K
⊢ J / spanSingleton R₁⁰ d = spanSingleton R₁⁰ d⁻¹ * J

Tactic:
by
  rw [← one_div_spanSingleton]
  by_cases hd : d = 0
  · simp only [hd, spanSingleton_zero, div_zero, zero_mul]
  have h_spand : spanSingleton R₁⁰ d ≠ 0 := mt spanSingleton_eq_zero_iff.mp hd
  apply le_antisymm
  · intro x hx
    rw [← mem_coe, coe_div h_spand, Submodule.mem_div_iff_forall_mul_mem] at hx
    specialize hx d (mem_spanSingleton_self R₁⁰ d)
    have h_xd : x = d⁻¹ * (x * d) := by field
    rw [← mem_coe, coe_mul, one_div_spanSingleton, h_xd]
    exact Submodule.mul_mem_mul (mem_spanSingleton_self R₁⁰ _) hx
  · rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀ hd, spanSingleton_one, mul_one]

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
⊢ Prime P

Tactic:
refine ⟨hP, mt isUnit_iff.mp h.ne_top, fun I J hIJ => ?_⟩

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
I J : Ideal A
hIJ : P ∣ I * J
⊢ P ∣ I ∨ P ∣ J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ 0 < I⁻¹

Tactic:
by simpa [pos_iff_ne_zero]

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
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₁
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
I J : FractionalIdeal R⁰ K
⊢ ⟨Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑(I * J), ⋯⟩ =
    ⟨Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑I, ⋯⟩ *
      ⟨Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑J, ⋯⟩

Tactic:
simp only [FractionalIdeal.coe_ext_iff, val_eq_coe, coe_mul, coe_mk]
      apply le_antisymm <;> simp only [map_le_iff_le_comap, Submodule.mul_le, mem_coe, mem_comap,
          semilinearEquivOfRingEquiv_apply, map_mul, mem_map_equiv,
          semilinearEquivOfRingEquiv_symm_apply, LinearEquiv.coe_coe]
      · exact fun m hm n hn ↦ Submodule.mul_mem_mul (mem_map_of_mem hm) (mem_map_of_mem hn)
      · exact fun m hm n hn ↦ Submodule.mul_mem_mul hm hn

Goal state after:
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
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : Ideal A
⊢ x✝ ⊓ 0 = 0

Tactic:
simp only [zero_eq_bot, inf_bot_eq]

Goal state after:
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
f : R ⧸ I →+* A ⧸ J
hf : Function.Surjective ⇑f
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
⊢ map (Ideal.Quotient.mk I) X ≤ map (Ideal.Quotient.mk I) Y

Tactic:
rwa [map_le_iff_le_comap, comap_map_of_surjective (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot, mk_ker,
      sup_eq_left.mpr <| le_of_dvd hY]

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

Goal state before:
pp: case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
i : Ideal R
hi : i ∈ {I | I ∈ normalizedFactors (span {r})}
this✝ : i.IsPrime
this : ∃ q ∈ normalizedFactors r, Associated (Submodule.IsPrincipal.generator i) q
⊢ ∃ a, (fun d ↦ ⟨span {↑d}, ⋯⟩) a = ⟨i, hi⟩

Tactic:
obtain ⟨a, ha, ha'⟩ := this

Goal state after:
case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
i : Ideal R
hi : i ∈ {I | I ∈ normalizedFactors (span {r})}
this : i.IsPrime
a : R
ha : a ∈ normalizedFactors r
ha' : Associated (Submodule.IsPrincipal.generator i) a
⊢ ∃ a, (fun d ↦ ⟨span {↑d}, ⋯⟩) a = ⟨i, hi⟩
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
ι : Sort ?u.18
inst✝² : Finite ι
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
⊢ FinitePresentation R (M × N)

Tactic:
have hf : Function.Surjective (LinearMap.fst R M N) := LinearMap.fst_surjective

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
ι : Sort ?u.18
inst✝² : Finite ι
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
hf : Function.Surjective ⇑(LinearMap.fst R M N)
⊢ FinitePresentation R (M × N)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
A : Type u_4
inst✝⁶ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁵ : CommRing B
inst✝⁴ : IsDedekindDomain B
inst✝³ : Algebra A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ (⊥.primesOver B).Finite

Tactic:
have : IsDomain A := IsDomain.of_bot_isPrime A

Goal state after:
case pos
A : Type u_4
inst✝⁶ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁵ : CommRing B
inst✝⁴ : IsDedekindDomain B
inst✝³ : Algebra A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
⊢ (⊥.primesOver B).Finite
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
⊢ torsionOf R M x = Ideal.span {p ^ pOrder hM x}

Tactic:
dsimp only [pOrder]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
⊢ torsionOf R M x = Ideal.span {p ^ Nat.find ⋯}
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x y : S
e : P.σ x = P.σ y
⊢ (algebraMap P.Ring S) (P.σ x) = y

Tactic:
← P.algebraMap_σ y,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x y : S
e : P.σ x = P.σ y
⊢ (algebraMap P.Ring S) (P.σ x) = (algebraMap P.Ring S) (P.σ y)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case mul_X
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
p : MvPolynomial ι T
i : ι
hp :
  (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm p) =
    (aeval (Generators.baseChange T P.toGenerators).val) p
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm (p * X i)) =
    (aeval (Generators.baseChange T P.toGenerators).val) (p * X i)

Tactic:
simp [hp, e]

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

Goal state before:
pp: 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 : mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
y : P.Ring
y_in : y ∈ RingHom.ker f.toRingHom
y_in' : y ∈ P.ker
hy : y - ↑x ∈ P.ker ^ 2
⊢ ↑x - y ∈ P.ker ^ 2

Tactic:
by rwa [← Submodule.neg_mem_iff, neg_sub]

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

Goal state before:
pp: case e'_5
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ i ∈ Finset.map (↑e).toEmbedding (support x) with i.1 = i, (monomial (e.symm i)) (coeff (e.symm i) x) =
    (monomial (e.symm (i, 0))) 1 *
      ∑ x_1 ∈ Finset.map e.toEmbedding (support x) with x_1.1 = i,
        (Q.toComp P).toAlgHom.toRingHom ((monomial x_1.2) (coeff (e.symm x_1) x))

Tactic:
Finset.mul_sum

Goal state after:
case e'_5
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ i ∈ Finset.map (↑e).toEmbedding (support x) with i.1 = i, (monomial (e.symm i)) (coeff (e.symm i) x) =
    ∑ i_1 ∈ Finset.map e.toEmbedding (support x) with i_1.1 = i,
      (monomial (e.symm (i, 0))) 1 * (Q.toComp P).toAlgHom.toRingHom ((monomial i_1.2) (coeff (e.symm i_1) x))
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
⊢ VanishesTrivially R m n

Tactic:
set en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ n i with hen

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
⊢ VanishesTrivially R m n
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Flat R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : N
x : N →ₗ[R] M
h : x f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ ↑e = y ∘ₗ a
haf : a (e.symm f) = 0
⊢ x = y ∘ₗ a ∘ₗ ↑e.symm

Tactic:
rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]

Goal state after: