Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/goal.txt

Created February 5, 2019 10:05
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kbuzzard/75f316bccc64cb17f5217e02e364b4e8 to your computer and use it in GitHub Desktop.
Save kbuzzard/75f316bccc64cb17f5217e02e364b4e8 to your computer and use it in GitHub Desktop.
Download ZIP
eq.rec hell
Raw
goal.txt
⊢ @eq.{u₁+1}
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
(@eq.rec.{u₁+1 u₁+1}
(@quot.{u₁+1} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@setoid.r.{u₁+1} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@quotient_group.left_rel.{u₁} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@multiplicative.group.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)
(@finsupp.add_group.{u₁ 0} R int (λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
int.decidable_eq
(@add_comm_group.to_add_group.{0} int
(@ring.to_add_comm_group.{0} int
(@domain.to_ring.{0} int
(@to_domain.{0} int
(@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
int.decidable_linear_ordered_comm_ring))))))))
(@is_group_hom.ker.{u₁ u₂} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)) Γ₁
(@multiplicative.group.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)
(@finsupp.add_group.{u₁ 0} R int (λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
int.decidable_eq
(@add_comm_group.to_add_group.{0} int
(@ring.to_add_comm_group.{0} int
(@domain.to_ring.{0} int
(@to_domain.{0} int
(@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
int.decidable_linear_ordered_comm_ring))))))))
(@comm_group.to_group.{u₂} Γ₁ (@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))
(λ (f : multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)),
@finsupp.prod.{u₁ 0 u₂} R int Γ₁ int.has_zero
(@comm_group.to_comm_monoid.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))
f
(λ (r : R),
@has_pow.pow.{u₂ 0} Γ₁ int
(@group.has_pow.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5)))
(@option.get_or_else.{u₂} Γ₁
(@coe_fn.{(max 1 (u₁+1) (u₂+1)) (max (u₁+1) (u₂+1))}
(@valuation.{u₁ u₂} R _inst_4 Γ₁ _inst_5)
(@valuation.has_coe_to_fun.{u₁ u₂} R _inst_4 Γ₁ _inst_5)
v₁
r)
(@has_one.one.{u₂} Γ₁
(@monoid.to_has_one.{u₂} Γ₁
(@group.to_monoid.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))))))))
(@valuation.minimal_value_group._proof_1.{u₁ u₂} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₁
_inst_5
v₁))
(@valuation.minimal_value_group._proof_2.{u₁ u₂} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₁
_inst_5
v₁))))
(@quot.mk.{u₁+1} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@setoid.r.{u₁+1} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@quotient_group.left_rel.{u₁} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@multiplicative.group.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)
(@finsupp.add_group.{u₁ 0} R int (λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
int.decidable_eq
(@add_comm_group.to_add_group.{0} int
(@ring.to_add_comm_group.{0} int
(@domain.to_ring.{0} int
(@to_domain.{0} int
(@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
int.decidable_linear_ordered_comm_ring))))))))
(@is_group_hom.ker.{u₁ u₂} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)) Γ₁
(@multiplicative.group.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)
(@finsupp.add_group.{u₁ 0} R int (λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
int.decidable_eq
(@add_comm_group.to_add_group.{0} int
(@ring.to_add_comm_group.{0} int
(@domain.to_ring.{0} int
(@to_domain.{0} int
(@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
int.decidable_linear_ordered_comm_ring))))))))
(@comm_group.to_group.{u₂} Γ₁ (@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))
(λ (f : multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)),
@finsupp.prod.{u₁ 0 u₂} R int Γ₁ int.has_zero
(@comm_group.to_comm_monoid.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))
f
(λ (r : R),
@has_pow.pow.{u₂ 0} Γ₁ int
(@group.has_pow.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5)))
(@option.get_or_else.{u₂} Γ₁
(@coe_fn.{(max 1 (u₁+1) (u₂+1)) (max (u₁+1) (u₂+1))}
(@valuation.{u₁ u₂} R _inst_4 Γ₁ _inst_5)
(@valuation.has_coe_to_fun.{u₁ u₂} R _inst_4 Γ₁ _inst_5)
v₁
r)
(@has_one.one.{u₂} Γ₁
(@monoid.to_has_one.{u₂} Γ₁
(@group.to_monoid.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))))))))
(@valuation.minimal_value_group._proof_1.{u₁ u₂} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₁
_inst_5
v₁))
(@valuation.minimal_value_group._proof_2.{u₁ u₂} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₁
_inst_5
v₁)))
g₁)
(λ
(g :
@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₂} Γ₁ _inst_5
(@valuation.minimal_value_group.{u₁ u₂} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₁
_inst_5
v₁)),
@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
(@finsupp.prod.{u₁ 0 u₁} R int
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
int.has_zero
(@comm_group.to_comm_monoid.{u₁}
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
(@valuation.minimal_valuation.parametrized_subgroup.grp.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂)))
g₂
(λ (r : R),
@has_pow.pow.{u₁ 0}
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
int
(@group.has_pow.{u₁}
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
(@comm_group.to_group.{u₁}
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
(@valuation.minimal_valuation.parametrized_subgroup.grp.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))))
(@valuation.minimal_value_group.mk.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂
r)))
(@quot.mk.{u₁+1} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@setoid.r.{u₁+1} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@quotient_group.left_rel.{u₁} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@multiplicative.group.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)
(@finsupp.add_group.{u₁ 0} R int (λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
int.decidable_eq
(@add_comm_group.to_add_group.{0} int
(@ring.to_add_comm_group.{0} int
(@domain.to_ring.{0} int
(@to_domain.{0} int
(@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
int.decidable_linear_ordered_comm_ring))))))))
(@is_group_hom.ker.{u₁ u₂} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)) Γ₁
(@multiplicative.group.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)
(@finsupp.add_group.{u₁ 0} R int (λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
int.decidable_eq
(@add_comm_group.to_add_group.{0} int
(@ring.to_add_comm_group.{0} int
(@domain.to_ring.{0} int
(@to_domain.{0} int
(@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
int.decidable_linear_ordered_comm_ring))))))))
(@comm_group.to_group.{u₂} Γ₁ (@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))
(λ (f : multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)),
@finsupp.prod.{u₁ 0 u₂} R int Γ₁ int.has_zero
(@comm_group.to_comm_monoid.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))
f
(λ (r : R),
@has_pow.pow.{u₂ 0} Γ₁ int
(@group.has_pow.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5)))
(@option.get_or_else.{u₂} Γ₁
(@coe_fn.{(max 1 (u₁+1) (u₂+1)) (max (u₁+1) (u₂+1))}
(@valuation.{u₁ u₂} R _inst_4 Γ₁ _inst_5)
(@valuation.has_coe_to_fun.{u₁ u₂} R _inst_4 Γ₁ _inst_5)
v₁
r)
(@has_one.one.{u₂} Γ₁
(@monoid.to_has_one.{u₂} Γ₁
(@group.to_monoid.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))))))))
(@valuation.minimal_value_group._proof_1.{u₁ u₂} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₁
_inst_5
v₁))
(@valuation.minimal_value_group._proof_2.{u₁ u₂} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₁
_inst_5
v₁)))
g₂)
(@quot.sound.{u₁+1} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@setoid.r.{u₁+1} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@quotient_group.left_rel.{u₁} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@multiplicative.group.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)
(@finsupp.add_group.{u₁ 0} R int (λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
int.decidable_eq
(@add_comm_group.to_add_group.{0} int
(@ring.to_add_comm_group.{0} int
(@domain.to_ring.{0} int
(@to_domain.{0} int
(@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
int.decidable_linear_ordered_comm_ring))))))))
(@is_group_hom.ker.{u₁ u₂} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)) Γ₁
(@multiplicative.group.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)
(@finsupp.add_group.{u₁ 0} R int (λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
int.decidable_eq
(@add_comm_group.to_add_group.{0} int
(@ring.to_add_comm_group.{0} int
(@domain.to_ring.{0} int
(@to_domain.{0} int
(@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
int.decidable_linear_ordered_comm_ring))))))))
(@comm_group.to_group.{u₂} Γ₁ (@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))
(λ (f : multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)),
@finsupp.prod.{u₁ 0 u₂} R int Γ₁ int.has_zero
(@comm_group.to_comm_monoid.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))
f
(λ (r : R),
@has_pow.pow.{u₂ 0} Γ₁ int
(@group.has_pow.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5)))
(@option.get_or_else.{u₂} Γ₁
(@coe_fn.{(max 1 (u₁+1) (u₂+1)) (max (u₁+1) (u₂+1))}
(@valuation.{u₁ u₂} R _inst_4 Γ₁ _inst_5)
(@valuation.has_coe_to_fun.{u₁ u₂} R _inst_4 Γ₁ _inst_5)
v₁
r)
(@has_one.one.{u₂} Γ₁
(@monoid.to_has_one.{u₂} Γ₁
(@group.to_monoid.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))))))))
(@valuation.minimal_value_group._proof_1.{u₁ u₂} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₁
_inst_5
v₁))
(@valuation.minimal_value_group._proof_2.{u₁ u₂} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₁
_inst_5
v₁)))
g₁
g₂
(@or.inl
(@eq.{u₂+1} Γ₁
(@finsupp.prod.{u₁ 0 u₂} R int Γ₁ int.has_zero
(@comm_group.to_comm_monoid.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))
(@has_mul.mul.{u₁} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@semigroup.to_has_mul.{u₁} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@monoid.to_semigroup.{u₁} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@group.to_monoid.{u₁} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@multiplicative.group.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)
(@finsupp.add_group.{u₁ 0} R int
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
int.decidable_eq
(@add_comm_group.to_add_group.{0} int
(@ring.to_add_comm_group.{0} int
(@domain.to_ring.{0} int
(@to_domain.{0} int
(@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0}
int
int.decidable_linear_ordered_comm_ring)))))))))))
(@has_inv.inv.{u₁} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@group.to_has_inv.{u₁} (multiplicative.{u₁} (@finsupp.{u₁ 0} R int int.has_zero))
(@multiplicative.group.{u₁} (@finsupp.{u₁ 0} R int int.has_zero)
(@finsupp.add_group.{u₁ 0} R int
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
int.decidable_eq
(@add_comm_group.to_add_group.{0} int
(@ring.to_add_comm_group.{0} int
(@domain.to_ring.{0} int
(@to_domain.{0} int
(@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0}
int
int.decidable_linear_ordered_comm_ring)))))))))
g₁)
g₂)
(λ (r : R),
@has_pow.pow.{u₂ 0} Γ₁ int
(@group.has_pow.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5)))
(@option.get_or_else.{u₂} Γ₁
(@coe_fn.{(max 1 (u₁+1) (u₂+1)) (max (u₁+1) (u₂+1))}
(@valuation.{u₁ u₂} R _inst_4 Γ₁ _inst_5)
(@valuation.has_coe_to_fun.{u₁ u₂} R _inst_4 Γ₁ _inst_5)
v₁
r)
(@has_one.one.{u₂} Γ₁
(@monoid.to_has_one.{u₂} Γ₁
(@group.to_monoid.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))))))))
(@has_one.one.{u₂} Γ₁
(@monoid.to_has_one.{u₂} Γ₁
(@group.to_monoid.{u₂} Γ₁
(@comm_group.to_group.{u₂} Γ₁
(@linear_ordered_comm_group.to_comm_group.{u₂} Γ₁ _inst_5))))))
false
h12)))
(@finsupp.prod.{u₁ 0 u₁} R int
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
int.has_zero
(@comm_group.to_comm_monoid.{u₁}
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
(@valuation.minimal_valuation.parametrized_subgroup.grp.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂)))
g₂
(λ (r : R),
@has_pow.pow.{u₁ 0}
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
int
(@group.has_pow.{u₁}
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
(@comm_group.to_group.{u₁}
(@valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))
(@valuation.minimal_valuation.parametrized_subgroup.grp.{u₁ u₃} Γ₂ _inst_6
(@valuation.minimal_value_group.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂))))
(@valuation.minimal_value_group.mk.{u₁ u₃} R _inst_4
(λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b))
Γ₂
_inst_6
v₂
r)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment