mathlib-initiative/mathlib-tactics huggingface dataset:
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).restrict ⋯) ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
[

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).restrict ⋯) ⟨x, hx⟩ = ⟨y, hy⟩
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
j : Fin 8
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «0».«0»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «0».«1»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «0».«2»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «0».«3»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «0».«4»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «0».«5»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «0».«6»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «0».«7»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1»
j : Fin 8
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «1».«0»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «1».«1»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «1».«2»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «1».«3»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «1».«4»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «1».«5»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «1».«6»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «1».«7»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2»
j : Fin 8
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «2».«0»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «2».«1»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «2».«2»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «2».«3»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «2».«4»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «2».«5»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «2».«6»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «2».«7»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ b ∈ ↑J, IsInteger R (a • b)
⊢ ∀ b ∈ I, IsInteger R (a • b)

Tactic:
intro b b_mem

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ b ∈ ↑J, IsInteger R (a • b)
b : P
b_mem : b ∈ I
⊢ IsInteger R (a • b)
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3»
j : Fin 8
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «3».«0»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «3».«1»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «3».«2»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «3».«3»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «3».«4»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «3».«5»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «3».«6»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «3».«7»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0
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✝ : IsCancelMulZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
⊢ ↑(d ⟨u, hu'⟩) = 1

Tactic:
[

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : IsCancelMulZero M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
inst✝ : IsCancelMulZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
⊢ ↑(d ⟨u, hu'⟩) = 1
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4»
j : Fin 8
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «4».«0»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «4».«1»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «4».«2»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «4».«3»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «4».«4»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «4».«5»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «4».«6»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «4».«7»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
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 ↑α
μ : ↥LieSubalgebra.root
hμ : μ ∈ I.rootSet
this : ↑span_compl_roots = ⨆ β, ⨆ (_ : β ∉ I.rootSet), ↑(f β)
⊢ ↑span_compl_roots ≤ Weight.ker

Tactic:
this

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
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 ↑α
μ : ↥LieSubalgebra.root
hμ : μ ∈ I.rootSet
this : ↑span_compl_roots = ⨆ β, ⨆ (_ : β ∉ I.rootSet), ↑(f β)
⊢ ⨆ β, ⨆ (_ : β ∉ I.rootSet), ↑(f β) ≤ Weight.ker
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5»
j : Fin 8
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «5».«0»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «5».«1»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «5».«2»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «5».«3»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «5».«4»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «5».«5»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «5».«6»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «5».«7»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0
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
⊢ ↑1 = 1

Tactic:
coe_one_eq_coeSubmodule_top,

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
⊢ coeSubmodule P ⊤ = 1
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6»
j : Fin 8
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «6».«0»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «6».«1»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «6».«2»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «6».«3»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «6».«4»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «6».«5»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «6».«6»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «6».«7»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «7»
j : Fin 8
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «7».«0»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «7».«1»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «7».«2»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «7».«3»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «7».«4»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «7».«5»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «7».«6»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «7».«7»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0
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 p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
this : ↑(d ⟨p, ⋯⟩) ^ s = ↑(d ⟨p ^ s, hs'⟩)
⊢ ↑(d ⟨p, ⋯⟩) ^ s ≤ n

Tactic:
this

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 p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
this : ↑(d ⟨p, ⋯⟩) ^ s = ↑(d ⟨p ^ s, hs'⟩)
⊢ ↑(d ⟨p ^ s, hs'⟩) ≤ n
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
j : Fin 4
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «0».«0»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «0».«1»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «0».«2»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «0».«3»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1»
j : Fin 4
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «1».«0»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «1».«1»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «1».«2»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «1».«3»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2»
j : Fin 4
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «2».«0»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «2».«1»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «2».«2»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «2».«3»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3»
j : Fin 4
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «3».«0»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «3».«1»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «3».«2»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «3».«3»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
j : Fin 2
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «0».«0»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «0».«1»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1»
j : Fin 2
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

Tactic:
fin_cases j

Goal state after:
case «1».«0»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «1».«1»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
FiniteMultiplicity.of_prime_left (prime_of_normalized_factor p hp) hm
    |>.emultiplicity_eq_multiplicity,

Goal state after:
case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑(multiplicity p m) ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n
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✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
⊢ Prime (Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩))

Tactic:
this

Goal state after:
M : Type u_1
inst✝⁶ : CommMonoidWithZero M
inst✝⁵ : IsCancelMulZero M
N : Type u_2
inst✝⁴ : CommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
⊢ Prime ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
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
J : FractionalIdeal R₁⁰ K
h : J ≠ 0
⊢ ↑J⁻¹ = IsLocalization.coeSubmodule K ⊤ / ↑J

Tactic:
[

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
J : FractionalIdeal R₁⁰ K
h : J ≠ 0
⊢ ↑J⁻¹ = IsLocalization.coeSubmodule K ⊤ / ↑J
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
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) = (map (↑h) I)⁻¹

Tactic:
FractionalIdeal.map_div,

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
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 = (map (↑h) I)⁻¹
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✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
⊢ emultiplicity (Associates.mk p) (Associates.mk m) =
    emultiplicity (Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩))
      (Associates.mk n)

Tactic:
this

Goal state after:
M : Type u_1
inst✝⁶ : CommMonoidWithZero M
inst✝⁵ : IsCancelMulZero M
N : Type u_2
inst✝⁴ : CommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
⊢ emultiplicity (Associates.mk p) (Associates.mk m) =
    emultiplicity (↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)) (Associates.mk n)
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'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P'
⊢ map (↑g) (map (↑g.symm) I) = I

Tactic:
by rw [← map_comp, AlgEquiv.comp_symm, map_id]

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
h : 0 = 1
⊢ 1 ∈ 0

Tactic:
← (algebraMap R₁ K).map_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
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
h : 0 = 1
⊢ (algebraMap R₁ K) 1 ∈ 0
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
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
x✝ : K
h : x✝ ∈ I
⊢ x✝ ∈ ⟨↑I / ↑1, ⋯⟩

Tactic:
apply mem_div_iff_forall_mul_mem.mpr
    rintro y ⟨y', _, rfl⟩
    convert! Submodule.smul_mem _ y' h using 1
    rw [mul_comm, Algebra.linearMap_apply, ← Algebra.smul_def]

Goal state after: