mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
⊢ (I ^ n • ⊤).mkQ ∘ₗ lift I f ⋯ = f n

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
x✝ : M
⊢ ((I ^ n • ⊤).mkQ ∘ₗ lift I f ⋯) x✝ = (f n) x✝
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
J : Ideal S
⊢ J.IsMaximal ↔ (under R J).IsMaximal ∧ y ∉ under R J

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
J : Ideal S
⊢ J.IsMaximal → (under R J).IsMaximal ∧ y ∉ under R J

case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
J : Ideal S
⊢ (under R J).IsMaximal ∧ y ∉ under R J → J.IsMaximal
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
⊢ Submodule.factorPow I N hle ∘ₗ extend ha f n = extend ha f m

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x✝ : M
⊢ (Submodule.factorPow I N hle ∘ₗ extend ha f n) x✝ = (extend ha f m) x✝
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
n : ℕ
⊢ (I ^ a n • ⊤).mkQ ∘ₗ lift I ha f ⋯ = f n

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
n : ℕ
x✝ : M
⊢ ((I ^ a n • ⊤).mkQ ∘ₗ lift I ha f ⋯) x✝ = (f n) x✝
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : KrullDimLE 0 R
⊢ minimalPrimes R = {I | I.IsPrime}

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : KrullDimLE 0 R
x✝ : Ideal R
⊢ x✝ ∈ minimalPrimes R ↔ x✝ ∈ {I | I.IsPrime}
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : KrullDimLE 0 R
⊢ minimalPrimes R = {I | I.IsMaximal}

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : KrullDimLE 0 R
x✝ : Ideal R
⊢ x✝ ∈ minimalPrimes R ↔ x✝ ∈ {I | I.IsMaximal}
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
⊢ (∀ (x : R), IsNilpotent x ↔ ¬IsUnit x) → (nilradical R).IsMaximal

Tactic:
refine fun H ↦ ⟨fun e ↦ ?_, fun I hI ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
e : nilradical R = ⊤
⊢ False

case refine_2
R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
I : Ideal R
hI : nilradical R < I
⊢ I = ⊤
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
x✝ : Valuation R Γ₀
⊢ map (MonoidWithZeroHom.ofClass f.symm) ⋯ (map (MonoidWithZeroHom.ofClass f) ⋯ x✝) = x✝

Tactic:
ext

Goal state after:
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
x✝ : Valuation R Γ₀
r✝ : R
⊢ (map (MonoidWithZeroHom.ofClass f.symm) ⋯ (map (MonoidWithZeroHom.ofClass f) ⋯ x✝)) r✝ = x✝ r✝
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
x✝ : Valuation R Γ'₀
⊢ map (MonoidWithZeroHom.ofClass f) ⋯ (map (MonoidWithZeroHom.ofClass f.symm) ⋯ x✝) = x✝

Tactic:
ext

Goal state after:
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
x✝ : Valuation R Γ'₀
r✝ : R
⊢ (map (MonoidWithZeroHom.ofClass f) ⋯ (map (MonoidWithZeroHom.ofClass f.symm) ⋯ x✝)) r✝ = x✝ r✝
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
hI' : ¬I = ⊤
hx : maximalIdeal R = Ideal.span {0}
H : ∀ (r : R), ¬IsUnit r ↔ 0 ∣ r
⊢ False

Tactic:
apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
hI' : ¬I = ⊤
hx : maximalIdeal R = Ideal.span {0}
H : ∀ (r : R), ¬IsUnit r ↔ 0 ∣ r
⊢ maximalIdeal R = ⊥
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a : R
hi : Irreducible (Classical.choose ⋯)
⊢ (addVal R) a = ⊤ ↔ a = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a : R
hi : Irreducible (Classical.choose ⋯)
⊢ (addVal R) a = ⊤ → a = 0

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a : R
hi : Irreducible (Classical.choose ⋯)
⊢ a = 0 → (addVal R) a = ⊤
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
⊢ (addVal R) a ≤ (addVal R) b ↔ a ∣ b

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
⊢ (addVal R) a ≤ (addVal R) b → a ∣ b

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
⊢ a ∣ b → (addVal R) a ≤ (addVal R) b
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ (addVal R) x = (addVal R) y ↔ Associated x y

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ (addVal R) x = (addVal R) y → Associated x y

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ Associated x y → (addVal R) x = (addVal R) y
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
⊢ ∃ r s, 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict s = ↑γ

Tactic:
use x, a, hx, zero_lt_iff.mpr ha

Goal state after:
case right
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
⊢ v.restrict x / v.restrict a = ↑γ
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
⊢ v.leAddSubgroup 0 = ⊥

Tactic:
ext

Goal state after:
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
x✝ : K
⊢ x✝ ∈ v.leAddSubgroup 0 ↔ x✝ ∈ ⊥
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : Associates R
⊢ Quot.out x ∈ R⁰ ↔ span {Quot.out x} ∈ (Ideal R)⁰

Tactic:
span_singleton_nonZeroDivisors

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : Associates R
⊢ Quot.out x ∈ R⁰ ↔ Quot.out x ∈ R⁰
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
h : I ≠ ⊥
⊢ Submodule.subtype I ∘ₗ ↑(isoBaseOfIsPrincipal h) = (LinearMap.mul R R) (IsPrincipal.generator I)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
h : I ≠ ⊥
⊢ (Submodule.subtype I ∘ₗ ↑(isoBaseOfIsPrincipal h)) 1 = ((LinearMap.mul R R) (IsPrincipal.generator I)) 1
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → IsPrincipalIdealRing R
tfae_1_to_4 : IsPrincipalIdealRing R → IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ Std.Total fun x1 x2 ↦ x1 ≤ x2

Tactic:
constructor

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → IsPrincipalIdealRing R
tfae_1_to_4 : IsPrincipalIdealRing R → IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ ∀ (a b : Ideal R), a ≤ b ∨ b ≤ a
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
hr : IsRegular r
inst✝ : Flat R M
h : Function.Injective ⇑(rTensor M (toSpanSingleton R R r))
⊢ (fun x ↦ r • x) = ⇑(↑(TensorProduct.lid R M) ∘ₗ rTensor M (toSpanSingleton R R r) ∘ₗ ↑(TensorProduct.lid R M).symm)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
hr : IsRegular r
inst✝ : Flat R M
h : Function.Injective ⇑(rTensor M (toSpanSingleton R R r))
x✝ : M
⊢ r • x✝ = (↑(TensorProduct.lid R M) ∘ₗ rTensor M (toSpanSingleton R R r) ∘ₗ ↑(TensorProduct.lid R M).symm) x✝
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ ⇑(lift (lsmul R M)) ∘ ⇑(TensorProduct.lid R M).symm.toEquiv = id

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
x✝ : M
⊢ (⇑(lift (lsmul R M)) ∘ ⇑(TensorProduct.lid R M).symm.toEquiv) x✝ = id x✝
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i : ι
⊢ (algebraMap K L) 2 = 2

Tactic:
rw [← Int.cast_two (R := K), ← Int.cast_two (R := L), map_intCast]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ { toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } j -
      (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
              (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
            ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } j))
          ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) •
        { toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i =
    { toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j)

Tactic:
ext

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ ↑({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } j -
        (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
                (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
              ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } j))
            ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) •
          { toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i) =
    ↑({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j))
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ { toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j -
      (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
              (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
            ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i))
          ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j) •
        { toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i =
    { toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j)

Tactic:
ext

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ ↑({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j -
        (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
                (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
              ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i))
            ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j) •
          { toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) =
    ↑({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j))
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: T : Type u_2
inst✝ : NonUnitalCommSemiring T
⊢ ↑(sumSq T) = {s | IsSumSq s}

Tactic:
ext

Goal state after:
T : Type u_2
inst✝ : NonUnitalCommSemiring T
x✝ : T
⊢ x✝ ∈ ↑(sumSq T) ↔ x✝ ∈ {s | IsSumSq s}
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: T : Type u_2
inst✝ : CommSemiring T
⊢ ↑(sumSq T) = {s | IsSumSq s}

Tactic:
ext

Goal state after:
T : Type u_2
inst✝ : CommSemiring T
x✝ : T
⊢ x✝ ∈ ↑(sumSq T) ↔ x✝ ∈ {s | IsSumSq s}
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
hx : x ∈ span S (range ⇑P.root)
i : ι
⊢ range ⇑(algebraMap S R) = ↑(Algebra.linearMap S R).range

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
hx : x ∈ span S (range ⇑P.root)
i : ι
x✝ : R
⊢ x✝ ∈ range ⇑(algebraMap S R) ↔ x✝ ∈ ↑(Algebra.linearMap S R).range
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Module S M
i : ι
⊢ P.rootSpanMem S ((P.reflectionPerm i) i) = -P.rootSpanMem S i

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Module S M
i : ι
⊢ ↑(P.rootSpanMem S ((P.reflectionPerm i) i)) = ↑(-P.rootSpanMem S i)
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Module S N
i : ι
⊢ P.corootSpanMem S ((P.reflectionPerm i) i) = -P.corootSpanMem S i

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Module S N
i : ι
⊢ ↑(P.corootSpanMem S ((P.reflectionPerm i) i)) = ↑(-P.corootSpanMem S i)
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: case add
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x y z : M
hy : y ∈ span R (range ⇑P.root)
hz : z ∈ span R (range ⇑P.root)
hy' : y ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
hz' : z ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
⊢ y + z ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))

Tactic:
| add y z hy hz hy' hz' =>

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ ↑(Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator) = ↑(⨅ i, LinearMap.ker (P.root' i))

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x✝ : N
⊢ x✝ ∈ ↑(Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator) ↔
    x✝ ∈ ↑(⨅ i, LinearMap.ker (P.root' i))
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ ↑(Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator) =
    ↑(span R (range P.root')).dualCoannihilator

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x✝ : N
⊢ x✝ ∈ ↑(Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator) ↔
    x✝ ∈ ↑(span R (range P.root')).dualCoannihilator
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
⊢ P.flip.toLinearMap ∘ₗ P.Polarization = P.RootForm

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x✝¹ x✝ : M
⊢ ((P.flip.toLinearMap ∘ₗ P.Polarization) x✝¹) x✝ = (P.RootForm x✝¹) x✝