Theorem: Groth16TypeIII.Polynomial.mul_self_modByMonic (FormalSnarksProject/Other/Groth16TypeIIIQuotientVersion.lean)

State before:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ (t * p).modByMonic t = 0
Tactic:
rw [Polynomial.dvd_iff_modByMonic_eq_zero]
State after:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t ∣ t * p

F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic

State before:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t ∣ t * p

F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic
Tactic:
apply dvd_mul_right
State after:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic

State before:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic
Tactic:
exact mt
State after:
no goals