mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * 0
h : J = 0
⊢ False

Tactic:
mul_zero

Goal state after:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = 0
h : J = 0
⊢ False
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
I : Submodule R₁ K
hI : I ≤ ⊥
⊢ I.FG

Tactic:
le_bot_iff

Goal state after:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ I.FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2.refine_2
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
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ a * 0 ∈ ↑J

Tactic:
mul_zero

Goal state after:
case refine_2.refine_2
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
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ 0 ∈ ↑J
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:
ext x; simp [← mem_coe]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M : Submodule R V
inst✝ : IsLattice A M
⊢ Module.Finite R ↥M

Tactic:
Module.Finite.iff_fg

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M : Submodule R V
inst✝ : IsLattice A M
⊢ M.FG
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : CommRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
u v : V →ₗ[K] V₂
A : Submodule K V
quot_A_noeth : IsNoetherian K (V ⧸ A)
eqOn_A : Set.EqOn ⇑u ⇑v ↑A
⊢ u ≈ v

Tactic:
have A_le : A ≤ eqLocus u v := le_eqLocus.mpr eqOn_A

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : CommRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
u v : V →ₗ[K] V₂
A : Submodule K V
quot_A_noeth : IsNoetherian K (V ⧸ A)
eqOn_A : Set.EqOn ⇑u ⇑v ↑A
A_le : A ≤ u.eqLocus v
⊢ u ≈ v
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
⊢ (∃ M, M.IsMaximal ∧ I ≤ M) → ∃ P, I ≤ P.asIdeal

Tactic:
rintro ⟨M, hMmax, hIM⟩

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
hR : ¬IsField R
I M : Ideal R
hMmax : M.IsMaximal
hIM : I ≤ M
⊢ ∃ P, I ≤ P.asIdeal
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
R : Type u_3
inst✝³ : Ring R
inst✝² : Module R M
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : StrongRankCondition R
hf : Surjective ⇑f
⊢ ↑(finrank R ↥f.ker) - ↑(finrank R (N ⧸ ⊤)) = ↑(finrank R ↥f.ker)

Tactic:
simp [finrank_eq_zero_of_subsingleton]

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

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : Ring R
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
a✝ : Nontrivial R
⊢ ↑(finrank R ↥id.ker) - ↑(finrank R (M ⧸ ⊤)) = 0

Tactic:
simp [finrank_eq_zero_of_subsingleton]

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), ⋯⟩
σ : ↥⋯.toFinset → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : ↥⋯.toFinset), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
⊢ FinitePresentation R N

Tactic:
refine ⟨(Set.finite_range (l ∘ b)).toFinset,
    by simpa [Set.range_comp, LinearMap.range_eq_top], ?_⟩

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✝¹ : 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), ⋯⟩
σ : ↥⋯.toFinset → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : ↥⋯.toFinset), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
⊢ (linearCombination R Subtype.val).ker.FG
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring 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'
a : R
x : M'
hx : IsInteger f x
⊢ IsInteger f (a • x)

Tactic:
by
  rcases hx with ⟨x', hx⟩
  use a • x'
  rw [← hx, LinearMapClass.map_smul]

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

Goal state before:
pp: case refine_1
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
⊢ ↑{d | d ∈ normalizedFactors r} → ↑{I | I ∈ normalizedFactors (span {r})}

Tactic:
exact fun d =>
      ⟨span {↑d}, singleton_span_mem_normalizedFactors_of_mem_normalizedFactors d.prop⟩

Goal state after:
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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1

Tactic:
have : p ^ k • f1.choose ∈ R ∙ z := by
    rw [← Quotient.mk_eq_zero, mk_smul, f1.choose_spec, ← f.map_smul]
    convert! f.map_zero; change _ • Submodule.Quotient.mk _ = _
    rw [← mk_smul, Quotient.mk_eq_zero, smul_eq_mul, mul_one]
    exact Submodule.mem_span_singleton_self _

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ R ∙ z
⊢ ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ.refine_3.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
⊢ M ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ R ∙ p ^ (fun i ↦ Option.rec (pOrder hM (s j)) k i) ((finSuccEquiv d) i)

Tactic:
refine
          (lequivProdOfRightSplitExact
            (g := f.toLinearMap.comp <| mkQ _)
            (f := (DirectSum.toModule _ _ _ fun i => (liftQSpanSingleton (p ^ k i)
                (LinearMap.toSpanSingleton _ _ _) (this i).choose_spec.left : R ⧸ _ →ₗ[R] _)))
              (R ∙ s j).injective_subtype ?_ ?_).symm ≪≫ₗ
          (((quotTorsionOfEquivSpanSingleton R M (s j)).symm ≪≫ₗ
            (quotEquivOfEq (torsionOf R M (s j)) _
              (Ideal.torsionOf_eq_span_pow_pOrder hp hM (s j)))).prodCongr (.refl _ _)) ≪≫ₗ
          (@DirectSum.lequivProdDirectSum R _ _
            (fun i => R ⧸ R ∙ p ^ @Option.rec _ (fun _ => ℕ) (pOrder hM <| s j) k i) _ _).symm ≪≫ₗ
          (DirectSum.lequivCongrLeft R (finSuccEquiv d).symm)
        · rw [range_subtype, LinearEquiv.ker_comp, ker_mkQ]
        · rw [LinearMap.comp_assoc]
          ext i : 3
          simp only [LinearMap.coe_comp, Function.comp_apply, mkQ_apply]
          rw [LinearEquiv.coe_toLinearMap, LinearMap.id_apply, DirectSum.toModule_lof,
            liftQSpanSingleton_apply, LinearMap.toSpanSingleton_apply_one, Ideal.Quotient.mk_eq_mk,
            map_one (Ideal.Quotient.mk _), (this i).choose_spec.right]

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

Goal state before:
pp: case map_units.right
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommGroup N'✝
inst✝⁸ : Module R N'✝
S : Submonoid R
f✝ : N →ₗ[R] N'✝
inst✝⁷ : IsLocalizedModule S f✝
M' : Type u_1
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
f : M →ₗ[R] M'
inst✝⁴ : IsLocalizedModule S f
N' : Type u_2
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g
inst✝ : FinitePresentation R M
s : ↥S
this : Function.Bijective ⇑((algebraMap R (End R N')) ↑s)
⊢ Function.Surjective ⇑((algebraMap R (End R (M' →ₗ[R] N'))) ↑s)

Tactic:
· intro h
      use ((IsLocalizedModule.map_units (S := S) (f := g) s).unit⁻¹).1 ∘ₗ h
      ext x
      exact Module.End.isUnit_apply_inv_apply_of_isUnit
        (IsLocalizedModule.map_units (S := S) (f := g) s) (h x)

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ x ∈ {C r * X () - 1}, (aeval fun x ↦ invSelf r) x = 0

pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ (aeval fun x ↦ invSelf r) 0 = 0

pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ (x y : MvPolynomial Unit R),
    x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
      y ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
        (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) y = 0 → (aeval fun x ↦ invSelf r) (x + y) = 0

pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ (a x : MvPolynomial Unit R),
    x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) → (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) (a • x) = 0

Tactic:
· rintro p ⟨q, rfl⟩
      simp

Goal state after:
case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ (aeval fun x ↦ invSelf r) 0 = 0

case refine_3
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ (x y : MvPolynomial Unit R),
    x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
      y ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
        (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) y = 0 → (aeval fun x ↦ invSelf r) (x + y) = 0

case refine_4
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ (a x : MvPolynomial Unit R),
    x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) → (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) (a • x) = 0
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
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
⊢ ↑(invtSubmoduleToLieIdeal q hq) = ↑(⨆ α, sl2SubmoduleOfRoot ⋯)

Tactic:
coe_invtSubmoduleToLieIdeal_eq_iSup,

Goal state after:
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
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
⊢ ↑(⨆ α, sl2SubmoduleOfRoot ⋯) = ↑(⨆ α, sl2SubmoduleOfRoot ⋯)
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
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
α : ↥LieSubalgebra.root
⊢ α ∈ (invtSubmoduleToLieIdeal q hq).rootSet ↔ (rootSystem H).root α ∈ q

Tactic:
set J := invtSubmoduleToLieIdeal q hq
  constructor
  · intro hα_mem
    by_contra hα_not
    have hα_nz := H.isNonZero_coe_root α
    have hne (χ : Weight K H L) (hχ : ↑χ ∈ q) : (χ : H → K) ≠ ((α : Weight K H L) : H → K) :=
      fun heq ↦ hα_not (by simpa [rootSystem_root_apply] using DFunLike.coe_injective heq ▸ hχ)
    have h_le : J.restr H ≤ ⨆ (χ : H → K) (_ : χ ≠ (α : Weight K H L)), genWeightSpace L χ := by
      refine iSup_le fun ⟨β, hβ_mem, hβ_nz⟩ ↦ ?_
      rw [sl2SubmoduleOfRoot_eq_sup]
      refine sup_le (sup_le ?_ ?_) ?_
      · exact le_iSup₂_of_le _ (hne β hβ_mem) le_rfl
      · have : ↑(-β) ∈ q := by rw [Weight.toLinear_neg]; exact q.neg_mem hβ_mem
        exact le_iSup₂_of_le _ (hne (-β) this) le_rfl
      · apply (LieSubmodule.map_incl_le.trans (rootSpace_zero_eq K L H).symm.le).trans
        exact le_iSup₂_of_le 0 (fun h ↦ hα_nz h.symm) le_rfl
    have h_disj := ((iSupIndep_genWeightSpace K H L _).mono_right h_le).mono_right hα_mem
    exact (α : Weight K H L).genWeightSpace_ne_bot L (disjoint_self.mp h_disj)
  · intro hα
    calc rootSpace H (α : Weight K H L)
        ≤ sl2SubmoduleOfRoot (H.isNonZero_coe_root α) := by
          rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_of_le_left le_sup_left
      _ ≤ ⨆ x : {β : Weight K H L // ↑β ∈ q ∧ β.IsNonZero}, sl2SubmoduleOfRoot x.2.2 :=
          le_iSup_of_le ⟨↑α, hα, H.isNonZero_coe_root α⟩ le_rfl
      _ = J.restr H := (restr_invtSubmoduleToLieIdeal_eq_iSup q hq).symm

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

Goal state before:
pp: case e_6
R : Type u
S : Type v
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹³ : CommRing R'
inst✝¹² : CommRing S'
inst✝¹¹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁰ : CommRing R''
inst✝⁹ : CommRing S''
inst✝⁸ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra R' S''
inst✝⁴ : Algebra S S'
inst✝³ : Algebra S' S''
inst✝² : Algebra S S''
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
r : P.Ring
⊢ ↑⟨f.toAlgHom ↑(r • x), ⋯⟩ = ↑(f.toRingHom r • ⟨f.toAlgHom ↑x, ⋯⟩)

Tactic:
simp only [SetLike.val_smul, smul_eq_mul, map_mul, Hom.toAlgHom_apply]

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
R' : Type ?u.16
S' : Type ?u.18
inst✝¹³ : CommRing R'
inst✝¹² : CommRing S'
inst✝¹¹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁰ : CommRing R''
inst✝⁹ : CommRing S''
inst✝⁸ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra R' S''
inst✝⁴ : Algebra S S'
inst✝³ : Algebra S' S''
inst✝² : Algebra S S''
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
r : S
x : P.Cotangent
⊢ of ((P.ker.mapCotangent P'.ker f.toAlgHom ⋯) (r • x).val) =
    (RingHom.id S) r • of ((P.ker.mapCotangent P'.ker f.toAlgHom ⋯) x.val)

Tactic:
ext
    obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
    obtain ⟨r, rfl⟩ := P.algebraMap_surjective r
    simp only [algebraMap_smul, val_smul', val_mk, val_of, Ideal.mapCotangent_toCotangent,
      RingHomCompTriple.comp_apply, ← (Ideal.toCotangent _).map_smul]
    conv_rhs => rw [← algebraMap_smul S', ← f.algebraMap_toRingHom, algebraMap_smul, val_smul',
      val_of, ← (Ideal.toCotangent _).map_smul]
    congr 1
    ext1
    simp only [SetLike.val_smul, smul_eq_mul, map_mul, Hom.toAlgHom_apply]

Goal state after:
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 : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'
m'_eq : m' = Subtype.coind m mem_M'
hm' : span R (Set.range m') = ⊤
⊢ ∑ i, m' i ⊗ₜ[R] n i = 0

Tactic:
apply hm

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 : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := ⋯
m'_eq : m' = Subtype.coind m mem_M'
hm' : span R (Set.range m') = ⊤
⊢ (rTensor N (span R (Set.range m)).subtype) (∑ i, m' i ⊗ₜ[R] n i) = (rTensor N (span R (Set.range m)).subtype) 0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case mp
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 ι
x : Q.Ring
⊢ (∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x) → x ∈ Q.ker

Tactic:
rintro ⟨x, hx, rfl⟩
    simp only [ker_eq_ker_aeval_val,
      RingHom.mem_ker] at hx ⊢
    rw [← hx, Hom.algebraMap_toAlgHom, algebraMap_self_apply]

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ m, (R ∙ m).annihilator ≤ p.asIdeal

Tactic:
not_imp_not,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (∃ m, ∀ (r : R), r • m = 0 → r ∈ p.asIdeal) ↔ ∃ m, (R ∙ m).annihilator ≤ p.asIdeal
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal) → p ∈ support R M

Tactic:
· intro ⟨m, _, hm⟩
    exact mem_support_iff_exists_annihilator.mpr ⟨m, hm⟩

Goal state after: