-- Mathlib/NumberTheory/FunctionField.lean
theorem InftyValuation.map_mul' (x y : RatFunc Fq) :
    inftyValuationDef Fq (x * y) = inftyValuationDef Fq x * inftyValuationDef Fq y

Proof state:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ (if x * y = 0 then 0 else ↑(Multiplicative.ofAdd (x * y).intDegree)) =
    (if x = 0 then 0 else ↑(Multiplicative.ofAdd x.intDegree)) *
      if y = 0 then 0 else ↑(Multiplicative.ofAdd y.intDegree)

Tactic:
rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]

Result:
no goals

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
⊢ (if x * y = 0 then 0 else ↑(Multiplicative.ofAdd (x * y).intDegree)) =
    (if x = 0 then 0 else ↑(Multiplicative.ofAdd x.intDegree)) *
      if y = 0 then 0 else ↑(Multiplicative.ofAdd y.intDegree)

Tactic:
by_cases hx : x = 0

Result:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ (if x * y = 0 then 0 else ↑(Multiplicative.ofAdd (x * y).intDegree)) =
    (if x = 0 then 0 else ↑(Multiplicative.ofAdd x.intDegree)) *
      if y = 0 then 0 else ↑(Multiplicative.ofAdd y.intDegree)

case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
⊢ (if x * y = 0 then 0 else ↑(Multiplicative.ofAdd (x * y).intDegree)) =
    (if x = 0 then 0 else ↑(Multiplicative.ofAdd x.intDegree)) *
      if y = 0 then 0 else ↑(Multiplicative.ofAdd y.intDegree)

Proof state:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
⊢ (if x * y = 0 then 0 else ↑(Multiplicative.ofAdd (x * y).intDegree)) =
    (if x = 0 then 0 else ↑(Multiplicative.ofAdd x.intDegree)) *
      if y = 0 then 0 else ↑(Multiplicative.ofAdd y.intDegree)

Tactic:
by_cases hy : y = 0

Result:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else ↑(Multiplicative.ofAdd (x * y).intDegree)) =
    (if x = 0 then 0 else ↑(Multiplicative.ofAdd x.intDegree)) *
      if y = 0 then 0 else ↑(Multiplicative.ofAdd y.intDegree)

case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else ↑(Multiplicative.ofAdd (x * y).intDegree)) =
    (if x = 0 then 0 else ↑(Multiplicative.ofAdd x.intDegree)) *
      if y = 0 then 0 else ↑(Multiplicative.ofAdd y.intDegree)

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
⊢ inftyValuationDef Fq (x * y) = inftyValuationDef Fq x * inftyValuationDef Fq y

Tactic:
rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]

Result:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
⊢ (if x * y = 0 then 0 else ↑(Multiplicative.ofAdd (x * y).intDegree)) =
    (if x = 0 then 0 else ↑(Multiplicative.ofAdd x.intDegree)) *
      if y = 0 then 0 else ↑(Multiplicative.ofAdd y.intDegree)

Proof state:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else ↑(Multiplicative.ofAdd (x * y).intDegree)) =
    (if x = 0 then 0 else ↑(Multiplicative.ofAdd x.intDegree)) *
      if y = 0 then 0 else ↑(Multiplicative.ofAdd y.intDegree)

Tactic:
rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithZero.coe_mul, WithZero.coe_inj,
  ← ofAdd_add, RatFunc.intDegree_mul hx hy]

Result:
no goals

Proof state:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else ↑(Multiplicative.ofAdd (x * y).intDegree)) =
    (if x = 0 then 0 else ↑(Multiplicative.ofAdd x.intDegree)) *
      if y = 0 then 0 else ↑(Multiplicative.ofAdd y.intDegree)

Tactic:
rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]

Result:
no goals