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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
t : Finset K := (constantCoeff ψ).roots.toFinset
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
⊢ ∃ s, r ≤ s.card ∧ ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0

Tactic:
use s \ t

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⋯
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⋯
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L := ⋯
hx₀ : x ≠ 0
Q : Type u_2 := ⋯
r : ℕ := ⋯
hr : r < finrank K L
x' : ↥U := ⋯
y' : ↥U := ⋯
u : ↥U := ⋯
χ : K[X][X] := ⋯
ψ : K[X][X] := ⋯
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
t : Finset K := ⋯
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
⊢ r ≤ (s \ t).card ∧ ∀ α ∈ s \ t, eval α (constantCoeff ψ) ≠ 0
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1✝ D2✝ : Derivation R A A
a✝ : A
D1 D2 : Derivation R A A
a b : A
⊢ a * D1 (D2 b) + D2 b * D1 a + (b * D1 (D2 a) + D2 a * D1 b) -
      (a * D2 (D1 b) + D1 b * D2 a + (b * D2 (D1 a) + D1 a * D2 b)) =
    a * (D1 (D2 b) - D2 (D1 b)) + b * (D1 (D2 a) - D2 (D1 a))

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ d (f a) + e (f a) - (f (d a) + f (e a)) = d (f a) - f (d a) + (e (f a) - f (e a))

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d + e, f⁆ = ⁅d, f⁆ + ⁅e, f⁆

Tactic:
by ext a; simp only [commutator_apply, add_apply, map_add]; ring

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ d (e a) + d (f a) - (e (d a) + f (d a)) = d (e a) - e (d a) + (d (f a) - f (d a))

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d, e + f⁆ = ⁅d, e⁆ + ⁅d, f⁆

Tactic:
by ext a; simp only [commutator_apply, add_apply, map_add]; ring

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ d (e (f a)) - d (f (e a)) - (e (f (d a)) - f (e (d a))) =
    d (e (f a)) - e (d (f a)) - (f (d (e a)) - f (e (d a))) + (e (d (f a)) - e (f (d a)) - (d (f (e a)) - f (d (e a))))

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
x✝² x✝¹ : Derivation R A A
x✝ : A
⊢ x✝² (x✝¹ x✝) = ⁅x✝², x✝¹⁆ x✝ + x✝¹ (x✝² x✝)

Tactic:
by rw [commutator_apply]; abel

Goal state after:
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
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
hmby✝ : single m b + y ∈ gradeBy R (⇑f) i
hmby : ↑((single m b).coeff + y.coeff).support ⊆ ⇑f ⁻¹' {i}
this : Disjoint (Finsupp.single m b).support y.coeff.support
⊢ (decomposeAux f) ↑⟨single m b + y, hmby✝⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m b + y, hmby✝⟩

Tactic:
coeff_single,

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
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
hmby✝ : single m b + y ∈ gradeBy R (⇑f) i
hmby : ↑(Finsupp.single m b + y.coeff).support ⊆ ⇑f ⁻¹' {i}
this : Disjoint (Finsupp.single m b).support y.coeff.support
⊢ (decomposeAux f) ↑⟨single m b + y, hmby✝⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m b + y, hmby✝⟩
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ (x :: y :: l).formPerm x ≠ x

pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ ∀ ⦃y_1 : α⦄, (x :: y :: l).formPerm y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1

Tactic:
· rwa [formPerm_apply_mem_ne_self_iff _ hl _ mem_cons_self]

Goal state after:
case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ ∀ ⦃y_1 : α⦄, (x :: y :: l).formPerm y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: case h
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
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x : LieAlgebra.ofTwoCocycle c
hx :
  x ∈
    LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      { toFun := fun x ↦ ((ofProd c).symm x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.ker
this : ((ofProd c).symm x).1 = 0
⊢ (ofProd c) (0, ((ofProd c).symm x).2) = x

Tactic:
nth_rw 2 [← Equiv.apply_symm_apply (ofProd c) x]

Goal state after:
case h
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
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x : LieAlgebra.ofTwoCocycle c
hx :
  x ∈
    LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      { toFun := fun x ↦ ((ofProd c).symm x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.ker
this : ((ofProd c).symm x).1 = 0
⊢ (ofProd c) (0, ((ofProd c).symm x).2) = (ofProd c) ((ofProd c).symm x)
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case inr
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
h : -x ∈ Finset.image Neg.neg (F f).support
⊢ x ∈ (F f).support ∨ x ∈ Finset.image (⇑(Equiv.neg A)) (F f).support

Tactic:
exact Or.inl <| by simpa using h

Goal state after:
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 : ℕ
i : Fin n
hEq1 : Eq1 A p
⊢ -((-1) ^ p * ∑ i > i, ∑ α ∈ S p i, bminor A i i α) = (-1) ^ (p + 1) * ∑ i > i, ∑ α ∈ S p i, bminor A i i α

Tactic:
ring

Goal state after:
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 : ℕ
i j : Fin n
hEq1 : Eq1 A p
⊢ (-1) ^ (p + 1) * ∑ i_1 ∈ S (p + 1) i, pminor A i_1 * A i j +
      (-1) ^ p * ∑ i_1 > i, ∑ i_2 ∈ S p i, bminor A i i_1 i_2 * A i_1 j =
    (-1) ^ (p + 1) * (∑ α ∈ S (p + 1) i, pminor A α * A i j - ∑ k > i, ∑ α ∈ S p i, bminor A i k α * A k j)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² : Derivation R A₁ A₁
x✝¹ x✝ : A₁
⊢ x✝ * x✝² x✝¹ = x✝² x✝¹ * x✝

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² x✝¹ : Derivation R A₁ A₁
x✝ a✝ : A₁
⊢ x✝ * x✝² (x✝¹ a✝) + x✝¹ a✝ * x✝² x✝ - x✝ * x✝¹ (x✝² a✝) = x✝ * (x✝² (x✝¹ a✝) - x✝¹ (x✝² a✝)) + x✝² x✝ * x✝¹ a✝

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m ∈ p

Tactic:
suffices a • m = a ⊗ₜ[R] (1 : B) • m by exact this.symm ▸ p.smul_mem _ hm
  simp [TensorProduct.Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case pos
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 = init ⟨n, h'⟩

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,
      have x := ⋯;
      E.coeffs k * E.mkSol init (n - E.order + ↑k)

Tactic:
· exact mod_cast heq ⟨n, 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 =
    ∑ k,
      have x := ⋯;
      E.coeffs k * E.mkSol init (n - E.order + ↑k)
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : E.IsSolution u
hv : E.IsSolution v
⊢ u = v ↔ Set.EqOn u v ↑(range E.order)

Tactic:
replace hu : u ∈ E.solSpace := (is_sol_iff_mem_solSpace _ _).mp hu

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hv : E.IsSolution v
hu : u ∈ E.solSpace
⊢ u = v ↔ Set.EqOn u v ↑(range E.order)
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
h : q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0
n : ℕ
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ q ^ n * (E.coeffs x✝¹ * q ^ ↑x✝¹) = E.coeffs x✝¹ * (q ^ n * q ^ ↑x✝¹)

Tactic:
ring

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

Goal state before:
pp: case mp.refine_4.mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
y : R
hy : y ∈ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
eq_y : (Algebra.linearMap R P) y = x
⊢ x ∈ J

Tactic:
← eq_y

Goal state after:
case mp.refine_4.mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
y : R
hy : y ∈ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
eq_y : (Algebra.linearMap R P) y = x
⊢ (Algebra.linearMap R P) y ∈ J
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
⊢ (A n).IsSimplyLaced

Tactic:
intro i j h

Goal state after:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ A n i j = 0 ∨ A n i j = -1
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
⊢ (D n).IsSimplyLaced

Tactic:
intro i j h

Goal state after:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ D n i j = 0 ∨ D n i j = -1
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
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule = ⨆ α ∈ I.rootSet, corootSubmodule ↑α

Tactic:
refine le_antisymm ?_ (iSup₂_le fun _ hα ↦
    le_inf (I.corootSubmodule_le hα) LieSubmodule.map_incl_le)
  intro x ⟨hxI, hxH⟩
  let f : H.root → LieIdeal K H := fun α ↦ corootSpace α.1
  set span_I_roots := ⨆ α ∈ I.rootSet, f α
  set span_compl_roots := ⨆ (β : H.root) (_ : β ∉ I.rootSet), f β
  have h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α :=
    (iSup_split f (· ∈ I.rootSet)).symm
  have h_top : span_I_roots ⊔ span_compl_roots = ⊤ := by
    rw [h_split, eq_top_iff, ← biSup_corootSpace_eq_top]
    exact iSup₂_le fun α hα ↦ le_iSup_of_le ⟨α, by simpa [LieSubalgebra.root] using hα⟩ le_rfl
  have hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
      ⨆ α ∈ I.rootSet, corootSubmodule α.1 := by
    change LieSubmodule.map _ (⨆ α ∈ I.rootSet, f α) = ⨆ α ∈ I.rootSet, _
    simp_rw [LieSubmodule.map_iSup]; rfl
  have hspan_compl_roots_vanish (μ : H.root) (hμ : μ ∈ I.rootSet) :
      span_compl_roots.toSubmodule ≤ μ.1.ker := by
    have : span_compl_roots.toSubmodule = ⨆ β ∉ I.rootSet, (f β).toSubmodule := by
      simp_rw [span_compl_roots, LieSubmodule.iSup_toSubmodule]
    rw [this]
    exact iSup₂_le fun γ hγ ↦ by
      rw [coe_corootSpace_eq_span_singleton, Submodule.span_singleton_le_iff_mem, LinearMap.mem_ker]
      exact I.rootSet_apply_coroot_eq_zero_of_notMem_rootSet hμ hγ
  have hx_top : (⟨x, hxH⟩ : H) ∈ span_I_roots ⊔ span_compl_roots := h_top ▸ trivial
  obtain ⟨a, ha, b, hb, hab⟩ := Submodule.mem_sup.mp hx_top
  have haI : (a : L) ∈ I :=
    (iSup₂_le (fun _ hα ↦ I.corootSubmodule_le hα) :
      ⨆ α ∈ I.rootSet, corootSubmodule α.1 ≤ _)
      (hspan_I_roots_incl ▸ LieSubmodule.mem_map_of_mem ha)
  have hbI : (b : L) ∈ I := by
    have h_sum : (a : L) + b = x := congr_arg Subtype.val hab
    have h_b_eq : (b : L) = x - a := by rw [← h_sum, add_sub_cancel_left]
    rw [h_b_eq]; exact I.toSubmodule.sub_mem hxI haI
  suffices b = 0 by
    subst this; simp only [add_zero] at hab; subst hab
    exact hspan_I_roots_incl ▸ LieSubmodule.mem_map_of_mem ha
  suffices b ∈ ⨅ α : Weight K H L, α.ker by simpa [iInf_ker_weight_eq_bot] using this
  refine (Submodule.mem_iInf _).mpr fun μ ↦ ?_
  by_cases hμ : μ.IsNonZero
  · have hμ_root : μ ∈ H.root := by simpa [LieSubalgebra.root] using hμ
    by_cases hμI : (⟨μ, hμ_root⟩ : H.root) ∈ I.rootSet
    · exact hspan_compl_roots_vanish ⟨μ, hμ_root⟩ hμI hb
    · exact I.root_apply_eq_zero_of_notMem_rootSet hbI hμI
  · simp only [Weight.IsNonZero, not_not] at hμ
    exact LinearMap.mem_ker.mpr (congr_fun hμ b)

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
s : Set P
x✝¹ : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x✝ : P
hb : x✝ ∈ span R s
⊢ IsInteger R (a • 0)

Tactic:
smul_zero

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
s : Set P
x✝¹ : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x✝ : P
hb : x✝ ∈ span R s
⊢ IsInteger R 0
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ ↑I.den • i ∈ ↑1

Tactic:
coe_one

Goal state after:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ ↑I.den • i ∈ 1
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
P' : Type u_3
inst✝⁴ : CommRing P'
inst✝³ : Algebra R P'
P'' : Type u_4
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
inst✝ : IsLocalization S P
I : (Submodule R P)ˣ
⊢ ↑⟨↑I, ⋯⟩ * ↑⟨↑I⁻¹, ⋯⟩ = ↑1

Tactic:
coe_one

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
P' : Type u_3
inst✝⁴ : CommRing P'
inst✝³ : Algebra R P'
P'' : Type u_4
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
inst✝ : IsLocalization S P
I : (Submodule R P)ˣ
⊢ ↑⟨↑I, ⋯⟩ * ↑⟨↑I⁻¹, ⋯⟩ = 1
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
P' : Type u_3
inst✝⁴ : CommRing P'
inst✝³ : Algebra R P'
P'' : Type u_4
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
inst✝ : IsLocalization S P
I : (Submodule R P)ˣ
⊢ ↑⟨↑I⁻¹, ⋯⟩ * ↑⟨↑I, ⋯⟩ = ↑1

Tactic:
coe_one

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
P' : Type u_3
inst✝⁴ : CommRing P'
inst✝³ : Algebra R P'
P'' : Type u_4
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
inst✝ : IsLocalization S P
I : (Submodule R P)ˣ
⊢ ↑⟨↑I⁻¹, ⋯⟩ * ↑⟨↑I, ⋯⟩ = 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg
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₁
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ ↑I * (↑1 / ↑I) ≤ ↑1

Tactic:
coe_one

Goal state after:
case neg
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₁
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ ↑I * (1 / ↑I) ≤ 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg
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₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (↑1 / ↑I)

Tactic:
coe_one

Goal state after:
case neg
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₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg
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₁
I : FractionalIdeal R₁⁰ K
hI : ↑I ≤ ↑1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)

Tactic:
coe_one

Goal state after:
case neg
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₁
I : FractionalIdeal R₁⁰ K
hI : ↑I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)
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 / map (↑h) I = 1 / map (↑h) I

Tactic:
FractionalIdeal.map_one

Goal state after:
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'
⊢ 1 / map (↑h) I = 1 / map (↑h) I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_2
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ IsInteger R₁ (↑a' • 0)

Tactic:
smul_zero

Goal state after:
case refine_2
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ IsInteger R₁ 0
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case e'_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
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)) =
    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)))

Tactic:
ring

Goal state after: